Verify end-to-end against real Lean 4.30.0; fix installer and ELAN_HOME bugs#34
Merged
Conversation
…env bugs
environment.py:
- Split elan binary install from toolchain install
(--default-toolchain none) so a blocked toolchain download can't
fail the elan install.
- Add GitHub-release toolchain fallback for networks that block
release.lean-lang.org: resolve latest tag via the releases/latest
redirect, download the official zip, extract preserving Unix
permission bits (ZipFile.extractall drops the exec bit), register
via elan toolchain link + elan default.
sandbox.py:
- Fix real bug: elan proxies resolve toolchains via ELAN_HOME, so
PATH alone fails with app-isolated installs ('no default toolchain
configured'). New _elan_env() sets both; used by lake init and
run_lake_build.
tests/test_real_data_validation.py:
- Use the sandbox's discovery instead of hardcoding ~/.elan/bin so
the 9 Lean-gated tests run against the repo's own install.
Verified in this container: 323 passed, 0 skipped (was 314+9skip);
full report in VERIFICATION.md.
https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Proves the pipeline end-to-end against a real Lean 4.30.0 toolchain and fixes the bugs that were in the way. Full report in
VERIFICATION.md.environment.py: elan binary install decoupled from toolchain install; GitHub-release toolchain fallback for networks that blockrelease.lean-lang.org(resolves latest tag via the releases/latest redirect, downloads the official zip, extracts preserving Unix exec bits —ZipFile.extractalldrops them — and registers viaelan toolchain link).sandbox.pyreal bug: elan proxies resolve toolchains viaELAN_HOME, so PATH alone fails with the app-isolated install ("no default toolchain configured"). New_elan_env()sets both, used bylake initandrun_lake_build.tests/test_real_data_validation.py: uses the sandbox's own discovery instead of hardcoding~/.elan/bin, so the project's installer makes the project's tests run.Verification (executed, not inferred)
python -m src.environment --install→ Lean 4.30.0 via the GitHub fallback (826 MB).Part of the project-wide polish batch.
https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
Generated by Claude Code