Incorrect manifest used

[alexstaeding]

I'm trying to set up a lean project with a flake, but I'm running into an issue as soon as I add mathlib4 as a dependency.

1. I started with the template:

nix flake new --template github:lenianiva/lean4-nix#dependency .

2. Then I replaced the lakefile.lean with a lakefile.toml and added the mathlib dependency:

name = "example"

[[lean_exe]]
name = "hello_world"
srcDir = "."
root = "Example"

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.24.0"

3. In the flake, I had to disable the binary lean distribution to make the build work at all on aarch64-darwin

_module.args.pkgs = import nixpkgs {
  inherit system;
  overlays = [
    (lean4-nix.readToolchainFile {
      toolchain = ./lean-toolchain;
      binary = system != "aarch64-darwin";
    })
  ];
};

4. I use nix run .# to run the default target in the flake, and get this as an output:

nix run .#                                                                                                                                                                                                                                              19s 18:11:06
warning: Git tree '/Users/alex/Documents/Git/me/lean4-nix-error' is dirty
error:
       … while calling the 'derivationStrict' builtin
         at <nix/derivation-internal.nix>:37:12:
           36|
           37|   strict = derivationStrict drvAttrs;
             |            ^
           38|

       … while evaluating derivation 'example'
         whose name attribute is located at /nix/store/qjg5hnnkydk3mri5k6rydhj08x9s7xya-source/pkgs/stdenv/generic/make-derivation.nix:540:13

       … while evaluating attribute 'buildCommand' of derivation 'example'
         at /nix/store/qjg5hnnkydk3mri5k6rydhj08x9s7xya-source/pkgs/build-support/trivial-builders/default.nix:80:17:
           79|         enableParallelBuilding = true;
           80|         inherit buildCommand name;
             |                 ^
           81|         passAsFile = [ "buildCommand" ] ++ (derivationArgs.passAsFile or [ ]);

       (stack trace truncated; use '--show-trace' to show the full, detailed trace)

       error: attribute '"ProofWidgets.Compat"' missing
       at /nix/store/3541lxww7nysxg7w019xfd7fqk7mx1i6-source/manifests/v4.22.0.nix:284:20:
          283|               then modCandidates.${dep}
          284|               else externalModMap.${dep})
             |                    ^
          285|             deps))

What's strange about this error is that it seems that despite my lean-toolchain containing a reference to lean v4.24, it seem that v4.22 is being used:

> cat lean-toolchain                                                                                                                                                                                                                                     
leanprover/lean4:v4.24.0

I also tried replacing the overlay with this, but it ends up with the same error about lean v4.22

(lean4-nix.readToolchain {
  toolchain = "leanprover/lean4:v4.24.0";
  binary = system != "aarch64-darwin";
})

I'm using the latest version of this flake:

├───lean4-nix: github:lenianiva/lean4-nix/3550873ed1a87d666d633d34921e79abaa4671c1?narHash=sha256-eEs2YpE84%2Bd6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk%3D (2025-10-25 05:01:07)

[lenianiva]

Can you set pkg.lean as a flake package output, and run nix build .#lean -- --version? This would show you which version is active.

[alexstaeding]

nix run .#lean -- --version does indeed show v4.24, so I'm not sure whats going on here.

(And it's not just showing the nixpkgs version, because it changes to v4.23 when I update the toolchain)

[lenianiva]

nix run .#lean -- --version does indeed show v4.24, so I'm not sure whats going on here.

(And it's not just showing the nixpkgs version, because it changes to v4.23 when I update the toolchain)

Can you show the complete example?

[alexstaeding]

Here you go https://github.com/alexstaeding/lean4-nix-issue-84

nix run leads to the error in the original description.

If I remove the mathlib dependency in lakefile.toml and refresh the lake-manifest.json, then nix run works as expected.

[lenianiva]

The reason it is using v4.22.0 is because the buildLeanPackage function was inherited from this earlier manifest.

I'm refactoring the code to use lake to build packages in the future, which should resolve this issue.

[lenianiva]

Now that #88 is merged this should not be a problem anymore.

Note that you must remove .executable or .sharedLib after mkPackage since its output is now a proper derivation.