setting up a project with nix

Stream: lean4

[MangoIV]

Has there been some work in nix support for lean4? I'm asking because I know some people who joined the lean FRO are nix enthusiasts and I would like to know what the current "preferred way" of setting up, building, and running a lean4 project with nix is.

Thanks in advance.

[Joachim Breitner]

There is a lean setup in the lean repo, and at some point it was even meant to be a viable even for interactive use on lean project. But I think nobody is using it (not even the people who created it ), and it does not seem viable to keep it running. The best I can hope for at the moment is that we maintain the ability to build lean itself using nix for now, and then on top maybe have a lake wrapping setup (maybe with a lake vendor command and including the vendor hash in the nix derivation, like for rust) for building lean programs in nix.

For actually developing with lean, using nix will not help you much. Just get elan (e.g. from nixpkgs, that’s fine), and then use that to get lake, and use that for developing.

[MangoIV]

alright, I was fearing something like that; I guess having lake as the frontend to all package builds is kinda a choice contrary to nix (I think we talked about that)

I guess providing some tools in a devShell is fine..

[Joachim Breitner]

Yes, for hacking _on_ lean I use the nix-shell there, which pulls in the right LLVM etc.

[Joachim Breitner]

And for loogle, the devShell pulls in mostly elan:
https://github.com/nomeata/loogle/blob/master/flake.nix#L190-L197