search

lenianiva / lean4-nix

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

template using lake and mathlib4 #1

Closed 9glenda closed 1 week ago

9glenda commented 2 weeks ago

I think it would be useful to have a template using lake and mathlib4

lenianiva commented 2 weeks ago

For lake, do you just want it to be an executable in the devShell? Building a Lean package doesn't require lake.

For mathlib4, would it be a good idea to add it as a flake output? I don't use mathlib4 extensively in my projects. If the user demands a high degree of flexibility we could leave the management of mathlib to the user

9glenda commented 2 weeks ago

sorry my bad lake is already in the devShell. No need to add it.

mathlib4 can just be added to the flake inputs of the template. There's no point in manging mathlib for the user.

lenianiva commented 2 weeks ago

Building mathlib4 using a flake-like build (either in this repo's main flake or in an example) maybe tough. I can try it though.

I suspect this will take a tool like poetry2nix or crate2nix, and we would have to parse the manifest to find dependencies. buildLeanPackage does not automatically deduce these dependencies.

9glenda commented 2 weeks ago

I'm pretty new to lean. For me the whole dependency handeling is a bit confusing. A example/template would be really useful for people starting out with lean.

lenianiva commented 2 weeks ago

I'm pretty new to lean. For me the whole dependency handeling is a bit confusing. A example/template would be really useful for people starting out with lean.

I have an example here of using LSpec with a Lean library and executable: https://git.leni.sh/aniva/Pantograph/src/commit/23efed960b890ad2c8bc8e87ad30c6f539e05c40/flake.nix

There is currently no machinery for converting Lean dependencies in lake-manifest.json into Nix build paths, so supporting a dependency tree like Mathlib will require more work

lenianiva commented 1 week ago

It is done: https://github.com/lenianiva/lean4-nix/tree/main/templates/dependency

The example uses aesop, which has a secondary dependency Batteries.

I didn't use Mathlib as an example since it takes at least 30 min to build. Give it a shot.

9glenda commented 1 week ago

Thanks, lake2nix makes using lean/lake on nixos so much easier!

I don't think the template has to include mathlib. It's pretty clear how to add new dependencies.

The template works as expected.