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. diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc index 1b79bf6..4fa9c72 100644 --- a/docs/kcut-correspondence.adoc +++ b/docs/kcut-correspondence.adoc @@ -35,11 +35,11 @@ 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 -|`1073d600004d13f1aec7363baa0ee2e38d91568e` +|`b0982c44f36133acd2d0e1d4e03cf031fff7a470` |`Echo`, `echo-intro` (the fibre); `Provenance`, `provenance-collapses-at`, `echoes-distinguish-tag` (the audience-facing provenance theorems) |=== 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..9d1bdd1 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -13,8 +13,8 @@ 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}" -ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}" +TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5}" +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.