Fetch lean binary

[lenianiva]

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]

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]

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

[RossSmyth]

Why is it the preferred method? It takes forever.

[lenianiva]

Why is it the preferred method? It takes forever.

Because it builds from source and that is preferred. If you use a cache it won't take forever. I need to setup cachix

[RossSmyth]

Again I ask, why is that preferred? Currently it isn't even a preference, you must build from source every flake.lock update. I would generally prefer to use released versions so that collaboration is easier with others, even if there is a cache.

[lenianiva]

Again I ask, why is that preferred? Currently it isn't even a preference, you must build from source every flake.lock update. I would generally prefer to use released versions so that collaboration is easier with others, even if there is a cache.

because it reduces reliance and trust on the source of the binary

Another benefit of using Nix build is that we get access to buildLeanPackage for no cost.