Repository navigation
Every workflow red on master, diagnosed: 5 fixable, 4 leave, 1 wrong trigger, 0 to delete #3316
Description
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.
Boundary
.github/workflows/auto-merge-ready-prs.yml.github/workflows/brain-seal-refresh.yml.github/workflows/build-paper.yml.github/workflows/build-vivado-image.yml.github/workflows/coq-proofs.yml.github/workflows/deploy-api.yml.github/workflows/issue-gate.yml.github/workflows/lean-proofs.yml.github/workflows/release.yml.github/workflows/vivado-synth.yml
Activity
skill: I said master was green after reading two of sixty-three workf…
ci: repair the two workflows whose failure was in the workflow (#3324)
gHashTag commentedon Sep 5, 2026
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.
coq-proofs.ymlopam envbrain-seal-refresh.ymllean-proofs.ymlrelease.ymllean-proofs.yml— withdrawn8571 of 8574 targets build. The two that fail are marked in the source:
norm_numdoes not evaluateReal.pi,Real.exporReal.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-greenRun 33180327861 succeeded on 2026-08-28, publishing
t27c 0.2.0. Of the two recent failures,33230021436is areleasewhose tag names no product — the PRODUCT GATE working as designed. The single false red is a bareworkflow_dispatch, on whichgithub.event.release.tag_nameis 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 fiveif:conditions in front of livecargo publish/npm publish.coq-proofs.yml— one repair uncovered a second defect#3324 fixed
OPAMROOTand 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:The pin requires a Coq older than the image (
coqorg/coq:8.19). 7 of the 13 compiled filesRequire 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_requestpaths.push:listed it andpull_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.ymlFIX-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.ci(coq): unpin coq-interval, which required a Coq the image does not …
ci(release): drop a dispatch that can only fail (#3325)
github-actions commentedon Oct 2, 2026
Re-filed as #5569.
An attempt claimed this issue on 2026-09-24 and left an empty branch. A dispatch row that has spent its retry ceiling is released once and then keeps its issue for good, which is the right rule for a third identical failure and the wrong outcome for an issue nobody ever attempted twice. The new issue carries the same work, the same boundary, and today's brief.
Closing this one so the swarm can take the work again.