chore: Update Lean to v4.33.0 - #554
Open
argument-ci-bot[bot] wants to merge 9 commits into
Open
Conversation
Toolchain and dependencies bumped by lean-update.
`pr: true` opens the update PR on any outcome and skips the updater's validation build by default; the PR's own CI is the authority on whether the update builds.
Carries the v4.31 adaptation work forward: Std.HashMap `find?` renames to `get?` (including call sites added on main since), the ByteArray FFI helpers removed on the Lean and Rust sides, and assorted API fixes. Dependency pins move to v4.33.0: Cli and batteries by tag, LSpec to the merge commit of its v4.33.0 bump, and Blake3 to its v4.33.0 bump commit — the manifest entry for Blake3 still needs `lake update Blake3` once that commit is reachable on the remote. Benchmarks/Compile moves to the v4.33.0 toolchain with mathlib and FLT at their v4.33.0 tags.
Upstream lean4-nix stops at Lean v4.32.0 and builds toolchains from source
behind an overlay; the fork provides released toolchains as plain
derivations and removed the overlay API. The overlay block is replaced by
`lib.${system}.fromToolchainFile`, and the Lean sysroot for bindgen, the
Lake build inputs, the binary wrappers, and the dev shell take the
toolchain derivation directly.
The dev shell and the crane-side derivations evaluate now. The Lake
packages remain blocked on the `blake3-lean` input: it follows this flake's
lean4-nix, so Blake3.lean's own fork migration must be pushed and merged,
after which `nix flake update blake3-lean` and `lake update Blake3`
complete the move.
Formatting-only, plus the formatter declaration itself; nixfmt-tree wraps nixfmt so `nix fmt .` can still take a directory.
Lean v4.33.0 fixed two kernel soundness bugs (leanprover/lean4#14613, leanprover/lean4#14615) where a sort spelled e.g. `Sort (imax 1 0)` was not recognized as `Prop` because the zero test was syntactic; a non-proof field could then be projected out of a proof, and the inductive checker could misclassify Prop-only elimination and K-like reduction. Both ix kernels had the same syntactic test. `KUniv.isSemanticZero` / `KUniv::is_semantic_zero` decide `u ≡ 0` through the existing Géran normal form (zero normalizes to empty entries only, and norm-level equality already ignores empty entries), and replace the syntactic test at the four affected sites, in lockstep across both kernels: - proof-irrelevance Prop classification (Tc/DefEq, kernel/def_eq) - the struct-eta H3 Prop-major guard (Tc/Whnf, kernel/whnf) - the A4 field-universe Prop exemption (Tc/Inductive, kernel/inductive) - recursor-generation isProp/isLarge (AuxGen/Recursor; compile-side, Lean only) The IxVM kernel model retains the syntactic test and needs the same treatment separately.
Fallout of the v4.29 -> v4.33 bump that the skipped updater validation never surfaced: - batteries retired the `Batteries.Data.RBMap` umbrella module and moved the type to `RBTree.RBMap` in `Batteries.Recycling.RBTree`; ix keeps the recycled structure (the Verify layer proves theorems about it) rather than migrating `NormLevel`/`CNorm` to `Std.TreeMap`. - Two `groups`/`atoms` lookups in IxonUniv were RBMap sites caught in the earlier `Std.HashMap` `find?` -> `get?` rename; RBMap kept `find?`. - `do match` arms are non-dependent since v4.32 (leanprover/lean4#13305); the ShardMap size-invariant proofs need `match (dependent := true)`. - `Environment.addDeclCore` gained a `maxRecDepth` parameter (leanprover/lean4#13956); pass Lean's default. - The Canonicity alias fixtures need `@[expose]` under the module system's cross-module compilation-type check.
`Lean.Int` is in the compiler's `builtinRuntimeTypes`, so at runtime it shares `Nat`'s representation — a tagged scalar or a GMP mpz object; `Int.ofNat` compiles to the identity `lean_nat_to_int` and no ctor cell ever exists. The mdata `DataValue.ofInt` decode path nevertheless read it through the `LeanIxInt` ctor layout, dereferencing a tagged scalar (or reading mpz limbs as ctor fields) whenever an `Expr.mdata` KVMap carried an integer. Decode by value instead: arithmetic-shift the tagged scalar to recover the signed payload, and for mpz objects take the sign from `lean_int_dec_lt` and the magnitude from `lean_nat_abs`. `LeanIxInt` remains in use for `Ix.Int`, a genuine two-ctor inductive. Pre-existing bug surfaced by the v4.33 FFI layout audit, which found no other divergence between the hardcoded layouts and Lean v4.33.0.
Records the lean4lean integration steps and their verification queue, the open kernel-semantics divergences from upstream (theorem opacity, the IxVM syntactic zero test, the deliberately-unenforced mutual universe uniformity, missing regression fixtures), the divergences considered and cleared during the audit, and the non-blocking follow-ups (FFI pointer liveness, benchmark re-baselining, thread-pool stack ordering, OpenSSL link watch, setup-file JSON parsing).
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.
lean-toolchainand dependencies updated for Lean releasev4.33.0by lean-update.