Skip to content

chore(toolchain): track Lean v4.35.0 #47

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Oct 19, 2026
Merged

chore(toolchain): track Lean v4.35.0 #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0e14efa
chore(toolchain): track Lean v4.35.0
Oct 19, 2026
465d1a3
docs(state): name no Lean version in "Next action"
claude Oct 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.1,
Machine-checked, in this repository, by `lake build` (Lean 4, v4.35.0,
no dependencies):

* Every well-typed non-empty cross-region trace strictly worsens
Expand Down Expand Up @@ -171,7 +171,7 @@ artifact for PROVEN rows. No fabricated identifiers.

[source,shell]
----
elan default leanprover/lean4:v4.34.1 # or let lake read lean-toolchain
elan default leanprover/lean4:v4.35.0 # or let lake read lean-toolchain
lake build
----

Expand Down
21 changes: 17 additions & 4 deletions STATE.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,17 @@
= STATE — cross-session log

== 2026-10-19 — toolchain v4.34.1 → v4.35.0 (weekly track-lean bot)

* Gates on v4.35.0, verbatim:
+
Comment thread
coderabbitai[bot] marked this conversation as resolved.
Resolved
----
$ lake build
Build completed successfully (15 jobs).
$ grep -rnw sorry Marches/ Marches.lean # empty
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]
----

== 2026-10-14 — CI: estate audit pinned to cicd-suite main (not a rung)

* hyperpolymath/cicd-suite#50 merged as `376898b`. Its tree is identical to
Expand Down Expand Up @@ -256,7 +268,8 @@ Rung 3 (see ROADMAP.adoc), the remaining items. 3d: import the estate's
fully proved `TropicalAdapterPath.lean` (hyperpolymath/tropical-types,
lake package `tropical-resource-typing`, pinned `e172f8a`, Lean v4.13.0)
behind the `Marches/Tropical.lean` seam — vendor or depend on it, do NOT
paraphrase, and expect toolchain friction against v4.34.1. 3e: path
provenance as graded accumulation (echo-types bridge). 3f: file the
postern cross-issue once that repository exists. Obtain the real files;
never reconstruct from memory. One rung only.
paraphrase, and expect toolchain friction against the Lean marches pins
(`lean-toolchain`; named there, not here, so a weekly bump cannot make
this line stale). 3e: path provenance as graded accumulation (echo-types
bridge). 3f: file the postern cross-issue once that repository exists.
Obtain the real files; never reconstruct from memory. One rung only.
2 changes: 1 addition & 1 deletion lean-toolchain
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.34.1
leanprover/lean4:v4.35.0
Loading