Bump Lean toolchain to v4.31.0 - #29
Merged
Merged
Conversation
The v4.30.0..v4.31.0 src/kernel diff has no semantic changes: it fixes one comment typo and adds noexcept to the type_checker move constructor declaration and definition. Rename the non-portable Variable! module and make simplifier-dependent proofs explicit for Lean 4.31. Refresh the versioned Lean.Level divergence link. Validated with lake build and both CI replay commands.
kim-em
force-pushed
the
agent/bump-v4.31.0
branch
from
August 3, 2026 02:56
ae29fbf to
af60c9a
Compare
digama0
marked this pull request as ready for review
August 3, 2026 04:06
digama0
added a commit
that referenced
this pull request
Aug 3, 2026
`Experimental` is not a default target, so nothing built it. Two rounds of breakage had accumulated unnoticed: * `7842f38` moved the `Std.Basic` prelude into `namespace Lean4Lean`, which makes `List.Forall₂.imp` and friends resolvable only under an explicit `open Lean4Lean` -- the enclosing namespace does not count for generalized field notation. Every `Theory`/`Verify` file got that `open`; the `Experimental` files did not, so eight call sites across five files stopped resolving. This already failed on v4.30.0. * The v4.31.0 bump then broke eight more proofs, all cases of `simp` no longer unfolding a definition on its own: `VExpr.instL`/`VLevel.inst` in `Stronger.IsDefEqStrong.instL` (the same fix #29 applied to the `Theory` copy in `Strong.lean`), plus `HasTypePi`, `Pattern.WF`, `Nat` associativity and a `Sigma` eta step in `ShapeLogRel`. `WShape.ctor'_join` was separately relying on a `by_contra` that does not elaborate here (also already broken on v4.30.0); it is now `Classical.not_imp`, which is core and needs no tactic import. `SoundEq.rfl` is marked `protected` so that a bare `rfl` in that namespace still means `Eq.refl`. No statement changes and no new `sorry`s -- every edit is an `open`, a `simp` hint, a `protected` marker, or a term-mode replacement for a tactic that no longer applies. `lake build Lean4Lean.Experimental` is now a CI step so this cannot rot silently again. Co-Authored-By: Claude Opus 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
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.
Updates Lean and Batteries to v4.31.0.
Lean kernel changes
The direct
v4.30.0..v4.31.0diff undersrc/kernelcontains only three non-semantic edits:declaration.h(declationstodeclarations)noexcepton thetype_checkermove constructor declarationnoexcepton its definitionThere are therefore no trusted type-checking or reduction changes to mirror in lean4lean.
Compatibility updates
Lean 4.31 rejects non-portable module names, so
Lean4Lean.Std.Variable!is renamed toLean4Lean.Std.VariableBang. A handful of proofs also now require explicit unfolding or simplification hints where Lean 4.30's simplifier reduced the expressions automatically; their statements and proof strategy are unchanged.The versioned
Lean.Levelsource link indivergences.mdis also refreshed to v4.31.0.Validation
lake build(146 jobs)lake exe lean4lean Init.Core(1,036 declarations)lake exe lean4lean --fresh Init.System.IO(43,602 declarations)🤖 prepared with assistance from Codex