chore: Update Lean to v4.33.1 - #6
Merged
Merged
Conversation
v4.33.1 is a kernel release, so this is more than a toolchain bump. Five of its six kernel changes are mirrored here; the sixth was already satisfied. - lean4#14582: `Environment.addInductive` runs `checkUniformIndOccs` before nested-inductive elimination, rejecting occurrences of a datatype being declared that are not applied to the declaration's parameters and universe levels. Occurrences erased by a later `whnf`, and permuted universe levels, are now rejected where they were previously accepted. - lean4#14806: replace the union-find `EquivManager` positive cache with a hash-ordered pair set (`succeededBefore`/`cacheSuccess`), so `isDefEq` no longer depends on the order pairs were checked in. `isDefEq` is a sound but incomplete semi-decision procedure and so is not transitive; closing over its successes made results order-dependent. `Lean4Lean/EquivManager.lean` and `Lean4Lean/Verify/EquivManager.lean` are deleted, and the cache invariant is now `DefEqCache.WF` in `Verify/TypeChecker/Basic.lean`. This also drops `ptrEqExpr_eq` from the axiom dependencies of every `#print axioms` guard that reached it through `quickIsDefEq`. - lean4#14807: no change needed. `isProp` already routed through `ensureSortCore`, so this fork never had the bug upstream fixed. - lean4#14808: `AddInductive.checkRecursors` type-checks each generated recursor and verifies that each computation rule is type-preserving. - lean4#14843: `toCtorWhenStruct` takes a sort-ensuring `isNeverProp` callback rather than matching on `whnf (inferType eType)` with an `unreachable!` fallback, so a non-sort type raises a kernel error. The deliberate `isNeverZero`/`!isAlwaysZero` divergence is preserved. - lean4#14849: bound `Nat` numeral size via a new `FuelConfig.natMaxSize` (default 128 MB, matching `LEAN_NAT_MAX_SIZE`). Literals entering the kernel and the numerals `reduceNat` computes are checked; `reducePow` and the new `reduceShiftLeft` bound their results before forming them, replacing the old `reducePowMaxExp` exponent cap. Batteries stays pinned at v4.33.0: no patch release was cut for v4.33.1, and those sources build unchanged under the new toolchain. Tests: `Tests/UniformIndOccs.lean` ports upstream's `tests/elab/issue_14576_nonuniform.lean` (five rejections, three acceptances) plus the mutual defeq-parameter case from `tests/elab/inductiveDefeqParams.lean`. `Tests/NestedInductive.lean` gains `badUniformDecl`, whose ill-typed dropped parameter sits beside a uniform occurrence so the uniformity check cannot preempt the nested-parameter check it is testing. Docs: ledger entries D018 (toolchain) and D021 (the kernel mirroring), plus fixes to two stale claims in `divergences.md` — `addMutual` described lean4#14608/#14632 as unreleased though they landed in v4.33.0-rc2, and the `restoreNested` entry said lean4lean retains lean4#14621, which it does not. Sorry frontier unchanged at 22.
Runs `argumentcomputer/lean-update` daily against `dev`, opening an
`update/lean-{release}` PR whether or not the build passes, so an incompatible
release surfaces as a failing PR to review rather than silently not appearing.
`pinned-tags` bump mode suits this package: batteries is pinned to a Lean
version tag rather than tracking a branch, so its `rev` moves with the
toolchain. Only the Lean half is automated -- `flake.nix` resolves the
toolchain through lean4-nix's vendored release table, which lags a release, so
bumping the `lean4-nix` input stays a manual follow-up on the update PR.
Requires the TOKEN_APP_ID and TOKEN_APP_PRIVATE_KEY secrets already used by
repo-sync.yml; pushes made with GITHUB_TOKEN would not trigger CI.
johnchandlerburnham
approved these changes
Aug 22, 2026
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.
No description provided.