[fathom (gale)] — main's branch protection requires zero status checks. CI is advisory: a PR with every check red can be merged.
Measured
gh api repos/pulseengine/gale/branches/main/protection
required_status_checks : { strict: true, contexts: 0 } <- nothing required
required_pull_request_reviews : true
enforce_admins : true
allow_force_pushes : false
gh api repos/pulseengine/gale/rulesets -> (empty)
strict: true means "branch must be up to date before merging" — it does not require anything to pass, because the context list is empty. No ruleset supplies one either.
What this actually means
gh pr view reporting CLEAN / MERGEABLE says there are no conflicts and no failing required checks — and since nothing is required, it says almost nothing about CI. A PR sitting on a red matrix reports CLEAN. That is the trap: the word looks like a verdict and is not one.
The repo runs a genuinely serious gate set — ~60 checks per PR, Verus SMT over 39 modules, Kani BMC over 185 harnesses, 14 Rocq proof targets, the Lean proofs, the gust seam and dissolve gates, the Renode cycle gates. None of it can block a merge. The whole apparatus is opt-in on whoever is pressing the button.
Why I am filing it rather than fixing it
Two reasons.
It is a repo-settings change, not a code change — it needs someone with admin on the repo, and it is the kind of change that should be made deliberately rather than by an agent tidying up. Turning on required checks with the wrong list is worse than none: it can wedge merges on a check that is legitimately skipped for some paths.
Picking the list is a real decision. Most of these workflows have paths: filters, so a check that is required but skipped for a docs-only PR blocks it forever unless the required-check list is chosen to account for that. The honest candidates are the always-run ones — Test + Lint, Verus-Strip Gate, rivet V-closure — with the heavy path-filtered matrices deliberately left advisory, or moved to a merge queue.
Evidence this is not theoretical
I have merged six PRs in this repo today. Every one of them I re-confirmed by hand — gh pr checks <n> showing fails=0 and a full pass count — before merging, because the standing instruction is to never merge over a red. That discipline is the only thing that was enforcing the gate. Had I trusted CLEAN/MERGEABLE, nothing would have stopped a merge over a failing matrix; and today's matrix went red three separate times from unretried network fetches (#289).
I also renamed a check today (Lean Proofs (7 files) -> Lean Proofs) and verified first that no protection rule referenced it. That verification came back empty for the same reason this issue exists.
Kill-criterion
Open a throwaway PR whose only change makes a required check fail, and confirm GitHub refuses the merge — rather than reporting CLEAN and allowing it. Today it allows it.
Related
[fathom (gale)] —
main's branch protection requires zero status checks. CI is advisory: a PR with every check red can be merged.Measured
strict: truemeans "branch must be up to date before merging" — it does not require anything to pass, because the context list is empty. No ruleset supplies one either.What this actually means
gh pr viewreportingCLEAN / MERGEABLEsays there are no conflicts and no failing required checks — and since nothing is required, it says almost nothing about CI. A PR sitting on a red matrix reportsCLEAN. That is the trap: the word looks like a verdict and is not one.The repo runs a genuinely serious gate set — ~60 checks per PR, Verus SMT over 39 modules, Kani BMC over 185 harnesses, 14 Rocq proof targets, the Lean proofs, the gust seam and dissolve gates, the Renode cycle gates. None of it can block a merge. The whole apparatus is opt-in on whoever is pressing the button.
Why I am filing it rather than fixing it
Two reasons.
It is a repo-settings change, not a code change — it needs someone with admin on the repo, and it is the kind of change that should be made deliberately rather than by an agent tidying up. Turning on required checks with the wrong list is worse than none: it can wedge merges on a check that is legitimately skipped for some paths.
Picking the list is a real decision. Most of these workflows have
paths:filters, so a check that is required but skipped for a docs-only PR blocks it forever unless the required-check list is chosen to account for that. The honest candidates are the always-run ones —Test + Lint,Verus-Strip Gate,rivet V-closure— with the heavy path-filtered matrices deliberately left advisory, or moved to a merge queue.Evidence this is not theoretical
I have merged six PRs in this repo today. Every one of them I re-confirmed by hand —
gh pr checks <n>showingfails=0and a full pass count — before merging, because the standing instruction is to never merge over a red. That discipline is the only thing that was enforcing the gate. Had I trustedCLEAN/MERGEABLE, nothing would have stopped a merge over a failing matrix; and today's matrix went red three separate times from unretried network fetches (#289).I also renamed a check today (
Lean Proofs (7 files)->Lean Proofs) and verified first that no protection rule referenced it. That verification came back empty for the same reason this issue exists.Kill-criterion
Open a throwaway PR whose only change makes a required check fail, and confirm GitHub refuses the merge — rather than reporting
CLEANand allowing it. Today it allows it.Related
curl | shrustup installs across 12 workflows — no retry, and no pipefail, so a truncated installer can pass the stage #289 — unretried network fetches turning green matrices red at random. Less dangerous while nothing is required, and more dangerous the moment something is.