Not commiting the flake.lock file makes the nix code virtually unusable

[MangoIV]

Hi, I'm having some issues wrt nix:

• I cannot use any command that cannot write lockfiles (like nix run github:leanprover/lake)
• reproducibility will be broken
• I do not understand how it adds maintenance cost to commit the lockfile, from my understanding, it should decrease it because we don't have to change the nix code until we really want; like this it can just break upon getting a new version of nixpkgs or any other input.

[MangoIV]

I have a solution for this, though:

• use https://github.com/DeterminateSystems/update-flake-lock to regularly update flake lock
• follow lean nixpkgs

Note
I can do both if wanted

Warning
in case you use the update-flake-lock-action, you will have to add a github token

[Kha]

The only correct solution is to keep the locked lean input in sync with lean-toolchain, which would be a hassle to do manually for virtually no users. In any case, when Kha/lean4@25db543 is merged, you can simply use the Lean flake instead. We should probably remove the Nix code from this repo at that point, or right now.

[MangoIV]

@Kha perhaps my PR does what you want (keep it in sync)

I have noticed that the nix code in the lean repo is really weird. E g it doesn’t follow the standard output scheme making it not work with tools like nix flake show, is there a specific reason for it?

[Kha]

perhaps

How would it do that without even referencing lean-toolchain

making it not work with tools like nix flake show

That doesn't work anyway because of IFD (edit: I see this has been addressed by NixOS/nix#6988)

[MangoIV]

How would it do that without even referencing lean-toolchain

I will have a look what the difference there is, principally though, if we have a flake update action it should not get out of sync and also not break randomly

That doesn't work anyway because of IFD

even without the nix fix, there's a hack fix for this.

nix flake show not working is not the only reason why not following the standard output schema is bad, though...