upgrade lean 4.32 rc1#1
Merged
Merged
Conversation
cameronfreer
commented
Jun 27, 2026
cameronfreer
commented
Owner
- build: upgrade to Lean v4.32.0-rc1 + mathlib v4.32.0-rc1; drop LeanArchitect fork
- build: #upgrade — repair Graphon/Lovasz.lean for Lean v4.32.0-rc1 / mathlib v4.32.0-rc1
- build: #upgrade — repair SimpleRank + CycleKrylov for Lean v4.32.0-rc1
- build: #upgrade — repair core analysis chain for Lean v4.32.0-rc1
- build: #upgrade — repair MatrixDetermination for Lean v4.32.0-rc1
- build: #upgrade — repair InverseCounting for Lean v4.32.0-rc1
- build: #upgrade — deprecation sweep (warning-clean on Lean v4.32.0-rc1)
…chitect fork Dependency bump only (Commit 1 of the upgrade; API fixes follow separately). - lean-toolchain: v4.27.0 -> v4.32.0-rc1. - mathlib: d557daf (v4.27.0-era) -> v4.32.0-rc1. - LeanArchitect: cameronfreer fork (e14a867) -> upstream hanwenzhu d9013cc (v4.32.0-rc1). The fork's sole change was commenting out an explicit batteries pin to dodge a version conflict; at v4.32.0-rc1 upstream LeanArchitect, mathlib, and batteries all resolve to the same batteries commit (954dbc987), so the fork is no longer needed. - Dropped graphon's explicit batteries/Cli requires (Lake warned they break cache-hash computation); they now come transitively from Mathlib. Moved 'require mathlib' LAST so Mathlib's transitive dependency versions take precedence. - lake update + lake exe cache get succeed (8563 mathlib oleans cached); lake env lean reports v4.32.0-rc1. checkdecls left at its old pin (only used by the CI blueprint step, not the build).
…athlib v4.32.0-rc1 API-fix pass (proof bodies only; no statement changes; pre-existing sorries preserved). v4.32 mathlib changes handled: - SimpleGraph structure: symm/loopless fields are now Std.Symm/Std.Irrefl classes. Inline builds use nested-field syntax (symm.symm := …, loopless.irrefl := …); accesses use G.loopless.irrefl / G.irrefl / G.ne_of_adj. - Sym2.mk is now curried (α → α → Sym2 α); Sym2.mk (Quot.out e) reworked via s(p.1, p.2) + Sym2.eq_iff; Sym2.map_pair_eq → Sym2.map_mk. - SimpleGraph.map Adj now carries a Ne component (Ne ⊓ Relation.Map); membership goals go through SimpleGraph.map_adj. - empty 'simp only' now errors (removed); a few convert-leftover goals closed with funext+simp; edgeFinset_bot instance-mismatch worked around with explicit Fintype. lake build Graphon.Lovasz: 0 errors. Sorry inventory unchanged (one incidental docstring reword near a repaired proof).
API-fix pass (proof bodies only; no statement changes; sorries identical to baseline). - SimpleGraph inline builds (rootAttach, k23Arms, k2kArmsStructured): symm/loopless fields → nested-field syntax symm.symm / loopless.irrefl; .symm adjacency access → G.adj_symm / h.symm; G.loopless _ h → G.irrefl h. - Sym2: out_pair_eq / out_pair_eq' reworked off the curried Sym2.mk (s(p.1,p.2) + Sym2.eq_iff instead of Quot.out_eq + Sym2.mk_eq_mk_iff); Sym2.map_pair_eq → Sym2.map_mk. - convert depth/Pi-add residuals closed with ext+simp. #70 rank framework survives the upgrade (verified via #print axioms): multiEvalSubmodule_eq_orbitInvariantSubmodule — clean [propext, choice, Quot.sound] finrank_orbitInvariantSubmodule — clean vertexOrbitRel_of_rootedProfileEquiv — sorryAx via the one intentional residue only. lake build Graphon.CycleKrylov: 0 errors.
Basic, Step, HomDensity, CutNorm, Pullback, CutDistance, Approximation, Regularity, Compactness, Counting + leaves (Operator, Sampling, Operations) — all 0 errors. Proof bodies only; sorries identical to baseline. v4.32 API changes handled: - Measure.prod is now noncomputable ⟹ FORCED 'noncomputable' modifier on defs that build through it: Graphon.zero/one/compl, SignedGraphon.sub (Basic), SymmKernel.pullback, Graphon.pullback (Pullback). Modifier-only; no type/statement change. - Sym2.mk curried (HomDensity): Sym2.mk (Quot.out e) → s((out e).1,(out e).2). - empty 'simp only' now errors (Regularity, Compactness): removed / replaced with the follow-up tactic that already closed the goal. - zero_le is now a 0-ary proposition, not zero_le _ (Regularity). - Summable goal: convert+ext → Summable.congr (Compactness).
The heavy file (103 errors). Proof bodies only; no statement changes; sorries identical to baseline (incl. the frozen-motif and Lovász-infrastructure sorries). v4.32 API changes handled: - ~64 inline SimpleGraph builds / Sym2 sites: symm/loopless → Std.Symm/Std.Irrefl nested-field syntax; Sym2.map_pair_eq → Sym2.map_mk; curried Sym2.mk reworks. - Equiv.Perm inverse: π⁻¹ vs .symm — bridged with Equiv.Perm.inv_def so Equiv.apply_symm_apply / Equiv.symm_apply_apply fire again. lake build Graphon.MatrixDetermination: 0 errors.
Proof bodies only; no statement changes; sorries identical to baseline. - zero_le is now 0-ary: zero_le _ -> zero_le (7 sites). - ENNReal.toReal_eq_toReal -> ENNReal.toReal_eq_toReal_iff'. - ENNReal.toReal_prod now takes explicit (s) (f): toReal_prod -> toReal_prod _ _. (Convergence needed no changes once InverseCounting was green.)
Pure mathlib deprecated-alias renames (proof bodies only; no statement changes; sorry inventory identical to baseline at 136; #70 framework axioms unchanged): - Sym2.map_pair_eq → Sym2.map_mk (101 sites) - push_neg tactic → push Not (~75 sites) - Set diff→sdiff family: diff_subset/mem_diff(_of_mem)/union_diff_cancel/diff_eq_empty/ diff_empty/compl_diff/inter_union_diff/diff_diff_cancel_left/diff_union_self → sdiff_* (both Set.-qualified and unqualified open forms) - MeasureTheory.measure_diff → measure_sdiff, measure_inter_add_diff → measure_inter_add_sdiff, integral_finset_sum → integral_finsetSum - tendsto_finset_prod/sum → tendsto_finsetProd/Sum - Sym2.mem_diagSet_iff_isDiag → Sym2.mem_diagSet - Fin.coe_castSucc → Fin.val_castSucc, Fin.coe_cast → Fin.val_cast, Fin.lt_iff_val_lt_val → Fin.lt_def - _root_.not_imp → Classical.not_imp - import Mathlib.Data.Real.Sqrt → Mathlib.Analysis.Real.Sqrt lake build: 0 errors, 0 deprecation warnings.
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.