Every workflow red on master, diagnosed: 5 fixable, 4 leave, 1 wrong trigger, 0 to delete

[gHashTag]

Nine workflows on the default branch have never once been green, some since
April. The question nobody had asked: how many of them should exist at all?

Fanned tri red why (#3271) across all ten red workflows, one agent each, with
an adversarial stage set to attack any DELETE or DISABLE.

recommendation	count
FIX	5
LEAVE	4
RESTRICT_TRIGGER	1
DELETE / DISABLE	0

class	count
GENUINELY_BROKEN	7
MISSING_SECRET_OR_RUNNER	2
WRONG_TRIGGER	1

Nothing should be removed. The refutation stage had nothing to check,
because no agent proposed removing a check — every one of these either guards
something real or is red for a reason outside the repository.

The five fixable

build-paper.yml — one character. main.tex:278 declares
\begin{tabular}{lll} for a table whose header and four body rows all carry
four columns. Fixed in #3315.

coq-proofs.yml — the container's opam root. options: --user root gives
HOME=/root, which has no opam root; the image's belongs to the coq user. Set
OPAMROOT: /home/coq/.opam at job level and eval $(opam env) in both run
steps — coqc is not on root's PATH under Actions' non-login shell. Keep
--user root: removing it reintroduces the older checkout-ownership failure.

lean-proofs.yml — two Lean targets. H4Lagrangian.lean has two hard
errors whose file comment blames a missing import that is already there; the
four names it tried are pre-rename spellings, and the bounds exist at the pinned
mathlib rev as Real.pi_gt_d2 / pi_lt_d2 / exp_one_gt_d9 / exp_one_lt_d9.
TernaryInference.lean has 0 errors and 20 warnings, promoted to failure by
--wfail. Keep --wfail; dropping it hides the rot.

brain-seal-refresh.yml — a push that has never succeeded. Its first four
steps pass; only the final Commit brain seals fails, on a PR-only branch where
the push cannot work. Dropping that step and the orphaned contents: write
makes it green as what it can actually be: a check that the aggregation runs and
validates against the schema, with the seals as an artifact. Nothing is lost —
the push has never once succeeded, so it has never refreshed anything.

auto-merge-ready-prs.yml — already fixed in #3314 (zero checks read as
zero failures; a batch that merged nothing reported green).

The one wrong trigger

release.yml carries a bare workflow_dispatch: alongside
release: [published]. The preflight step reads the tag from
github.event.release.tag_name, which a dispatch does not supply, so every
manual fire fails at step 3 — the only reason it is red on master. Deleting the
four-line workflow_dispatch: block loses nothing.

Making the manual trigger actually work is three coupled edits, not one: a
required tag input, a fallback in both TAG: and the concurrency group (which
today collapses to the literal release- for every dispatch), and
github.event_name == 'release' && prepended to the if: of all five publish
jobs — otherwise a dispatch whose tag passes preflight runs cargo publish and
npm publish against the live registries for real. The file header records two
such irreversible burns already. Not recommended.

The four to leave

vivado-synth.yml and build-vivado-image.yml need a Vivado image/licence the
CI does not have — docker pull returns manifest unknown. deploy-api.yml
and issue-gate.yml's master runs are similar: nothing in the repository is
wrong.

---

Each fix is small and independent. Filed as one issue because the population
is the finding: a set of never-green workflows that turns out to contain no dead
weight at all.

[gHashTag]

Pass 118 — the four FIXes, and two corrections to this list

Two of the four were wrong. I re-read every failing run before editing, and the stored diagnoses did not all survive that.

workflow	recorded here	actual
coq-proofs.yml	OPAMROOT + opam env	correct — shipped in #3324, then #3326
brain-seal-refresh.yml	drop the push step	correct — shipped in #3324
lean-proofs.yml	FIX: two Lean targets	withdrawn — not a defect
release.yml	RESTRICT_TRIGGER, never green	premise wrong — shipped in #3325

lean-proofs.yml — withdrawn

8571 of 8574 targets build. The two that fail are marked in the source:

-- LEFT FAILING, DELIBERATELY.                           H4Lagrangian.lean:73
-- LEFT FAILING, DELIBERATELY, AND THIS IS THE ONLY ONE. H4Lagrangian.lean:108

norm_num does not evaluate Real.pi, Real.exp or Real.sqrt. The job is red because it is telling the truth, and this workflow's own header already says that outcome is the finding. Nothing to fix in the workflow; closing the two goals is analysis, not configuration.

release.yml — not never-green

Run 33180327861 succeeded on 2026-08-28, publishing t27c 0.2.0. Of the two recent failures, 33230021436 is a release whose tag names no product — the PRODUCT GATE working as designed. The single false red is a bare workflow_dispatch, on which github.event.release.tag_name is empty so preflight exits 1 and every publishing job is skipped: it cannot publish and cannot measure. Removed in #3325 rather than made to work, because giving preflight a tag input makes preflight succeed on a dispatch, trading a structural guard for five if: conditions in front of live cargo publish/npm publish.

coq-proofs.yml — one repair uncovered a second defect

#3324 fixed OPAMROOT and the job got further: opam now updates both repositories and reaches the solver. It then failed on something that had never been printed in this repository, because opam had never got that far:

[ERROR] Package conflict!
  * Missing dependency:
    - coq-interval = 4.9.0 -> coq < 8.19~
No solution found, exiting

The pin requires a Coq older than the image (coqorg/coq:8.19). 7 of the 13 compiled files Require Import Interval.Tactic, so the dependency is real — only the version can move. Unpinned in #3326, which records what the solver picks so a pin can be restored from a reading.

#3324 also added this workflow to its own pull_request paths. push: listed it and pull_request: did not, so a PR repairing this workflow could not run it and any repair shipped unverified. That is a plausible account of how it stayed broken, and the addition immediately earned its keep by proving the first repair incomplete instead of letting it merge as finished.

Remaining

release.yml FIX-to-working is still not recommended and is now better supported: the pipeline already works on real tags, so a dispatch buys only a rehearsal nobody has asked for, at the cost of weakening a live-publish guard.