chore: bump Lean toolchain to v4.32.2 - #12
Open
kim-em wants to merge 1 commit into
Open
Conversation
Follow lean4lean master, which moved to v4.32.2 in digama0/lean4lean#30, and move mathlib to its matching v4.32.2 tag. No source change was needed: `lake build` reports only the three pre-existing `sorry`s (two in upstream `Lean4Lean/Theory/Inductive.lean`, one in `consistency`). Requiring mathlib last is what keeps `lake exe cache get` working. lean4lean and mathlib both pull in batteries, and at v4.32.2 they no longer agree: lean4lean asks for the `v4.32.2` tag while mathlib pins `023ce7d`, which the tag only adds a `lean-toolchain` bump and a docs lakefile change on top of. Mathlib's olean cache is keyed on its dependency sources, so resolving batteries to the tag makes the cache lookup miss and mathlib build from source. The later require wins, so mathlib goes last; the comment in the lakefile said the opposite and has been corrected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017x8crJD7VZZZohyfeoHg1o
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
1 participant
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.
This PR bumps the toolchain to Lean
v4.32.2, following lean4lean master (which moved there in digama0/lean4lean#30, "chore: bump Lean toolchain to v4.32.2"), and moves mathlib to its matchingv4.32.2tag. No source change was needed:lake buildcompletes with only the three pre-existingsorrys, two in upstreamLean4Lean/Theory/Inductive.leanand one inconsistency.Requiring mathlib last is what keeps
lake exe cache getworking. lean4lean and mathlib both pull in batteries, and atv4.32.2they no longer agree: lean4lean asks for thev4.32.2tag, mathlib pins023ce7d, and the tag adds only alean-toolchainbump and a docs lakefile change on top of that commit. Mathlib's olean cache is keyed on its dependency sources, so resolving batteries to the tag makes the cache lookup miss and mathlib build from source. The later require wins, so mathlib now goes last; the comment in the lakefile claimed the first require wins and has been corrected.🤖 Prepared with Claude Code