Bump toolchain to Lean v4.30.0 (final) and Mathlib v4.30.0 - #9
Merged
Conversation
Matches the same fix in ironwood's copy of this file. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Update the CompPoly pin to its last commit on Lean v4.30.0 (d458e5cebd364b15660ff8de20ec964dcd52c120, before its v4.31 bump), which transitively pins Mathlib at the v4.30.0 tag, keeping the toolchain and Mathlib revision agreed between the two. The toolchain moves from v4.30.0-rc2 to the v4.30.0 release. No source changes were needed; the full build is clean. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
daira
marked this pull request as ready for review
July 20, 2026 11:51
mitschabaude-bot
added a commit
to mitschabaude-bot/ironwood
that referenced
this pull request
Jul 20, 2026
CompElliptic's own v4.30.0-final bump; brings CompPoly d458e5c via its manifest. Both default targets build clean.
mitschabaude-bot
added a commit
to Verified-zkEVM/clean
that referenced
this pull request
Jul 20, 2026
CompElliptic's own bump to Lean/mathlib v4.30.0 final — the same rev the zcash/ironwood toolchain PR now pins; brings CompPoly d458e5c. Clean and CleanTests build clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Bumps the toolchain from
v4.30.0-rc2to the finalv4.30.0release, consistent with zcash/ironwood#69.Changes:
lean-toolchain:leanprover/lean4:v4.30.0-rc2→leanprover/lean4:v4.30.0lakefile.lean: CompPoly pin84fc00c2→d458e5cebd364b15660ff8de20ec964dcd52c120— CompPoly's last commit on Lean v4.30.0, before its v4.31 bump. Unlike ironwood, no direct Mathlib require is needed: CompPoly at this revision transitively pins Mathlib at thev4.30.0tag, preserving this repo's arrangement where the two always agree on the toolchain and Mathlib revision.lake-manifest.json: regenerated (lake update); Mathlib resolves tov4.30.0(c5ea0035) and the shared transitive dependencies (aesop, Qq, Cli) to theirv4.30.0tags.No source changes were needed: the full build (1985 jobs, including
CompElliptic.TrustBoundarywith itsassert_axioms/assert_computablechecks) is clean on the final toolchain, verified locally with the Mathlib cache.Also folds in the pending docs commit
8d607ab(ASCII ellipsis in theassert_axiomsdocstring).A check of the Lean v4.31.0 release notes and of Mathlib commits to the elliptic-curve area in the v4.30.0→v4.31.0 window found no kernel-soundness or statement-correctness fixes that would argue for overshooting to v4.31.0; staying on v4.30.0 keeps the toolchain aligned with ironwood and Clean.
🤖 Claude Fable 5