search

lenianiva / lean4-nix

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

Extract test and default targets from `lakefile.lean` #21

Open lenianiva opened 3 weeks ago

lenianiva commented 3 weeks ago

Is it possible to do this?

lenianiva commented 1 week ago

I read the source code of Lake a bit more. If we want to do this we may have to call functions in Lake.