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

fix: invoke elan explicitly #14

Merged
merged 5 commits into from
Apr 19, 2024

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Apr 17, 2024

Instead of trying to find the location of elan-disguised-as-lake, this now invokes elan
plainly, using elan run --install <toolchain>.

This fixes building a multi-toolchain verso project on my setup (where elan comes from nix, but it should not matter where elan comes from, only that the lake in path is from elan).

Fixes #4

@nomeata nomeata changed the title fix: simply use lake from PATH, avoid cleverness fix: invoke elan explicitly Apr 17, 2024
@david-christiansen
Copy link
Collaborator

This sounds like a real improvement - thanks!

I want to stick a bit more CI on this (to validate that it at least works for Homebrew installs on Mac as well as the curl | bash install method), then merge.

@david-christiansen david-christiansen merged commit 60b5dbc into leanprover:main Apr 19, 2024
6 checks passed
@david-christiansen
Copy link
Collaborator

Thanks again - the improved CI validates that this is a good approach. It's simpler, and it even actually works!

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.

Can't find lake when elan comes from Homebrew
2 participants