search

lenianiva / lean4-nix

Nix overlay for Lean 4, and lake2nix
Apache License 2.0
16 stars 2 forks source link

Fetch lean binary #11

Open lenianiva opened 4 weeks ago

lenianiva commented 4 weeks ago

Can we replace the lean dependency with a binary like what rust-overlay does? This would allow us to abridge the stage 1 build and remove all the bootstrapping.

One problem I could think of is it would not expose with pkgs.lean; [ Init Std Lean ]

lenianiva commented 2 weeks ago

I looked a bit into buildLeanPackage.nix's source code, and I think this is definitely doable.

We need to feed the lean binary executable into this function, which could be done by extracting files from the tar/zip files from https://github.com/leanprover/lean4/releases/tag/v4.13.0

lenianiva commented 1 week ago

Building from source seems to be the preferred method. If we get more users I can contact cachix