Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: use lean4 from nixpkgs #35

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

Conversation

stepbrobd
Copy link
Contributor

closes #11

WIP

  • pass lib (builtins + nixpkgs.lib) from flake.nix to overlay.nix
  • auto import all files in ./manifests
  • attempt to use nixpkgs' lean4 package definition

@stepbrobd
Copy link
Contributor Author

stepbrobd commented Jan 25, 2025

couple problems found during the process

  • most of the attributes exported from manifests are not used at all
  • libraries (Init Std Lean Lake) are already included package, need to find a way to re-expose them
  • if locked nixpkgs version is too outdated, build might fail, user level override may be needed
  • bootstrapped manifests all have IFD, eval time is unbearably slow

@lenianiva
Copy link
Owner

Does this mean every future Lean version will have a ${version}.nix and ${version}-bin.nix in the manifest?

@stepbrobd
Copy link
Contributor Author

we can do that or just add a bootstrap-bin or whatever function inside ${version}.nix

ideally -bin variants should only depend on tag and rev

@lenianiva
Copy link
Owner

we can do that or just add a bootstrap-bin or whatever function inside ${version}.nix

ideally -bin variants should only depend on tag and rev

What's the point of doing this when you have to build the entire Lean binary anyways

@stepbrobd
Copy link
Contributor Author

i was thinking of implementing this by overriding pkgs.lean4 so we can reuse the nixpkgs binary cache

apparently it won't work unless we pin multiple versions of nixpkgs in flake inputs

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Fetch lean binary
2 participants