From 18e88a4c5c13310642a3de115b265a21b8011e08 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:30:18 +0000 Subject: [PATCH] chore(toolchain): pin the patched Lean v4.34.1 CodeRabbit review on #36 (Major, security): v4.34.1 is the patched release of the 4.34 line. Checked against leanprover/lean4 itself: v4.34.0..v4.34.1 adds three runtime reference-count fixes (leanprover/lean4#15241, #15288, #15307), a BitVec backport and release preparation. marches checks only its own proofs, so the practical risk was low; the patch keeps the soundness floor on the patched build. lean-toolchain, README's two version mentions, and a STATE entry. Gates (v4.34.1): lake build -> Build completed successfully (15 jobs); grep -rnw sorry empty; #eval orbit unchanged. Rung: 3 (housekeeping; rung stays OPEN) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- README.adoc | 4 ++-- STATE.adoc | 16 ++++++++++++++++ lean-toolchain | 2 +- 3 files changed, 19 insertions(+), 3 deletions(-) diff --git a/README.adoc b/README.adoc index 469d5ef..c45c26f 100644 --- a/README.adoc +++ b/README.adoc @@ -14,7 +14,7 @@ object*: region-crossing well-formedness is a typing judgment on traces (`Marches.Trace`), and ill-typed crossings are *unconstructible* — they have no derivation — rather than detected and filtered. -Machine-checked, in this repository, by `lake build` (Lean 4, v4.34.0, +Machine-checked, in this repository, by `lake build` (Lean 4, v4.34.1, no dependencies): * Every well-typed non-empty cross-region trace strictly worsens @@ -164,7 +164,7 @@ artifact for PROVEN rows. No fabricated identifiers. [source,shell] ---- -elan default leanprover/lean4:v4.34.0 # or let lake read lean-toolchain +elan default leanprover/lean4:v4.34.1 # or let lake read lean-toolchain lake build ---- diff --git a/STATE.adoc b/STATE.adoc index 5a18bb3..592ca9e 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,21 @@ = STATE — cross-session log +== 2026-10-14 — toolchain v4.34.0 → v4.34.1 (patch; review finding on #36) + +* CodeRabbit flagged #36 (Major, security): v4.34.1 is the patched + release of the 4.34 line. Verified against leanprover/lean4 rather than + the bot's summary: `v4.34.0..v4.34.1` adds three runtime + reference-count fixes (#15241 sticky counts in deletion cascades, + #15288 children of overflowed objects, #15307 panic instead of + wrapping in `sharecommon_quick_fn`), a `BitVec.ofNatClamp` backport + and release preparation. marches checks only its own proofs, so the + practical risk was low. Taking the patch keeps the soundness floor on + the patched build at no cost. +* Gates on v4.34.1: `lake build` → `Build completed successfully (15 jobs).`; + `grep -rnw sorry Marches/ Marches.lean` empty; `#eval orbit` unchanged + (`[(false, false), (true, true), (false, false), (true, true)]`). The + v4.34.0 results below are now historical. + == 2026-10-14 — toolchain moved to v4.34.0 before rung 3 (Claude Code session) * Maintainer decision (MRC-01 open question): move `lean-toolchain` from diff --git a/lean-toolchain b/lean-toolchain index 12359f9..ba8ebf2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.34.1