From f351d954723c43c145d767182f04559d19ec8da8 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898583+github-actions[bot]@users.noreply.github.com> Date: Mon, 2 Nov 2026 07:25:04 +0000 Subject: [PATCH 1/3] chore(siblings): re-pin tropical-types to 168f09d Weekly track-siblings run: https://github.com/hyperpolymath/marches/actions/runs/41406053103. PASS: 28 Lean names and 22 sibling names exist at the pins; both negative controls refused (cherry picked from commit e8148a4d3488b4c5b2bd7e060061d9934bd8584e) --- docs/kcut-correspondence.adoc | 2 +- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- scripts/fetch-siblings.sh | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc index 1b79bf6..e05eee4 100644 --- a/docs/kcut-correspondence.adoc +++ b/docs/kcut-correspondence.adoc @@ -35,7 +35,7 @@ ground (`LIMITATIONS.adoc`). |`_≼_` convention, `Loss`, `MaxPlus`, S-3 witnesses, M-2 status |hyperpolymath/tropical-types -|`226c9e191e0ab966f094a6394f0958cdc28254e0` +|`168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5` |`TropicalAdapterPath.lean` (also IMPORTED: the lake `require` in `lakefile.toml` is at this same commit), `TropicalSessionTypes.lean` (the Lean side of M-2) |hyperpolymath/echo-types diff --git a/lake-manifest.json b/lake-manifest.json index 2877cc3..d3e0f4a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "226c9e191e0ab966f094a6394f0958cdc28254e0", + "rev": "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5", "name": "«tropical-resource-typing»", "manifestFile": "lake-manifest.json", - "inputRev": "226c9e191e0ab966f094a6394f0958cdc28254e0", + "inputRev": "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5", "inherited": false, "configFile": "lakefile.lean"}], "name": "marches", diff --git a/lakefile.toml b/lakefile.toml index d8d6ef5..23d0fc9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,4 +11,4 @@ name = "Marches" [[require]] name = "tropical-resource-typing" git = "https://github.com/hyperpolymath/tropical-types" -rev = "226c9e191e0ab966f094a6394f0958cdc28254e0" +rev = "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5" diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 4ef07e4..b506c02 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -13,7 +13,7 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-f5a41772c2ca2345bd53579b73f064f4a3ab7ed7}" RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-e9482657aa791678e1d99996a18fb3e126e0d3c2}" -TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-226c9e191e0ab966f094a6394f0958cdc28254e0}" +TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5}" ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}" # Fetch a sibling repository and check out its pinned commit. From 74cae1ceaff2d1cc491f1e5e1046d05332e68900 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898583+github-actions[bot]@users.noreply.github.com> Date: Mon, 2 Nov 2026 07:25:36 +0000 Subject: [PATCH 2/3] chore(siblings): re-pin echo-types to b0982c4 Weekly track-siblings run: https://github.com/hyperpolymath/marches/actions/runs/41406053103. PASS: 28 Lean names and 22 sibling names exist at the pins; both negative controls refused (cherry picked from commit da0c680620e72db6fc782e987ad5528c42fa5c68) --- docs/kcut-correspondence.adoc | 2 +- scripts/fetch-siblings.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc index e05eee4..4fa9c72 100644 --- a/docs/kcut-correspondence.adoc +++ b/docs/kcut-correspondence.adoc @@ -39,7 +39,7 @@ ground (`LIMITATIONS.adoc`). |`TropicalAdapterPath.lean` (also IMPORTED: the lake `require` in `lakefile.toml` is at this same commit), `TropicalSessionTypes.lean` (the Lean side of M-2) |hyperpolymath/echo-types -|`1073d600004d13f1aec7363baa0ee2e38d91568e` +|`b0982c44f36133acd2d0e1d4e03cf031fff7a470` |`Echo`, `echo-intro` (the fibre); `Provenance`, `provenance-collapses-at`, `echoes-distinguish-tag` (the audience-facing provenance theorems) |=== diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index b506c02..9d1bdd1 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -14,7 +14,7 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-f5a41772c2ca2345bd53579b73f064f4a3ab7ed7}" RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-e9482657aa791678e1d99996a18fb3e126e0d3c2}" TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5}" -ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}" +ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-b0982c44f36133acd2d0e1d4e03cf031fff7a470}" # Fetch a sibling repository and check out its pinned commit. # Arguments: $1 is the repository name under hyperpolymath; $2 is the commit. From b9ea83a796e7b203d6426f1aff711b886316d2fe Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Wed, 4 Nov 2026 22:36:08 +0000 Subject: [PATCH 3/3] docs(state): rung 3d closed, tropical-types re-pinned to the #65 merge commit The two preceding commits are the weekly track-siblings re-pins from ci/track-siblings (cherry-picked with -x; that run could not open the PR without AUTOMATION_TOKEN). tropical-types moves from the PR-head pin 226c9e1, unreachable from a fresh clone since its branch was deleted, to 168f09d, the hyperpolymath/tropical-types#65 squash merge (identical Lean tree). echo-types moves to b0982c4 (F6: the cited files are untouched). The stale pin is also why that run filed #54 and #55: both checks died fetching tropical-types. With the fixed pin both siblings pass at HEAD. Gates from an empty _build/dependencies: lake build green (19 jobs); grep -rnw sorry empty; #eval orbit unchanged; check-correspondence.sh PASS (28 Lean, 22 sibling names). ROADMAP 3d met; rung 3 open on 3f only. No tag. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- ROADMAP.adoc | 4 ++-- STATE.adoc | 54 ++++++++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 48 insertions(+), 10 deletions(-) diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 859ac40..ca756b1 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -70,8 +70,8 @@ tropical-types: build on marches' toolchain (hyperpolymath/tropical-types#65). |`lakefile.toml` `require`; `Marches/TropicalAdapter.lean`; `track-siblings.yml` moves the lake pin with the sibling pin |it builds inside this repo on the pinned toolchain, unparaphrased -|met on a PR-head pin 2026-10-27; re-pin to the tropical-types#65 merge -commit closes it +|met 2026-11-04 (pinned to tropical-types `168f09d`, the #65 merge +commit) |3e. Path provenance as graded accumulation (echo-types bridge): what a trace *carries* across an interface, not just where it may go. diff --git a/STATE.adoc b/STATE.adoc index eb291c5..a71851c 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,48 @@ = STATE — cross-session log +== 2026-11-04 — rung 3d closed: tropical-types re-pinned to the #65 merge commit + +* #52 merged before hyperpolymath/tropical-types#65, so `main` kept the + PR-head pin `226c9e1`. #65 squash-merged as `168f09d` and its branch was + deleted; `226c9e1` is then on no branch, and a fresh clone's + `git fetch origin` never brings it in. Reproduced: + `TROPICAL_TYPES_COMMIT=226c9e1… scripts/fetch-siblings.sh` on an empty + `_build/dependencies` → `fatal: reference is not a tree: 226c9e1…`. +* That is why the 2026-11-02 `track-siblings` run filed #54 + (choreographic-types) and #55 (resource-algebra): both checks died on + the tropical-types fetch, not on a lost name. With the fixed pin, both + siblings at their current HEADs (`8751c7d`, `e25d35d`) give PASS. The + next weekly run re-pins them. +* The same run had already committed the right re-pins on + `ci/track-siblings` (tropical-types → `168f09d`, echo-types → `b0982c4`) + and failed only at `gh pr create` (Actions may not open PRs without + `AUTOMATION_TOKEN`). Those two commits are cherry-picked here with `-x`, + authorship kept. `168f09d` and `226c9e1` have identical Lean trees + (`git diff --stat` over `*.lean`, `lean-toolchain`, `lakefile.lean` is + empty). +* F6, echo-types `1073d60..b0982c4`: one commit, and it touches neither + `proofs/agda/Echo.agda` nor `proofs/agda/EchoProvenance.agda`. +* #52's squash also carries CodeRabbit's autofix of `track-siblings.yml` + (its Major finding: build candidate pins without the write token). Read + after the fact: a read-only `check` job builds and passes patches and + JSON as data; `publish` holds the token, applies only patches touching + the four pin files, and still exits red on broken names. shellcheck on + both extracted run blocks: clean except SC2153 (info, `BASE` comes from + `env:`), which actionlint 1.7.7 also reports. +* Gates on v4.35.0 at `168f09d`, from an empty `_build/dependencies`: ++ +---- +$ lake build +Build completed successfully (19 jobs). +$ grep -rnw sorry Marches/ Marches.lean # empty +$ lake env lean Marches/BadGadget.lean +[(false, false), (true, true), (false, false), (true, true)] +$ scripts/check-correspondence.sh +PASS: 28 Lean names and 22 sibling names exist at the pins; both negative controls refused +---- +* ROADMAP 3d: met. Rung 3 stays OPEN on 3f only (postern: `list_repos` + query `postern` empty). No tag. + == 2026-10-27 — rung 3d: TropicalAdapterPath imported, unparaphrased * Upstream prerequisite: hyperpolymath/tropical-types#65 moves that @@ -389,11 +432,6 @@ $ lake env lean Marches/BadGadget.lean == Next action -Rung 3 (see ROADMAP.adoc), the remaining items. 3d: once -hyperpolymath/tropical-types#65 merges, re-pin `lakefile.toml`, -`lake-manifest.json`, `scripts/fetch-siblings.sh` and the correspondence -pin table to its merge commit (one sed of the SHA; then `lake build` and -`scripts/check-correspondence.sh`). 3e: met 2026-10-27 -(`Marches/Provenance.lean`). 3f: file the postern cross-issue once that -repository exists. Obtain the real files; never reconstruct from memory. -One rung only. +Rung 3 (see ROADMAP.adoc): only 3f remains. File the postern cross-issue +once that repository exists (not found 2026-11-04). 3d and 3e are met. +Obtain the real files; never reconstruct from memory. One rung only.