ci: weekly track-latest for the Lean toolchain and sibling pins

.github/workflows/track-lean.yml

@@ -0,0 +1,109 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Track latest Lean
+
+# Weekly: is there a newer stable Lean than lean-toolchain pins? If so, build
+# marches on it and run every gate. Green → a PR that bumps lean-toolchain and
+# README's two version mentions and records the gate output in STATE.adoc.
+# Red → an issue carrying the failing output. Either way a person merges or
+# decides; nothing lands on main unreviewed.
+#
+# "Stable" means a vMAJOR.MINOR.PATCH tag of leanprover/lean4 (no -rc).
+#
+# ⚠ NO `uses:` (see labels.yml): Lean comes from elan's installer, so this
+# workflow needs no action and no actions.lock entry beyond [].
+#
+# Token: AUTOMATION_TOKEN if set (see actions-lock.yml), else GITHUB_TOKEN.
+
+on:
+  schedule:
+    - cron: "11 7 * * 1"   # weekly, Monday
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: track-lean
+  cancel-in-progress: false
+
+jobs:
+  bump:
+    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-lean
+      ORBIT: "[(false, false), (true, true), (false, false), (true, true)]"
+    steps:
+      - name: Try the latest stable Lean and open a PR or an issue
+        run: |
+          set -euo pipefail
+          gh auth setup-git
+          gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE"
+          cd repo
+
+          current=$(sed -n 's|^leanprover/lean4:||p' lean-toolchain)
+          latest=$(git ls-remote --tags --refs https://github.com/leanprover/lean4 \
+                     | sed -n 's|.*refs/tags/\(v[0-9]*\.[0-9]*\.[0-9]*\)$|\1|p' | sort -V | tail -1)
+          echo "pinned: $current   latest stable: $latest"
+          if [ "$(printf '%s\n%s\n' "$current" "$latest" | sort -V | tail -1)" = "$current" ]; then
+            echo "lean-toolchain is already at the latest stable release."
+            exit 0
+          fi
+
+          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"
+          echo "leanprover/lean4:$latest" > lean-toolchain
+          sed -i "s/${current//./\\.}/$latest/g" README.adoc
+
+          # The three gates (CLAUDE.md), each recorded verbatim.
+          log=$(mktemp)
+          build_ok=0; sorry_ok=0; orbit_ok=0
+          if lake build >"$log" 2>&1; then build_ok=1; fi
+          build_line=$(tail -n 1 "$log")
+          if ! grep -rnw sorry Marches/ Marches.lean >/dev/null; then sorry_ok=1; fi
+          orbit=$(lake env lean Marches/BadGadget.lean 2>&1 || true)
+          # shellcheck disable=SC2153  # ORBIT is set in the job env:
+          if [ "$orbit" = "$ORBIT" ]; then orbit_ok=1; fi
+          gates=$(printf '%s\n' \
+            "\$ lake build" "$build_line" \
+            "\$ grep -rnw sorry Marches/ Marches.lean  # $([ "$sorry_ok" = 1 ] && echo empty || echo FOUND)" \
+            "\$ lake env lean Marches/BadGadget.lean" "$orbit")
+          run_url="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+
+          if [ "$build_ok$sorry_ok$orbit_ok" != 111 ]; then
+            title="Lean $latest breaks marches"
+            # shellcheck disable=SC2016  # literal Markdown backticks
+            body=$(printf 'Weekly check (%s) built marches on Lean %s (pinned: %s). At least one gate failed.\n\n```\n%s\n```\n\nLast 60 lines of `lake build`:\n\n```\n%s\n```\n' \
+              "$run_url" "$latest" "$current" "$gates" "$(tail -n 60 "$log")")
+            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
+            exit 1
+          fi
+
+          today=$(date -u +%F)
+          entry=$(printf '== %s — toolchain %s → %s (weekly track-lean bot)\n\n* Gates on %s, verbatim:\n+\n----\n%s\n----\n' \
+            "$today" "$current" "$latest" "$latest" "$gates")
+          ENTRY="$entry" awk 'NR==2 && !done { print; print ENVIRON["ENTRY"]; print ""; done=1; next } { print }' \
+            STATE.adoc > STATE.new && mv STATE.new STATE.adoc
+
+          git switch --quiet -c "$BRANCH"
+          git -c user.name='github-actions[bot]' \
+              -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \
+              commit --quiet -am "chore(toolchain): track Lean $latest" \
+              -m "Weekly track-lean run: $run_url. All three gates pass on $latest."
+          git push --quiet --force origin "$BRANCH"
+          # shellcheck disable=SC2016  # literal Markdown backticks
+          body=$(printf 'Lean %s is the latest stable release; marches pins %s. Built and gated on %s by %s:\n\n```\n%s\n```\n' \
+            "$latest" "$current" "$latest" "$run_url" "$gates")
+          if [ -n "$(gh pr list --head "$BRANCH" --state open --json number --jq '.[].number')" ]; then
+            gh pr edit "$BRANCH" --title "chore(toolchain): track Lean $latest" --body "$body"
+          else
+            gh pr create --base "$BASE" --head "$BRANCH" --title "chore(toolchain): track Lean $latest" --body "$body"
+          fi

.github/workflows/track-siblings.yml

@@ -0,0 +1,103 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Track latest siblings
+
+# Weekly: for each sibling proof repository pinned in scripts/fetch-siblings.sh
+# (choreographic-types, resource-algebra, tropical-types), check
+# docs/kcut-correspondence.adoc against the sibling's current HEAD.
+#
+# - Every cited name still exists at HEAD → re-pin: one commit per sibling,
+#   updating the pin in fetch-siblings.sh and the doc's pin table together,
+#   re-checked with scripts/check-correspondence.sh, in one PR.
+# - A cited name is gone at HEAD → an issue with the check's output; the pin
+#   stays put.
+#
+# 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.
+#
+# ⚠ NO `uses:` (see labels.yml): Lean comes from elan's installer.
+# Token: AUTOMATION_TOKEN if set (see actions-lock.yml), else GITHUB_TOKEN.
+
+on:
+  schedule:
+    - cron: "17 7 * * 1"   # weekly, Monday
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: track-siblings
+  cancel-in-progress: false
+
+jobs:
+  repin:
+    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
+    steps:
+      - name: Check the correspondence against sibling HEADs and re-pin
+        run: |
+          set -euo pipefail
+          gh auth setup-git
+          gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE"
+          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"
+          git switch --quiet -c "$BRANCH"
+
+          repinned=(); broken=()
+          for spec in choreographic-types:CHOREOGRAPHIC_TYPES_COMMIT \
+                      resource-algebra:RESOURCE_ALGEBRA_COMMIT \
+                      tropical-types:TROPICAL_TYPES_COMMIT; do
+            repo="${spec%%:*}"; var="${spec#*:}"
+            pinned=$(grep -E "^${var}=" scripts/fetch-siblings.sh | grep -oE '[0-9a-f]{40}')
+            head=$(git ls-remote "https://github.com/hyperpolymath/$repo.git" HEAD | cut -f1)
+            echo "$repo: pinned ${pinned:0:7}, HEAD ${head:0:7}"
+            [ "$pinned" = "$head" ] && continue
+
+            out=$(mktemp)
+            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
+              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}" \
+                  -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)")
+            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' \
+                "$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")
+            fi
+          done
+
+          if [ "${#repinned[@]}" -gt 0 ]; then
+            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[@]}")")
+            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)"
+            exit 1
+          fi

Marches/Cut.lean

@@ -34,7 +34,7 @@
                                      `Interface` of `Compose.lean` (the
                                      2-node DAG `Reassembly.boolUp`).
 
-  Provenance. choreographic-types (pinned at edb784a) proves the cut side
+  Provenance. choreographic-types (pinned in scripts/fetch-siblings.sh) proves the cut side
   for global choreographies in Agda: `Choreographic.Global.Cut`,
   `KCut.proj-cut`, `KCut.cut-projectable`. The relation between those
   names and these is a table, not a link (docs/kcut-correspondence.adoc).

Marches/Tropical.lean

@@ -12,7 +12,7 @@
   import: OPEN (rung 3 in ROADMAP.adoc). Nothing here fabricates or
   depends on that file's contents.
 
-  The cross-prover bridge is resource-algebra's M-2 (pinned at cf9235c):
+  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,
   port-and-reprove, with no mechanical link. `TropicalNat` below is
   min-plus, not max-plus, so it is not one of M-2's two objects; see
@@ -46,7 +46,7 @@ theorem tropical_no_return (l : Nat) (ls : List Nat) (a : Nat) :
   `TropicalNat` read as a (min, +) grade, in the path algebra's own terms:
   alternatives keep the cheaper route (`better` is `<`), sequencing adds
   costs, and the unit of sequencing is cost `0`, the grade of the empty
-  word. choreographic-types (pinned at edb784a) records that K-CUT-LOSS
+  word. choreographic-types (pinned in scripts/fetch-siblings.sh) records that K-CUT-LOSS
   uses exactly two laws, `𝟙 ⊗ x ≡ x` and `x ⊕ x ≡ x` (K-4, TESTED there
   by `scripts/minimal-laws.sh`). Both hold here. Whether this reading
   agrees with any Agda instance is a cross-prover question: ASSUMED,
@@ -80,9 +80,9 @@ theorem label_cost_ne_one (w : Nat) : w + 1 ≠ one := fun h => Nat.noConfusion
 theorem alt_of_better {a b : Nat} (h : TropicalNat.better a b) : alt a b = a :=
   Nat.min_eq_left (Nat.le_of_lt h)
 
-/-- The order `alt` induces, in resource-algebra's convention at cf9235c
-    (`a ≼ b` when `b` absorbs `a`). It is defined here for marches' own
-    grade; it is NOT the Agda `_≼_`, and no link between them is claimed. -/
+/-- The order `alt` induces, in resource-algebra's convention (read at
+    cf9235c, 2026-10-14: `a ≼ b` when `b` absorbs `a`). It is defined here for
+    marches' own grade; it is NOT the Agda `_≼_`, and no link between them is claimed. -/
 def altLe (a b : Nat) : Prop := alt a b = b
 
 /-- S-3 inside marches: `better` runs WITH cost, the induced order runs

README.adoc

@@ -182,6 +182,15 @@ at their pinned commits (into `_build/dependencies`). It checks that every
 name `docs/kcut-correspondence.adoc` cites exists, and it needs network
 access.
 
+Pins track latest, weekly, through reviewed PRs:
+
+* `actions-lock.yml` relocks `.github/workflows/actions.lock`.
+* `track-lean.yml` tries the newest stable Lean against the three gates.
+* `track-siblings.yml` re-checks the correspondence against each sibling's
+  HEAD and re-pins when every name still exists.
+
+A red result opens an issue instead of a PR.
+
 == Module map
 
 * `Marches/Basic.lean` — path algebras, strict/non-strict inflation, `run`.

ROADMAP.adoc

@@ -61,9 +61,12 @@ are refused
 |met 2026-10-14 (names only; F6 open)
 
 |3d. Import the estate's fully proved `TropicalAdapterPath.lean` behind
-the `Marches/Tropical.lean` seam. Do NOT paraphrase it; vendor or depend
-on it. It lives in hyperpolymath/tropical-types (lake package
-`tropical-resource-typing`) at `e172f8a`, on Lean v4.13.0.
+the `Marches/Tropical.lean` seam. Do NOT paraphrase it. It lives in
+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.
 |—
 |it builds inside this repo on the pinned toolchain, unparaphrased
 |OPEN

STATE.adoc

@@ -15,8 +15,25 @@
 * `.github/workflows/actions-lock.yml` (new, no `uses:`) runs
   `github/gh-actions-lock v0.2.0 --relock` remotely. It triggers on pushes to
   main that change a workflow, weekly, and on dispatch. It is scoped to the
-  workflows the lock already tracks plus every workflow with no `uses:`, and opens a PR only when
-  `actions.lock` alone changes.
+  workflows the lock already tracks plus every workflow with no `uses:`, and
+  opens a PR only when `actions.lock` alone changes.
+* Track latest (maintainer preference: everything updated and checked
+  against latest). Two weekly workflows, neither with `uses:`; Lean comes
+  from elan's installer.
+  - `track-lean.yml`: tries the latest stable Lean and runs the three gates.
+    Green → a PR (toolchain, README, STATE entry); red → an issue. Dry run
+    here on v4.35.0: `Build completed successfully (15 jobs).`, `sorry`
+    grep empty, `#eval orbit` unchanged, so the first run opens a v4.35.0
+    PR.
+  - `track-siblings.yml`: runs `check-correspondence.sh` against each
+    sibling's HEAD. Green → one re-pin commit per sibling in one PR; a
+    missing name → an issue, pin unchanged. Dry run here:
+    choreographic-types `edb784a`→`ec08c7a` PASS, resource-algebra
+    `cf9235c`→`638dd3e` PASS, tropical-types current. Names only; F6 still
+    needs the diff read.
+  - Lean headers now point at `scripts/fetch-siblings.sh` instead of naming
+    a pin, so a re-pin leaves no stale SHA in prose.
+* 3d decided: depend on tropical-types, tracking latest (ROADMAP).
 * Gates: actionlint 1.7.7 (with shellcheck) clean. The run itself can only
   be exercised on GitHub, because this sandbox cannot reach the GitHub API.