CI: run the full main lane on demand (workflow_dispatch), writing nothing of main's

.github/workflows/ci.yml

@@ -12,6 +12,17 @@ on:
   # true on push AND on merge_group — never `== 'push'`.
   merge_group:
     types: [checks_requested]
+  # The full main lane on demand, for a long-lived branch before it enters the
+  # queue: `gh workflow run ci.yml --ref <branch>` (docs/CI.md, #1787). A
+  # dispatch is not a pull request, so every heavy worker runs as on a push to
+  # main. It runs the DISPATCHED ref's own copy of this file, so what follows
+  # holds for main's text; a branch that edits it can change it, exactly as its
+  # pull request run already could. In this text the one name main owns that is
+  # written here, the rolling ci-main tag, moves only on a push to
+  # refs/heads/main at main's tip; every non-fork ref pushes its own ci-<sha>.
+  # tools/ci_tier_check.sh checks those properties ([ci-main], [writer-actions],
+  # [secrets]).
+  workflow_dispatch:
 
 permissions:
   contents: read
@@ -26,14 +37,22 @@ permissions:
 env:
   ASAN_SHARDS: 3
 
-# Only one CI run per ref in flight: a new push (or PR update) cancels the
-# older run for the same branch. Prevents superseded/hung runs from piling
+# One run per concurrency group in flight: a new push to main (or a PR update)
+# cancels the older run in its group. Prevents superseded/hung runs from piling
 # up (2026-08-18: three main-push runs — 214m/118m/81m — alive at once after
 # a valgrind flake, none superseding the others). Pairs with the per-job
 # timeout-minutes, which bounds a single hang; this bounds the *fan-out*.
+# A dispatch has its own group (`ci-dispatch-<ref>`), apart from push, PR and
+# merge-queue runs, main's included. GitHub compares group names
+# case-insensitively, so refs differing only in case share one. A dispatch is
+# never cancelled in progress: a newer dispatch on the same ref waits, and a
+# third replaces the waiting one before it starts any job. So no cancelled
+# dispatch leaves its `if: always()` aggregators failing under required names.
+# Nothing else stops a running dispatch either, a later push to its branch
+# included: cancel it with `gh run cancel <run-id>`.
 concurrency:
-  group: ci-${{ github.event.pull_request.number || github.ref }}
-  cancel-in-progress: true
+  group: ci-${{ github.event_name == 'workflow_dispatch' && format('dispatch-{0}', github.ref) || github.event.pull_request.number || github.ref }}
+  cancel-in-progress: ${{ github.event_name != 'workflow_dispatch' }}
 
 # Pull requests run the release suite plus build, lint/LSP, self-test,
 # precheck, and docs gates. Heavy variants report their required names with a
@@ -121,28 +140,41 @@ jobs:
 
       # GHCR requires a lowercase owner; compute the ref once and hand it to
       # the downstream jobs through a job output. `image` is what the Linux
-      # legs run in; `tags` is what this job pushes (empty on fork PRs —
-      # nothing is pushed; main pushes also advance the rolling ci-main tag).
+      # legs run in; `tags` is what this job pushes: empty on fork PRs, this
+      # commit's ci-<sha> on every other run, and the rolling ci-main tag on a
+      # push to main at main's tip only. tools/ci_tier_check.sh runs this step
+      # across event x ref x tip to check that ([ci-main]).
       - name: Compute image ref
         id: ref
         env:
           OWNER: ${{ github.repository_owner }}
           IS_FORK: ${{ github.event.pull_request.head.repo.fork == true }}
-        # The event is read from the runner's GITHUB_EVENT_NAME, not an
-        # expression: tools/ci_tier_check.sh reds event-derived expression
-        # values on a required path (#1264). Only push advances ci-main.
+        # The event and ref are read from the runner's GITHUB_EVENT_NAME and
+        # GITHUB_REF, not expressions: tools/ci_tier_check.sh reds
+        # event-derived expression values on a required path (#1264). Only a
+        # push to main whose SHA is main's tip moves ci-main: a dispatch from
+        # any ref, main included, and a re-run of an older push push only
+        # ci-<sha>. Do not gate on GITHUB_RUN_ATTEMPT: a re-run at the tip is
+        # legitimate. Keep it bash-3.2 clean (tr, not ${OWNER,,}): precheck runs
+        # it, and macOS ships bash 3.2.
         run: |
-          BASE="ghcr.io/${OWNER,,}/eigenscript-dev"
+          BASE="ghcr.io/$(printf %s "$OWNER" | tr '[:upper:]' '[:lower:]')/eigenscript-dev"
+          SHA="${{ github.sha }}"
           if [ "$IS_FORK" = "true" ]; then
             echo "image=$BASE:ci-main" >> "$GITHUB_OUTPUT"
             echo "tags=" >> "$GITHUB_OUTPUT"
-          elif [ "$GITHUB_EVENT_NAME" = "push" ]; then
-            echo "image=$BASE:ci-${{ github.sha }}" >> "$GITHUB_OUTPUT"
-            echo "tags=$BASE:ci-${{ github.sha }},$BASE:ci-main" >> "$GITHUB_OUTPUT"
-          else
-            echo "image=$BASE:ci-${{ github.sha }}" >> "$GITHUB_OUTPUT"
-            echo "tags=$BASE:ci-${{ github.sha }}" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          TAGS="$BASE:ci-$SHA"
+          if [ "$GITHUB_EVENT_NAME" = "push" ] && [ "$GITHUB_REF" = "refs/heads/main" ]; then
+            # Move ci-main only while this SHA is main's tip, so re-running an
+            # older push run cannot point it back at an older image.
+            tip=$(git ls-remote origin refs/heads/main | cut -f1)
+            [ -n "$tip" ] || { echo "::error::cannot read main's tip; ci-main not moved"; exit 1; }
+            if [ "$tip" = "$SHA" ]; then TAGS="$TAGS,$BASE:ci-main"; else echo "main has moved to $tip: ci-main stays"; fi
           fi
+          echo "image=$BASE:ci-$SHA" >> "$GITHUB_OUTPUT"
+          echo "tags=$TAGS" >> "$GITHUB_OUTPUT"
 
       - name: Build and push dev image
         if: github.event.pull_request.head.repo.fork != true
@@ -207,6 +239,9 @@ jobs:
         run: |
           git config --global --add safe.directory "$GITHUB_WORKSPACE"
           base='${{ github.event.pull_request.base.sha || github.event.merge_group.base_sha || github.event.before }}'
+          # A workflow_dispatch carries no base: select what the dispatched ref
+          # changes against main, as its PR would. An empty base selects nothing.
+          [ -n "$base" ] || base=origin/main
           bash tools/selftests.sh --changed "$base" --list > selection.txt
           cat selection.txt
           n=$(sed -n 's/^selftests: enrolment .*; \([0-9][0-9]*\) self-tests selected$/\1/p' selection.txt)
@@ -1530,12 +1565,20 @@ jobs:
         # not origin/main — otherwise a PR is charged for the Ir cost of the PRs
         # ahead of it and falsely rejected (#1273 code review). Read from the
         # event payload inside the script, never via ${{ }} (tier gate rule).
+        # On a dispatch the baseline is the branch's merge-base with main: the
+        # branch's own changes, as the queue will measure them, not main's
+        # changes since the fork counted against it (or hiding its own).
         run: |
           base=origin/main
           if [ "$GITHUB_EVENT_NAME" = merge_group ]; then
             base=$(jq -r '.merge_group.base_sha' "$GITHUB_EVENT_PATH")
             [ -n "$base" ] && [ "$base" != null ] || { echo "merge_group event without base_sha"; exit 1; }
             git fetch --no-tags --depth=1 origin "$base"
+          elif [ "$GITHUB_EVENT_NAME" = workflow_dispatch ]; then
+            if [ "$(git rev-parse --is-shallow-repository)" = true ]; then git fetch --no-tags --unshallow origin main
+            else git fetch --no-tags origin main; fi
+            base=$(git merge-base origin/main HEAD)
+            echo "dispatch: the merge-base of $GITHUB_REF with origin/main ($(git rev-parse origin/main)) is $base"
           else
             git fetch --no-tags --depth=1 origin main
           fi

README.md

@@ -3,7 +3,7 @@
 </p>
 
 <p align="center">
-  <a href="https://github.com/InauguralSystems/EigenScript/actions/workflows/ci.yml"><img src="https://github.com/InauguralSystems/EigenScript/actions/workflows/ci.yml/badge.svg" alt="CI"></a>
+  <a href="https://github.com/InauguralSystems/EigenScript/actions/workflows/ci.yml"><img src="https://github.com/InauguralSystems/EigenScript/actions/workflows/ci.yml/badge.svg?branch=main&event=push" alt="CI"></a>
   <a href="https://github.com/InauguralSystems/EigenScript/releases/latest"><img src="https://img.shields.io/github/v/release/InauguralSystems/EigenScript" alt="Release"></a>
   <a href="LICENSE"><img src="https://img.shields.io/badge/license-MIT-green" alt="License: MIT"></a>
   <a href="https://github.com/InauguralSystems/EigenScript/stargazers"><img src="https://img.shields.io/github/stars/InauguralSystems/EigenScript?cacheSeconds=3600" alt="Stars"></a>

docs/CI.md

@@ -189,6 +189,66 @@ on the commit that will land, before it lands — see **Platform tiers** below.
 #1138 and #1158 both carried lanes only CI could run. Contributors never wait
 on it and never rebase to satisfy it; the queue does both.
 
+### The main lane on demand (`workflow_dispatch`)
+
+A long-lived branch, such as an integration branch that lives through many
+review rounds, can run the full main lane before it enters the queue (#1787):
+
+    gh workflow run ci.yml --ref <branch>
+    gh run list --workflow ci.yml --event workflow_dispatch --branch <branch>
+    gh run list --workflow ci.yml --commit <sha>
+
+- **What runs.** A dispatch is not a pull request, so every job runs as on a
+  push to `main`. That includes every heavy worker: the ASan shards, both TSan
+  variants, the native macOS suite, valgrind, the bench gate, the extension
+  suites and the db lane.
+  - The bench gate measures the branch against its merge-base with `main`, so
+    the branch is charged for its own changes, as the queue will measure them.
+  - The changed-gate self-tests select what the branch changes against `main`.
+- **When.** Dispatch on an integration branch before it is queued, and again
+  after a rebase that pulls in a lot. The queue still runs everything on the
+  candidate commit, so a dispatch is never a substitute for it.
+- **Which `ci.yml` runs.** The dispatched ref's own copy, with its own
+  `tools/ci_tier_check.sh`. What follows holds for `main`'s text. A branch that
+  edits `ci.yml` can change it, exactly as its pull-request run already could,
+  since a pull request also runs the branch's own workflow file.
+- **What it writes.** In `main`'s `ci.yml`, the only job that can write is
+  `build dev/ci image`:
+  - Every non-fork run pushes the commit's own `ci-<sha>` image tag, a
+    dispatch included.
+  - The rolling `ci-main` tag is the one name written here that `main` owns
+    (fork PRs run in it). It moves only on a push to `main` whose SHA is still
+    `main`'s tip, so neither a dispatch from any ref nor a re-run of an older
+    push moves it (`[ci-main]`, below).
+  - The build cache goes to the run's ref scope. A dispatch on a branch writes
+    the branch's scope; a dispatch on `main` writes `main`'s, as a push does.
+  - Artifacts stay in the run.
+
+  A dispatch on `main` also adds runs to `main`'s commit, but the README badge
+  reads only push runs (`badge.svg?branch=main&event=push`).
+- **Concurrency.** There is one run per concurrency group.
+  - A dispatch's group is `ci-dispatch-<ref>`, separate from push,
+    pull-request and merge-queue runs, `main`'s included. GitHub compares group
+    names case-insensitively, so refs that differ only in case share one.
+  - The group never cancels a running dispatch. A newer dispatch on the same
+    ref waits, and a third replaces the waiting one before it starts any job.
+  - A later push to the branch does not stop a dispatch either. To drop an
+    outdated one, run `gh run cancel <run-id>` and dispatch again. A cancelled
+    run's `if: always()` aggregators then conclude failure under their required
+    names on that commit; that failure records the cancellation, not a test
+    result.
+- **Where the results show.** In the dispatch run itself: `gh run view
+  <run-id>`, or `gh run list --commit <sha>`. GitHub's status rollup for a
+  commit, which pull requests and the queue read, leaves out `workflow_dispatch`
+  suites. (Measured: a commit that carries only a dispatch's 49 check runs has
+  no rollup at all.) So a dispatch neither appears among a pull request's
+  checks nor gates it.
+
+GitHub reads the trigger from the dispatched ref's own copy of `ci.yml`. A
+branch whose copy predates the trigger is refused with HTTP 422, "Workflow
+does not have 'workflow_dispatch' trigger" (measured on a stale branch). So
+rebase or merge `main` into a long-lived branch before its first dispatch.
+
 ## Nightly (`.github/workflows/nightly.yml`)
 
 - `macos-15-intel`, the full suite — the 35-minute job that used to set the PR
@@ -478,8 +538,9 @@ index headers and compiles `eigenlsp.c` with the trio in its flag bundle.
 Main CI did not finish green from 2026-09-16 to 2026-09-22 although every
 required check passed on every merge: one lane that no pull request had to pass
 (`macos / macos-15-intel`, main lane only) hit its timeout on nearly every
-push. The README badge is the status of the whole `ci.yml` workflow on `main`,
-so **any** `ci.yml` job that can fail there colours it, required or not.
+push. The README badge is the status of the whole `ci.yml` workflow's latest
+push run on `main` (`badge.svg?branch=main&event=push`), so **any** `ci.yml`
+job that can fail there colours it, required or not.
 
 The fix copies Rust (tiers plus a merge queue), CPython and Go:
 
@@ -541,7 +602,14 @@ self-tests` job. A missing PyYAML is exit 2, never a pass.
   those must use exactly `github.event_name != 'pull_request'`. A step `if:`
   may mention the event only as `github.event_name ==/!= 'pull_request'`, or
   via the PR payload `github.event.pull_request.*` (empty on push and in the
-  queue alike). Dot and bracket syntax are both read. The same rule covers
+  queue alike). Beyond those two forms, a condition may read only the `github`
+  fields whose value does not depend on the event that started the run:
+  `repository`, `repository_owner`, `repository_id`,
+  `repository_owner_id`, `server_url`, `api_url`, `graphql_url`, `workspace`,
+  `workflow`, `job`, `action`, `token` and `retention_days`. Any other field
+  (such as `ref_protected`, `workflow_ref`, `sha` or `actor`), or a bare
+  `github`, is red: that is an allowlist (#1787), not a list of known event
+  fields. Dot and bracket syntax are both read. The same rule covers
   indirection: an `env`, job `outputs`, workflow `env` or matrix value on a
   required path may not read the event (outside those two forms), and an
   `if:` that reads `env.*`, `needs.*.outputs` or `steps.*.outputs` is traced
@@ -559,6 +627,48 @@ self-tests` job. A missing PyYAML is exit 2, never a pass.
 - `[uncovered]` — a `ci.yml` job is neither required nor the worker of exactly
   one required `if: always()` aggregator. A failing non-required job does not
   stop the queue, yet it colours the badge: the `macos-15-intel` shape.
+- `[ci-main]` — `ci-main` is the one name `ci.yml` writes that `main` owns.
+  The check finds the step that computes the image push's tags and runs it,
+  under `bash -e`, across every event (push, pull request, merge queue,
+  dispatch), ref (`main`, a branch, a pull request's merge ref, the queue's
+  ref) and tip state (this SHA is `main`'s tip, is not, or the tip cannot be
+  read), plus fork pull requests. It requires `ci-main` exactly on a push to
+  `refs/heads/main` at `main`'s tip. Every non-fork run pushing its own
+  `ci-<sha>` is by design.
+  - `on.push` must be exactly `branches: [main]`.
+  - Each image push must take its tags from that one step.
+  - The matrix runs the step with the workflow, job and step env merged as the
+    runner merges them, and reads its `tags` output in any case, quotes
+    stripped.
+  - The check refuses what its matrix cannot model:
+    - a custom shell or directory (`defaults:`, `shell:`,
+      `working-directory:`);
+    - env in any scope that redirects bash or git (`PATH`, `BASH_ENV`, `ENV`,
+      `SHELLOPTS`, `BASHOPTS`, `GITHUB_*`, `GIT_*`, `BASH_FUNC_*`, `LD_*`);
+    - an expression it cannot evaluate;
+    - a multi-line `tags<<` output.
+- `[writer-actions]` — a `ci.yml` job that can write uses only the allowlisted
+  actions `actions/checkout`, `docker/setup-buildx-action`,
+  `docker/login-action` and `docker/build-push-action`.
+  - The allowlist compares action identities without the `@ref`, so a
+    Dependabot bump stays green.
+  - Each action takes only the inputs vetted for it. So
+    `docker/build-push-action` takes no `outputs:` and only a `type=gha`
+    `cache-to:`: an `outputs:` or a registry cache can push to any name, and a
+    registry cache is shared across refs.
+  - A new input goes red until someone vets it and adds it to `INPUTS`.
+  - No `./` or `docker://` action, and no reusable-workflow call.
+  - No script except the tag step that `[ci-main]` runs.
+
+  A job can write when it holds a write permission: its own, or the workflow's,
+  where a missing block counts as the repository default, which may write.
+- `[secrets]` — `ci.yml` reads no secret but `secrets.GITHUB_TOKEN`, in dot or
+  bracket syntax, and passes none to a reusable workflow. So `permissions:`
+  alone decide what it can write.
+
+These rules were each proven once, when written, against planted copies
+recorded in PR #1785 (`docs/PRINCIPLES.md` §5); none is re-proven on every
+run.
 
 Whether an aggregator's script really fails on every non-success worker
 result remains a code-review question. The gate's other accepted limits
@@ -626,7 +736,9 @@ The suite runs each gate's live check; `tools/selftests.sh --changed origin/main
 runs checker self-tests whose scripts, fixtures or helpers changed, including
 uncommitted and untracked files, and `make precheck` includes that selection.
 The required `gate self-tests (changed rows)` check uses the
-PR base SHA or merge-group base SHA, while nightly runs `tools/selftests.sh --all`
+PR base SHA or merge-group base SHA, the pushed range on `main`, or
+`origin/main` on a `workflow_dispatch` (which carries no base SHA), while
+nightly runs `tools/selftests.sh --all`
 and reports failures through its tracking issue.
 `tools/selftests.txt` owns the trigger globs, bounded commands and existing
 result pins; changing it or the driver selects every row.