chore: Update Lean to v4.34.1 - #654
Merged
Merged
Conversation
github-actions
Bot
force-pushed
the
update/lean-v4.34.1
branch
from
October 1, 2026 16:15
3fa04a7 to
d58a6f9
Compare
samuelburnham
force-pushed
the
update/lean-v4.34.1
branch
2 times, most recently
from
October 1, 2026 23:03
3962b62 to
e250a8d
Compare
samuelburnham
enabled auto-merge
October 1, 2026 23:04
samuelburnham
force-pushed
the
update/lean-v4.34.1
branch
from
October 2, 2026 13:29
e250a8d to
a96ab1a
Compare
Toolchain and dependencies bumped by lean-update.
lean-update leaves commit-pinned dependencies alone, so these three stayed on their v4.33.1 revisions. Move each to the head of its `main`, all of which now build on Lean v4.34.1; `lake update` on the three also carries plausible to v4.34.0 through LSpec's manifest. The compile benchmark inherits the same pins from the root package, so its manifest is brought in line by hand, as the Mathlib-sized `lake update` there is not worth running for inherited entries.
The toolchain deprecates `if_pos`, `if_neg`, `dif_pos`, `dif_neg`, `if_true`, `if_false` and `dif_eq_if` in favour of the `ite_*`/`dite_*` names. Each replacement has the same explicit arguments, so these are renames. The `Ix` library builds under `--wfail`, as does everything the build-all lint driver covers, so the warnings failed CI at `Ix.Lib`.
Lean v4.34 proves `Nat.le_iff_lt_add_one` and `Nat.pow_lt_pow_iff_right` classically, and `Std.DHashMap.Raw.WF` reaches them through its `emptyWithCapacity` proof. Every statement over `Ixon.Env`, `TcM` state or other hash-map-bearing types therefore depends on `Classical.choice` through the type alone, whatever its own proof does. The affected roots move to the `standard` allowance: 2 in the compile audit (`Catalog.ofEnv_finite`, `BlockWireTablesWF.of_preseed`) and 115 in the typechecker audit. Each manifest was evaluated in full against the new toolchain; the 5 and 62 roots that remain on the choice-free allowances verified as still choice-free, and no root changed in any other axiom.
The Nix build takes Blake3 from the `blake3-lean` flake input, whose URL pins a commit, rather than from the Lake manifest. The manifest moved to Blake3.lean's v4.34.1 revision but the input still named the v4.33.1 one, so inside the sandbox the test binary, built with v4.34.1, loaded a Blake3 olean produced by the older toolchain and failed on its incompatible header. The input now names the same commit as the manifest, and flake.lock follows.
`List.idxOf_cons` now unfolds to an `if x == y then ... else ...` rather than a `bif`, so the `rankOf_aux` membership case needs `Bool.false_eq_true` and `ite_false` in place of `cond_false`. `List.getElem_inj` moved to `List.Nodup.getElem_inj` with the `Nodup` hypothesis first; both call sites already pass it first.
Six primitives compile to new Ixon content addresses under the new toolchain: Nat.bitwise, Nat.land, Nat.lor, Nat.xor, String.back and String.Legacy.back. Their hardcoded addresses are updated everywhere they live — the Rust `PrimAddrs` table, its Lean mirror in `Ix/Tc/Primitive.lean`, the byte arrays the IxVM kernel reads in `Ix/IxVM/Kernel/NatPrim.lean` (five of the six; the kernel does not hardcode Nat.bitwise), and the checked-in generator record under `Tests/Fixtures/ixon-v4` — and the codegen'd kernel is regenerated with `lake exe ix codegen`. The values are the Ixon v4 addresses `lake exe ixon-v4-primitives` printed; `lake exe ix codegen --check` and `lake test -- primitive-address-parity` pass against them.
samuelburnham
force-pushed
the
update/lean-v4.34.1
branch
from
October 2, 2026 13:35
a96ab1a to
5f07f7c
Compare
Lean v4.34 proves `Std.DHashMap.Raw.WF` classically, so any statement over a hash-map-bearing type depends on `Classical.choice` through the type alone. Two `@[csimp]` roots in the exact-sharing search are of that kind: `searchComponents_eq_via` runs over `searchComponent`, whose state is a `Std.HashMap`, and `SCtx.phiE_eq_fast` is stated over `SCtx`, which carries a `Std.HashMap` field. Both move from `noChoice` to `standard`. Every choice-free root in the compile audit was re-evaluated against the new toolchain with `#print axioms`; the other 28 remain choice-free and no root changed in any other axiom.
arthurpaulino
previously approved these changes
Oct 2, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Oct 2, 2026
The new toolchain changes the bodies of several core definitions (Nat.land, Nat.lor, Nat.xor, String.back and their dependents), so the Ixon closures the IxVM kernel checks for those constants grow slightly and the exact proving-cost pins no longer hold. Twenty kernel-check pins in `kernelCheckEntries` and the shard-pipeline pin move to the values the merge-tests run and a local `lake test -- --ignored ixvm` both report; the remaining sixty-four pins are unchanged.
arthurpaulino
approved these changes
Oct 2, 2026
samuelburnham
enabled auto-merge
October 2, 2026 15:13
johnchandlerburnham
added a commit
that referenced
this pull request
Oct 2, 2026
…to ix-certified Brings in e328da2 (Lean v4.33.1 -> v4.34.1) and 209699b (.github/workflows/update-rust.yml). The branch was on Lean v4.34.0. Conflicts (200 files): - Ix/Tc/Verify/** (155 files): deleted on this branch (docs/kernel.md, removal ledger), edited on main (4.34.1 deprecation renames). Resolved as deleted; nothing ported. - Ix/Compile/Verify/** (33 files): deleted at the old path. Main's edits were checked against the relocated copies by a three-way merge (base = fork point, ours = relocated copy, theirs = main): * 25 files relocated under their own names (Ix/Sharing/Verify/{SharingExact, SharingExactCanon,Tiered*,Uniform*}.lean, Ix/Ixon/Verify/TagN.lean) already contain every hunk of main's: the same renames (if_pos -> ite_eq_left, if_neg -> ite_eq_right, if_true -> ite_true, if_false -> ite_false, dif_pos -> dite_eq_left, List.getElem_inj -> List.Nodup.getElem_inj). The three-way result differs from the relocated copy only in TieredTier.lean (2 lines) and UniformGain.lean (2 lines), where main still writes Ix.Compile.Verify.SharingExact.* for the relocated Ix.Sharing.Verify.SharingExact.* (namespace only). * Codec, ExprCodec, ExprSpineCodec, ConstantCodec, ConstantTablesCodec (preserved as Ix/Ixon/Verify/{Basic,Expr,ExprSpine,Constant, ConstantTables}), CompileSharingCodec (its builder part is Ix/Sharing/Verify/Builder.lean), CompileMutualCodec, CompilePreseed (retired): main's hunks are renames only; nothing to port. * Audit/Statements.lean: main moved four roots from noChoice to standard. searchComponents_eq_via and SCtx.phiE_eq_fast already carry standard in Ix/Sharing/Verify/Audit/Statements.lean; Catalog.ofEnv_finite and BlockWireTablesWF.of_preseed are retired roots. Nothing to port. - Toolchain files: lean-toolchain and Benchmarks/{Catalog/RelocFixtureA, Catalog/RelocFixtureB,Compile,Compile/TruthMines,TruthMines}/lean-toolchain set to leanprover/lean4:v4.34.1; IxKernel/ and Models/SetTheory/ lean-toolchain set to the same (CI compares the four). - lakefile.lean, lake-manifest.json, flake.nix, Benchmarks/Compile/ {lakefile.toml,lake-manifest.json}: the branch's files with main's 4.34.1 revisions: LSpec d8eb3e0d (descends from the branch's 369c09df), Blake3.lean 3f8b8056 (descends from the branch's c32002ee), Mathlib v4.34.1 (d13f23b7) in Benchmarks/Compile. Cli and batteries stay at v4.34.0 (as on main). The lean4lean (lean4ix) require, its manifest entries and its flake depOverride stay removed, as the branch retired them; main's bump of that pin is dropped. Main's 38-line change to the Benchmarks manifest is 19 revision bumps (no entries removed). - flake.lock: main's (lean4-nix e828640c, which descends from the branch's c8bce665 and adds v4.34.1; Blake3.lean 3f8b8056). The inputs are the same on both sides; `nix flake lock` on the merged tree leaves it unchanged. Semantic merge (files both sides changed without textual overlap): - primitives.tsv, prim_addrs.rs, Ix/Tc/Primitive.lean, Ix/IxVM/Kernel/ NatPrim.lean, aiur_ixvm.rs: both sides made identical edits (the same six rows: Nat.bitwise, Nat.land, Nat.lor, Nat.xor, String.back, String.Legacy.back), so 4.34.0 and 4.34.1 agree on every primitive address; confirmed by the tools on the merged tree. - Tests/Ix/Kernel/PrimeGapsReduction.lean: main replaced the deprecated Bool.and'/or'/not' with Bool.and/or/not; the branch kept the primed terms under `set_option linter.deprecated false`. Both merged cleanly into a file with unprimed terms under a now-false comment; took main's file. Nothing pins the primed terms (the original addresses are informational). - Ix/Lib.lean, Ix/Sharing/Exact/*: identical on both sides. Models/SetTheory: Mathlib rev v4.34.0 -> v4.34.1 (lakefile.toml), manifest refreshed by `lake -d Models/SetTheory update`.
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.
lean-toolchainand dependencies updated for Lean releasev4.34.1by lean-update.