From 80aa15ca62372d220068784c629ba3045cf6040f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 14:01:19 +0000 Subject: [PATCH 1/2] feat(tropical): rung 3d, import TropicalAdapterPath unparaphrased MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lakefile.toml requires tropical-types (lake package tropical-resource-typing) at a full commit, and the new Marches/TropicalAdapter.lean imports TropicalAdapterPath without re-stating any of it. It connects upstream to rung 3e through upstream's own theorems: the min-max βŠ— is a marches Grade (bottleneck), upstream's pathCost is that grade's accumulation (pathCost_eq_accum), hub_ceiling floors it (carried_floor), and a non-empty path can carry πŸ™, so this grade gives no loop-freedom (bottleneck_carries_unit). The pin is hyperpolymath/tropical-types#65's head 226c9e1 (that PR moves tropical-types to Lean v4.35.0); fetch-siblings.sh pins the same commit. Re-pin both to #65's merge commit before merging. track-siblings.yml now moves lakefile.toml and lake-manifest.json with the tropical-types pin, and a failed re-check restores the pins and files an issue instead of exiting red. Negative control: a lake pin at e172f8a (v4.13-only) is re-materialised and fails the build. KC-13 records the one mechanical LINK in the correspondence table. Gates: lake build green (19 jobs); grep -rnw sorry empty; #eval orbit unchanged; check-correspondence.sh PASS (28 Lean, 22 sibling names). #print axioms: the five new declarations carry exactly the upstream lemmas' footprints (propext, Quot.sound); marches adds none. No tag: 3f (postern) still open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- .github/workflows/track-siblings.yml | 22 +++++--- Marches.lean | 1 + Marches/Tropical.lean | 11 ++-- Marches/TropicalAdapter.lean | 77 ++++++++++++++++++++++++++++ README.adoc | 18 +++++-- ROADMAP.adoc | 8 +-- STATE.adoc | 68 ++++++++++++++++++++---- docs/kcut-correspondence.adoc | 16 +++++- lake-manifest.json | 17 ++++-- lakefile.toml | 8 +++ scripts/fetch-siblings.sh | 11 ++-- 11 files changed, 222 insertions(+), 35 deletions(-) create mode 100644 Marches/TropicalAdapter.lean diff --git a/.github/workflows/track-siblings.yml b/.github/workflows/track-siblings.yml index bfb902f..a56529f 100644 --- a/.github/workflows/track-siblings.yml +++ b/.github/workflows/track-siblings.yml @@ -11,6 +11,10 @@ name: Track latest siblings # - A cited name is gone at HEAD β†’ an issue with the check's output; the pin # stays put. # +# tropical-types is also a lake `require` (rung 3d): its re-pin moves +# lakefile.toml and lake-manifest.json too, and the re-check's `lake build` +# must pass against the new HEAD, or the pin stays and an issue is filed. +# # Names only. Whether a re-pinned name still MEANS the same thing is falsifier # F6, and no script decides it: the PR asks for the sibling diff to be read. # @@ -64,12 +68,18 @@ jobs: echo "$repo: pinned ${pinned:0:7}, HEAD ${head:0:7}" [ "$pinned" = "$head" ] && continue - out=$(mktemp) + out=$(mktemp); ok=0 if env "$var=$head" scripts/check-correspondence.sh >"$out" 2>&1; then - sed -i "s/$pinned/$head/g" scripts/fetch-siblings.sh docs/kcut-correspondence.adoc - if ! scripts/check-correspondence.sh >"$out" 2>&1; then - echo "::error::$repo re-pin did not re-check"; cat "$out"; exit 1 - fi + # tropical-types is also a lake `require` at the same commit + # (rung 3d): move the lakefile and manifest pins with it, so the + # re-check's `lake build` builds marches against the new HEAD. + # If that fails, restore the pins and report it like a lost name. + sed -i "s/$pinned/$head/g" scripts/fetch-siblings.sh docs/kcut-correspondence.adoc \ + lakefile.toml lake-manifest.json + if scripts/check-correspondence.sh >"$out" 2>&1; then ok=1 + else git checkout --quiet -- .; fi + fi + if [ "$ok" -eq 1 ]; then git -c user.name='github-actions[bot]' \ -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \ commit --quiet -am "chore(siblings): re-pin $repo to ${head:0:7}" \ @@ -78,7 +88,7 @@ jobs: else title="Sibling $repo at HEAD breaks the K-CUT correspondence names" # shellcheck disable=SC2016 # literal Markdown backticks - body=$(printf 'Weekly check (%s): docs/kcut-correspondence.adoc against hyperpolymath/%s HEAD `%s` (pinned: `%s`). The pin stays put.\n\n```\n%s\n```\n' \ + body=$(printf 'Weekly check (%s): docs/kcut-correspondence.adoc (and, for tropical-types, `lake build`) against hyperpolymath/%s HEAD `%s` (pinned: `%s`). The pin stays put.\n\n```\n%s\n```\n' \ "$run_url" "$repo" "$head" "$pinned" "$(tail -n 40 "$out")") existing=$(gh issue list --state open --search "in:title \"$title\"" --json number --jq '.[0].number // empty') if [ -n "$existing" ]; then gh issue comment "$existing" --body "$body" diff --git a/Marches.lean b/Marches.lean index d6a55d5..e507d67 100644 --- a/Marches.lean +++ b/Marches.lean @@ -11,3 +11,4 @@ import Marches.Freewheel import Marches.Reassembly import Marches.Cut import Marches.Provenance +import Marches.TropicalAdapter diff --git a/Marches/Tropical.lean b/Marches/Tropical.lean index 37548aa..9239e15 100644 --- a/Marches/Tropical.lean +++ b/Marches/Tropical.lean @@ -6,11 +6,12 @@ extension adds weight + 1 (positive weights β‡’ strictness). This file is the seam for integrating the estate's existing - fully proved tropical work. Read 2026-10-14: `TropicalAdapterPath.lean` - lives in hyperpolymath/tropical-types (whose lake package is named - `tropical-resource-typing`) at e172f8a, on Lean v4.13.0. Status of the - import: OPEN (rung 3 in ROADMAP.adoc). Nothing here fabricates or - depends on that file's contents. + fully proved tropical work. `TropicalAdapterPath.lean` lives in + hyperpolymath/tropical-types (lake package `tropical-resource-typing`), + required in lakefile.toml at a pinned commit and imported unparaphrased + by `Marches/TropicalAdapter.lean` (rung 3d). Nothing in THIS file + depends on it: `TropicalNat` (min-plus) is not upstream's min-max + transport semiring. The cross-prover bridge is resource-algebra's M-2 (pinned in scripts/fetch-siblings.sh): Agda `MaxPlus` vs tropical-types' Lean `CommSemiring Tropical`, OPEN, diff --git a/Marches/TropicalAdapter.lean b/Marches/TropicalAdapter.lean new file mode 100644 index 0000000..fb575f4 --- /dev/null +++ b/Marches/TropicalAdapter.lean @@ -0,0 +1,77 @@ +/- + Marches β€” the estate's tropical proofs, imported (rung 3d). + + `TropicalAdapterPath` is hyperpolymath/tropical-types' fully proved + min-max ("bottleneck") transport semiring, required in `lakefile.toml` + at a pinned commit and imported here UNPARAPHRASED: nothing below + re-states or re-proves its contents. This file only connects it to + marches' own machinery, through upstream's own theorems. + + β€’ TropicalAdapter.bottleneck : upstream's `βŠ—` (`tcMul` = max, unit + `tcOne` = 0) is a marches `Grade`; all + three laws are upstream's. + β€’ TropicalAdapter.pathCost_eq_accum : upstream's `pathCost` IS marches' + `Grade.accum` of transport grades + under `bottleneck`. + β€’ TropicalAdapter.carried_floor : every step on a path floors the grade + the path carries (upstream's + `hub_ceiling`, read as provenance). + β€’ TropicalAdapter.bottleneck_carries_unit : a NON-empty path can carry + the unit `πŸ™` (one Concorde step). So + `bottleneck`, unlike `TropicalGrade`, + is not strictly inflationary as a + grade: `carried_cons_ne_one` has no + analogue, and no loop-freedom follows + from it (the F2 lesson, again). + + The min-max semiring is neither marches' `TropicalNat` (min-plus) nor + M-2's max-plus; see docs/kcut-correspondence.adoc (KC-13). Delimitation + unchanged: nothing here is protocol convergence (LIMITATIONS.adoc). +-/ + +import TropicalAdapterPath +import Marches.Provenance + +namespace Marches +namespace TropicalAdapter + +open Hyperpolymath.ProtocolSquisher.Tropical + +/-- The bottleneck grade: upstream's min-max `βŠ—` as a marches `Grade`. + Every law is an upstream theorem. -/ +def bottleneck : Grade where + G := Nat + seq := tcMul + one := tcOne + seq_assoc := tcMul_assoc + seq_unitl := tcMul_one_left + seq_unitr := tcMul_one_right + +/-- Upstream's path cost is marches' accumulation: the bottleneck grade a + path of transport steps carries. -/ +theorem pathCost_eq_accum : βˆ€ p : AdapterPath, pathCost p = bottleneck.accum grade p + | [] => rfl + | c :: cs => + (pathCost_cons c cs).trans (congrArg (Nat.max (grade c)) (pathCost_eq_accum cs)) + +/-- Upstream's `pathCost_append`, recovered from marches' `accum_append`: + the two developments agree on concatenation. -/ +theorem pathCost_append_via_accum (p q : AdapterPath) : + pathCost (p ++ q) = tcMul (pathCost p) (pathCost q) := by + rw [pathCost_eq_accum, pathCost_eq_accum, pathCost_eq_accum] + exact bottleneck.accum_append grade p q + +/-- Every step on a path floors the grade the path carries: upstream's + `hub_ceiling`, read as provenance. -/ +theorem carried_floor (e : TransportClass) (p : AdapterPath) (h : e ∈ p) : + grade e ≀ bottleneck.accum grade p := + pathCost_eq_accum p β–Έ hub_ceiling e p h + +/-- A non-empty path can carry the unit: one Concorde step carries `πŸ™`. + Contrast `TropicalGrade.carried_cons_ne_one`. -/ +theorem bottleneck_carries_unit : + bottleneck.accum grade [TransportClass.Concorde] = bottleneck.one := + rfl + +end TropicalAdapter +end Marches diff --git a/README.adoc b/README.adoc index d74c1e8..8d305fa 100644 --- a/README.adoc +++ b/README.adoc @@ -179,9 +179,18 @@ echo-types' `Echo` and provenance theorems checked at their pins by `scripts/check-correspondence.sh`. Falsifier F6 is open and has already withdrawn one proposed pairing. -|Tropical estate integration (`TropicalAdapterPath.lean`) -|OPEN -|rung 3 +|Tropical estate integration: tropical-types' `TropicalAdapterPath.lean` +builds inside this repo, unparaphrased, and its `pathCost` is marches' +grade accumulation under the bottleneck grade +|PROVEN +|`lake build` with the `lakefile.toml` `require`; +`TropicalAdapter.pathCost_eq_accum`, `pathCost_append_via_accum`, +`carried_floor`, `bottleneck_carries_unit` + +|The bottleneck grade gives no loop-freedom: a non-empty path can carry +the unit +|PROVEN (finite) +|`TropicalAdapter.bottleneck_carries_unit` |Protocol-level asynchronous convergence |OUT OF SCOPE @@ -247,6 +256,9 @@ A red result opens an issue instead of a PR. start `βŠ—` carried; a crossing trace is A-word, crossing, B-word, and carries the A-signature into the fibre of `Ο„`; in the DAG the grade reaching a cut or a crossing is accumulated inside the prefix. +* `Marches/TropicalAdapter.lean` β€” rung 3d: imports tropical-types' + `TropicalAdapterPath` unparaphrased (a lake `require`); its min-max `βŠ—` + is a marches `Grade`, and its `pathCost` is that grade's accumulation. == Licence diff --git a/ROADMAP.adoc b/ROADMAP.adoc index c750251..859ac40 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -66,10 +66,12 @@ hyperpolymath/tropical-types (lake package `tropical-resource-typing`) at `e172f8a`, on Lean v4.13.0. Decided 2026-10-14: *depend, tracking latest*. `lakefile` requires tropical-types at a pinned commit, and the weekly re-pin bot keeps that commit current. Prerequisite, upstream in -tropical-types: build on marches' toolchain. -|β€” +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 -|OPEN +|met on a PR-head pin 2026-10-27; re-pin to the tropical-types#65 merge +commit closes it |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 352e7f7..eb291c5 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,56 @@ = STATE β€” cross-session log +== 2026-10-27 β€” rung 3d: TropicalAdapterPath imported, unparaphrased + +* Upstream prerequisite: hyperpolymath/tropical-types#65 moves that + package from Lean v4.13.0 to v4.35.0. No statement changes; seven proof + edits for core-API drift (implicit arguments of `List.not_mem_nil`, + `List.mem_cons_self`, `List.mem_map_of_mem`; `Nat.max_def` now unfolds to + an `if`; new core `add_max_add_*`/`add_min_add_*` simp lemmas made four + `simp [.., helper]` calls loop). There: `lake build` β†’ 20 jobs green, and + its own `lean.yml` axiom audit, run verbatim, passes; only `hub_ceiling` + moved (`propext` β†’ `propext, Quot.sound`, from core `simp`). +* Here: `lakefile.toml` requires `tropical-resource-typing` at a full + commit, pinned for now to #65's head `226c9e1` so this PR's CI exercises + the real dependency. `scripts/fetch-siblings.sh` pins the same commit. + Re-pin both to #65's merge commit before merging this. +* New `Marches/TropicalAdapter.lean` imports `TropicalAdapterPath` and + re-states none of it. `bottleneck` (upstream's min-max `βŠ—` as a marches + `Grade`, by upstream's laws); `pathCost_eq_accum` (upstream's `pathCost` + is `Grade.accum`); `pathCost_append_via_accum`; `carried_floor` + (`hub_ceiling` read as provenance); `bottleneck_carries_unit` (a + non-empty path carries `πŸ™`: no loop-freedom from this grade). +* `track-siblings.yml`: a tropical-types re-pin now also moves + `lakefile.toml` and `lake-manifest.json`, so the re-check builds marches + against the new HEAD. A failed re-check restores the pins and files an + issue (before, it exited red with no issue). Negative control run here: + pointing the lake pin at `e172f8a` (v4.13-only) re-materialises that + commit and fails the build (`TropicalAdapterPath.lean:132:12`, omega); + restoring it builds green. +* KC-13: the one LINK in the correspondence table (both sides Lean, + imported). README rows PROVEN / PROVEN (finite). +* Gates on v4.35.0, verbatim: ++ +---- +$ 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 +---- ++ +`#print axioms` on the five new declarations: `propext` and/or +`Quot.sound`, each exactly the footprint of the upstream lemma it +consumes (`pathCost_cons`, `hub_ceiling`, `tcMul_one_left`). marches adds +none. The 20 rung-3e declarations still report none. +* actionlint 1.7.7 and shellcheck clean (workflow run block extracted and + checked too); Asciidoctor warning counts unchanged from `main`. +* ROADMAP 3d: met on the PR-head pin; the merge-commit re-pin closes it. + Rung 3 then stays OPEN only on 3f: postern still not found + (`list_repos` query `postern`: no match, 2026-10-27). No tag. + == 2026-10-27 β€” rung 3e: path provenance as graded accumulation (echo-types bridge) * New `Marches/Provenance.lean`, imported from `Marches.lean`. `Cut.lean` @@ -338,12 +389,11 @@ $ lake env lean Marches/BadGadget.lean == Next action -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 the Lean marches pins -(`lean-toolchain`; named there, not here, so a weekly bump cannot make -this line stale). 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), 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. diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc index 197b6e2..1b79bf6 100644 --- a/docs/kcut-correspondence.adoc +++ b/docs/kcut-correspondence.adoc @@ -35,8 +35,8 @@ ground (`LIMITATIONS.adoc`). |`_β‰Ό_` convention, `Loss`, `MaxPlus`, S-3 witnesses, M-2 status |hyperpolymath/tropical-types -|`e172f8abefd50fc40def4368fa60a155d130ff47` -|`TropicalAdapterPath.lean`, `TropicalSessionTypes.lean` (the Lean side of M-2) +|`226c9e191e0ab966f094a6394f0958cdc28254e0` +|`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` @@ -177,6 +177,18 @@ discharges all three for (min, +). A different law set for a different theorem, not a disagreement; no counterpart is proposed for `seq_assoc` or `seq_unitr`. |ASSUMED for `seq_unitl ↔ unitΛ‘` (as KC-6); the other two laws unpaired + +|KC-13 +|`Marches.TropicalAdapter.bottleneck`, `Marches.TropicalAdapter.pathCost_eq_accum`, `Marches.TropicalAdapter.carried_floor`, `Marches.TropicalAdapter.bottleneck_carries_unit` +|`tropical-types:TropicalAdapterPath.lean` +|Not a table row but a LINK, the only one here: both sides are Lean, and +`Marches/TropicalAdapter.lean` imports the file, so `lake build` checks +every use. Upstream's min-max `βŠ—` (`tcMul`, unit `tcOne`) is a marches +`Grade` by upstream's own laws; upstream's `pathCost` is that grade's +accumulation; `hub_ceiling` floors it. It is NOT `TropicalNat` (min-plus, +KC-8) and NOT M-2's max-plus: a non-empty path can carry `πŸ™`, so it gives no +loop-freedom. +|PROVEN (imported; `lake build`) |=== == Transport, for postern diff --git a/lake-manifest.json b/lake-manifest.json index 2bf1309..2877cc3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,5 +1,16 @@ -{"version": "1.1.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"url": "https://github.com/hyperpolymath/tropical-types", + "type": "git", + "subDir": null, + "scope": "", + "rev": "226c9e191e0ab966f094a6394f0958cdc28254e0", + "name": "Β«tropical-resource-typingΒ»", + "manifestFile": "lake-manifest.json", + "inputRev": "226c9e191e0ab966f094a6394f0958cdc28254e0", + "inherited": false, + "configFile": "lakefile.lean"}], "name": "marches", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index af0f3ba..d8d6ef5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,3 +4,11 @@ defaultTargets = ["Marches"] [[lean_lib]] name = "Marches" + +# Rung 3d: the estate's tropical proofs, imported unparaphrased. Pinned to a +# full commit; scripts/fetch-siblings.sh pins the same commit, and +# .github/workflows/track-siblings.yml moves both together. +[[require]] +name = "tropical-resource-typing" +git = "https://github.com/hyperpolymath/tropical-types" +rev = "226c9e191e0ab966f094a6394f0958cdc28254e0" diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 46da36d..4ef07e4 100755 --- a/scripts/fetch-siblings.sh +++ b/scripts/fetch-siblings.sh @@ -2,15 +2,18 @@ # SPDX-License-Identifier: MPL-2.0 # Fetch the sibling proof repositories marches cites, each at a pinned # commit, into _build/dependencies (pattern: choreographic-types, -# residual-evidence-types). Nothing here is imported into the Lean build: -# the siblings are read, never re-declared. Re-pin deliberately, one -# commit per pin, and update docs/kcut-correspondence.adoc to match. +# residual-evidence-types). The siblings are read, never re-declared. One is +# also imported: tropical-types is a lake `require` in lakefile.toml at the +# SAME commit as TROPICAL_TYPES_COMMIT below (rung 3d), and +# .github/workflows/track-siblings.yml moves both pins together. Re-pin +# deliberately, one commit per pin, and update docs/kcut-correspondence.adoc +# to match. set -euo pipefail 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:-e172f8abefd50fc40def4368fa60a155d130ff47}" +TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-226c9e191e0ab966f094a6394f0958cdc28254e0}" ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}" # Fetch a sibling repository and check out its pinned commit. From 8b640d5cb2e546b64a566f3a61283eae8df89e24 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 14:14:57 +0000 Subject: [PATCH 2/2] fix(ci): isolate sibling checks from write credentials in a separate publish job --- .github/workflows/track-siblings.yml | 104 ++++++++++++++++++++++----- 1 file changed, 85 insertions(+), 19 deletions(-) diff --git a/.github/workflows/track-siblings.yml b/.github/workflows/track-siblings.yml index a56529f..273492d 100644 --- a/.github/workflows/track-siblings.yml +++ b/.github/workflows/track-siblings.yml @@ -19,7 +19,9 @@ name: Track latest siblings # F6, and no script decides it: the PR asks for the sibling diff to be read. # # ⚠ NO `uses:` (see labels.yml): Lean comes from elan's installer. -# Token: AUTOMATION_TOKEN if set (see actions-lock.yml), else GITHUB_TOKEN. +# The check job has read-only permissions and no token in its environment. +# Only publish uses AUTOMATION_TOKEN (see actions-lock.yml), else GITHUB_TOKEN. +# Job outputs carry patches and issue text as data; publish never builds them. on: schedule: @@ -34,30 +36,34 @@ concurrency: cancel-in-progress: false jobs: - repin: + check: runs-on: ubuntu-latest permissions: - contents: write - issues: write - pull-requests: write + contents: read + outputs: + base: ${{ steps.check.outputs.base }} + patches: ${{ steps.check.outputs.patches }} + repinned: ${{ steps.check.outputs.repinned }} + issues: ${{ steps.check.outputs.issues }} env: - GH_TOKEN: ${{ secrets.AUTOMATION_TOKEN || secrets.GITHUB_TOKEN }} BASE: main BRANCH: ci/track-siblings steps: - name: Check the correspondence against sibling HEADs and re-pin + id: check run: | set -euo pipefail - gh auth setup-git - gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE" + git clone --quiet --depth 1 --branch "$BASE" "https://github.com/$GITHUB_REPOSITORY.git" repo cd repo curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ | sh -s -- -y --default-toolchain none --no-modify-path export PATH="$HOME/.elan/bin:$PATH" run_url="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID" + base=$(git rev-parse HEAD) git switch --quiet -c "$BRANCH" - - repinned=(); broken=() + report=$(mktemp -d) + printf '[]\n' > "$report/issues.json" + printf '[]\n' > "$report/repinned.json" for spec in choreographic-types:CHOREOGRAPHIC_TYPES_COMMIT \ resource-algebra:RESOURCE_ALGEBRA_COMMIT \ tropical-types:TROPICAL_TYPES_COMMIT \ @@ -84,31 +90,91 @@ jobs: -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \ commit --quiet -am "chore(siblings): re-pin $repo to ${head:0:7}" \ -m "Weekly track-siblings run: $run_url. $(tail -n 1 "$out")" - repinned+=("$repo ${pinned:0:7} β†’ ${head:0:7} (https://github.com/hyperpolymath/$repo/compare/$pinned...$head)") + jq --arg entry "$repo ${pinned:0:7} β†’ ${head:0:7} (https://github.com/hyperpolymath/$repo/compare/$pinned...$head)" \ + '. + [$entry]' "$report/repinned.json" > "$report/next.json" + mv "$report/next.json" "$report/repinned.json" else title="Sibling $repo at HEAD breaks the K-CUT correspondence names" # shellcheck disable=SC2016 # literal Markdown backticks body=$(printf 'Weekly check (%s): docs/kcut-correspondence.adoc (and, for tropical-types, `lake build`) against hyperpolymath/%s HEAD `%s` (pinned: `%s`). The pin stays put.\n\n```\n%s\n```\n' \ "$run_url" "$repo" "$head" "$pinned" "$(tail -n 40 "$out")") - existing=$(gh issue list --state open --search "in:title \"$title\"" --json number --jq '.[0].number // empty') - if [ -n "$existing" ]; then gh issue comment "$existing" --body "$body" - else gh issue create --title "$title" --body "$body"; fi - broken+=("$repo") + jq --arg title "$title" --arg body "$body" --arg repo "$repo" \ + '. + [{title: $title, body: $body, repo: $repo}]' \ + "$report/issues.json" > "$report/next.json" + mv "$report/next.json" "$report/issues.json" fi done - if [ "${#repinned[@]}" -gt 0 ]; then + # No candidate code runs in the later job. Transfer only commit + # patches and JSON reports, without actions that need a lock entry. + git format-patch --stdout "$base..HEAD" > "$report/patches" + { + printf 'base=%s\n' "$base" + printf 'patches=%s\n' "$(base64 -w0 < "$report/patches")" + printf 'repinned=%s\n' "$(jq -c . "$report/repinned.json")" + printf 'issues=%s\n' "$(jq -c . "$report/issues.json")" + } >> "$GITHUB_OUTPUT" + + publish: + needs: check + runs-on: ubuntu-latest + permissions: + contents: write + issues: write + pull-requests: write + env: + GH_TOKEN: ${{ secrets.AUTOMATION_TOKEN || secrets.GITHUB_TOKEN }} + BASE: main + BRANCH: ci/track-siblings + CHECKED_BASE: ${{ needs.check.outputs.base }} + PATCHES: ${{ needs.check.outputs.patches }} + REPINNED: ${{ needs.check.outputs.repinned }} + ISSUES: ${{ needs.check.outputs.issues }} + steps: + - name: Publish correspondence issues and re-pin PR + run: | + set -euo pipefail + gh auth setup-git + gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE" + cd repo + run_url="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID" + + # Treat the read-only job's outputs as data, never shell commands. + while IFS= read -r issue; do + title=$(jq -r '.title' <<< "$issue") + body=$(jq -r '.body' <<< "$issue") + existing=$(gh issue list --state open --search "in:title \"$title\"" --json number --jq '.[0].number // empty') + if [ -n "$existing" ]; then gh issue comment "$existing" --body "$body" + else gh issue create --title "$title" --body "$body"; fi + done < <(jq -c '.[]' <<< "$ISSUES") + + if [ "$(jq 'length' <<< "$REPINNED")" -gt 0 ]; then + [[ "$CHECKED_BASE" =~ ^[0-9a-f]{40}$ ]] + git fetch --quiet origin "$CHECKED_BASE" + git switch --quiet -c "$BRANCH" "$CHECKED_BASE" + printf '%s' "$PATCHES" | base64 --decode > "$RUNNER_TEMP/repin.patch" + git -c core.hooksPath=/dev/null \ + -c user.name='github-actions[bot]' \ + -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \ + am --quiet "$RUNNER_TEMP/repin.patch" + # Refuse patches outside the four files used for re-pinning. + while IFS= read -r -d '' path; do + case "$path" in + scripts/fetch-siblings.sh|docs/kcut-correspondence.adoc|lakefile.toml|lake-manifest.json) ;; + *) echo "::error::Unexpected re-pin path: $path"; exit 1 ;; + esac + done < <(git diff --name-only -z "$CHECKED_BASE" HEAD) git push --quiet --force origin "$BRANCH" # shellcheck disable=SC2016 # literal Markdown backticks body=$(printf 'Weekly re-pin (%s). Every name docs/kcut-correspondence.adoc cites still exists at the new pins, and both negative controls are refused (`scripts/check-correspondence.sh`).\n\n%s\n\n**Names only.** Read each sibling diff above before merging: whether a name still means the same thing is falsifier F6.\n' \ - "$run_url" "$(printf -- '- %s\n' "${repinned[@]}")") + "$run_url" "$(jq -r '.[] | "- " + .' <<< "$REPINNED")") if [ -n "$(gh pr list --head "$BRANCH" --state open --json number --jq '.[].number')" ]; then gh pr edit "$BRANCH" --body "$body" else gh pr create --base "$BASE" --head "$BRANCH" --title "chore(siblings): re-pin to latest" --body "$body" fi fi - if [ "${#broken[@]}" -gt 0 ]; then - echo "::error::names broken at HEAD for: ${broken[*]} (issues filed)" + if [ "$(jq 'length' <<< "$ISSUES")" -gt 0 ]; then + echo "::error::names broken at HEAD for: $(jq -r 'map(.repo) | join(" ")' <<< "$ISSUES") (issues filed)" exit 1 fi