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>
vasnesterov
pushed a commit
to vasnesterov/lean4lean
that referenced
this pull request
Aug 23, 2026
…d a guard class the audit missed **The systemic finding: a guard class §6/§7.1 did not account for.** Every `@[extern]` C entry point in scope that takes a `Nat` begins with a **`lean_is_scalar` bignum test -- before** the range test the audit records. `LEAN_MAX_SMALL_NAT = SIZE_MAX >> 1`, so it fires at `2^63`. §6 describes `lean_expr_instantiate_range` as "starts with `if (b > e || e > sz) lean_internal_panic`" -- that is the function's **second** statement, not its first. **Seven axioms in scope sit on that guard**, and it resolves four different ways. ## #21 `Lean.Expr.liftLooseBVars_eq` is FALSE if (!lean_is_scalar(s) || !lean_is_scalar(d)) { lean_inc(e); return e; } Witness `e := .bvar 0`, `s := 0`, `d := 2^63`. Both halves machine-checked, deliberately **by different instruments**: - C side, differential test on compiled code: `#eval idx ((Expr.bvar 0).liftLooseBVars 0 (2^63))` prints `"bvar 0"`. - Model side, kernel reduction: `liftLooseBVars' (.bvar 0) 0 (2^63) = .bvar (2^63)`, and `≠ .bvar 0`. So the axiom asserts `.bvar 0 = .bvar (2^63)`. Worse than #26/digama0#27 in one specific way: **the call completes.** No panic, no exotic input -- `2^63` is an ordinary literal and `.bvar 0` an ordinary `Expr`. Only the *model's* output is not runtime-constructible, which is why the two sides cannot be evaluated in one expression (`#eval` of the model's answer trips `lean_expr_mk_data`'s own panic -- observed). **Not an inconsistency**: `liftLooseBVars` is `opaque @[extern]` and the toolchain has no core theorem about it, so there is no second fact to contradict. Same category as #12/#17. Fix is `d < 2^63` or a `USize` restatement -- frozen file, needs sign-off. ## Three failed attacks, recorded as failed attacks - **#22, digama0#30** carry the same guard and **survive**: the C fallback coincides with the model on every input a real `Expr` can supply, with machine-checked agreement lemmas for both. One of the stream's own witnesses was wrong -- `(.bvar 7).lowerLooseBVars (2^63) 1` returns `bvar 7` from *both* sides -- and the correction is recorded rather than quietly dropped. - **digama0#29 `abstractRange_eq`**, the only unconditional range axiom, also survives: its fallback uses `lean_array_size` and `Array.extract 0 n` clamps to the same thing, agreeing at **every** input, logical or not. Verdict unchanged, for a reason §7.1 did not state. ## #26/digama0#27: the side condition is necessary but NOT sufficient `start ≤ stop ≤ subst.size` excludes the second guard, not the first -- `stop` may be non-scalar provided `subst.size` is too, which needs `subst.size ≥ 2^63`: expressible, not constructible. Strictly weaker than #21, no differential test possible. **Source reading only, and marked as such.** ## The two other priority targets, answered - **#17 `Expr.mkData_eq` -- no analogous consequence.** `lean_expr_mk_data` panics twice, and its hypothesis implies **both** are passed; the `approxDepth` clamp matches too. Unlike #12, correctly guarded. - **#3 `PersistentArray.toList'_push` -- hypothesis adequate**, in the strongest available sense: `WF` is generated by `empty`/`push` only, and a reverse scan shows lean4lean uses **no other `PersistentArray` operation**. So `WF` is exactly the reachable set, not an approximation. Not reached: #4-#7. **digama0#31's dependency on #15 deliberately not pursued** -- #15 belongs to another stream's section, and a cross-section attack run from one side only is the weaker version of the test. **No `False` was derived.** §11.9 keeps the evidence strengths separate: differential-test-plus-source, source-only, and proof are three different things, and none of this is a proof. Co-Authored-By: Claude Opus 5 (1M context) <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