Building a Lean Project with `flake.nix`

Stream: new members

[Agnishom Chattopadhyay]

First, I will confess that I do not really understand the nix toolchain very well.

I was wondering if it is possible to produce a flake.nix which can do the following.

1. I should be able to pin the version of the Lean to a specific version I want.
2. When I run nix develop, it should spawn a shell which has the appropriate lean tools available along with the plugin for VSCode.
3. When I run nix build, it should run something which is equivalent to lake build-- checking the proofs, in effect.

I have seen some flake.nix based Lean projects, but they seem to be doing something different. For example, this one does not seem to be running lake build

[Agnishom Chattopadhyay]

Does anyone have any thoughts on this?

I also have the analogous question for Coq

[Sebastian Ullrich]

Step 3 would have to always start from scratch instead of reusing previous results, do you really want that?

[Walter Moreira]

Using the tooling of Lean in the context of nix build is tricky, because (as far as I understand) there isn't still good support for installing the packages in locations other than .lake/. I also would love to hear if someone finds a solution for having the packages in the Nix store.

I'm using a flake.nix that allows me to spawn a nix develop environment with all the tooling ready, but I don't do nix build. My example is at https://github.com/provables/special-numbers.

[Agnishom Chattopadhyay]

Thanks for sharing the example!

[Agnishom Chattopadhyay]

I am not sure I understand why Step 3 should require starting from scratch. However, it is not important that it runs lake build exactly. I just want the nix build command to check the proofs (i.e, run the typechecker and do the compilation)