diff --git a/.claude/skills/ci-gates/incoming/2026-09-05-a-control-can-pass-while-deleting-the-thing-it-tested.md b/.claude/skills/ci-gates/incoming/2026-09-05-a-control-can-pass-while-deleting-the-thing-it-tested.md new file mode 100644 index 0000000000..c6965688b8 --- /dev/null +++ b/.claude/skills/ci-gates/incoming/2026-09-05-a-control-can-pass-while-deleting-the-thing-it-tested.md @@ -0,0 +1,42 @@ +## a control can pass while deleting the thing it tested + +A guard needed a control: does a real fold, with a spool file committed on the +base, pass? Building that needs two commits, so the control made them: + +```sh +git add -A && git commit -m "probe: spool a control lesson" +BASE=$(git rev-parse HEAD) +...fold... +git add -A && git commit -m "probe: fold it" +git reset -q --hard "$BASE~1" # tidy up +``` + +All four controls passed, including the sharpest one. The commit went out, the +PR body described the change, and the change **was not in it**. + +`git add -A` swept an uncommitted fix into the probe's first commit, and +`git reset --hard "$BASE~1"` then threw that commit away. The controls exercised +the fix — they ran against a binary built from it — and then the cleanup +removed it. Nothing failed. `git status` was clean afterwards, because the +working tree matched the commit the reset had chosen. + +It surfaced only from reading the pushed tree directly: + +``` +body claims the skill_files fix: 1 +branch has it: 0 +``` + +Two rules. **A probe must not stage with `-A`**: name the paths, so an unrelated +edit cannot be swept into a commit that is about to be discarded. And **a +control passing is not evidence the code is still there** — it is evidence about +a binary, at a moment. The claim "this PR contains X" is answered by +`git cat-file -p :`, not by a green control. + +This is the second time in one session that a git command chosen for safety +destroyed real work; the other was `git checkout HEAD@{1} -- `, which +restored clean versions over the edits it was meant to protect. Both were +cleanup steps, both ran without error, and both were invisible until the tree +was read on purpose. + +Related: [[the-population-is-the-spelling-on-disk-not-the-one-you-joined]]. diff --git a/.claude/skills/ci-gates/incoming/2026-09-05-a-diagnosis-ages-and-two-of-my-four-did-not-survive-the-log.md b/.claude/skills/ci-gates/incoming/2026-09-05-a-diagnosis-ages-and-two-of-my-four-did-not-survive-the-log.md new file mode 100644 index 0000000000..b0b12cf1ec --- /dev/null +++ b/.claude/skills/ci-gates/incoming/2026-09-05-a-diagnosis-ages-and-two-of-my-four-did-not-survive-the-log.md @@ -0,0 +1,34 @@ +## a diagnosis ages, and two of my four did not survive the log + +Four workflows were carried forward from one pass to the next as recorded FIXes, +each with a written cause. Re-reading the actual runs before editing anything, +**two of the four were wrong**: + +| workflow | recorded | what the evidence said | +|---|---|---| +| `coq-proofs.yml` | OPAMROOT + `opam env` | correct | +| `brain-seal-refresh.yml` | drop the push step | correct | +| `lean-proofs.yml` | "two Lean targets, keep `--wfail`" | **wrong** | +| `release.yml` | never green, restrict the trigger | **wrong premise** | + +`lean-proofs` is not misconfigured. 8571 of 8574 targets build, and the two that +fail carry comments in the source saying so: + +``` +-- LEFT FAILING, DELIBERATELY. H4Lagrangian.lean:73 +-- LEFT FAILING, DELIBERATELY, AND THIS IS THE ONLY ONE. H4Lagrangian.lean:108 +``` + +`release.yml` was on a *never-green* list while run `33180327861` had succeeded +on 2026-08-28, publishing `t27c 0.2.0`. And one of its two recent failures is a +`release` whose tag names no product — the product gate working as designed. + +A diagnosis is a reading taken at a moment, and it decays two ways: the subject +changes, and the diagnosis was never right. Neither is visible from the note. +The cost of re-reading the log is one command per workflow; the cost of not +doing it is shipping an edit against a cause that is not there. + +**Re-read the failure before applying a stored fix — including one you wrote.** +The list to be suspicious of is the one where every entry is marked FIX, because +that is the shape a list takes when it was written to be actioned rather than +measured. diff --git a/.claude/skills/ci-gates/incoming/2026-09-05-a-repair-reveals-the-defect-standing-behind-it.md b/.claude/skills/ci-gates/incoming/2026-09-05-a-repair-reveals-the-defect-standing-behind-it.md new file mode 100644 index 0000000000..ff82269317 --- /dev/null +++ b/.claude/skills/ci-gates/incoming/2026-09-05-a-repair-reveals-the-defect-standing-behind-it.md @@ -0,0 +1,33 @@ +## a repair reveals the defect standing behind it + +`coq-proofs.yml` had never passed. The cause was exact and the log stated it: +`options: --user root` runs the container as root, the coqorg image initialises +opam for the `coq` user under `/home/coq/.opam`, so `OPAMROOT` defaulted to +`/root/.opam` and opam reported `[ERROR] Opam has not been initialised`, exit 20. + +Setting `OPAMROOT` fixed that. The job then failed anyway, in the same step, on +something else entirely: + +``` +[ERROR] Package conflict! + * Missing dependency: + - coq-interval = 4.9.0 -> coq < 8.19~ +No solution found, exiting +``` + +The pin asks for a package requiring a Coq **older than the image it runs on** +(`coqorg/coq:8.19`). It could never have installed. But opam never got as far as +computing a solution, so the conflict had never once been printed in this +repository's history. + +The rule: **a workflow that fails early hides every defect after the first**, and +the count of defects is not knowable until the first is repaired. "Fixed" and +"green" are different claims. Reporting the first as the second is how a repair +gets recorded as done while the job stays red. + +The corollary for effort: the second failure is not evidence the first diagnosis +was wrong. Here the first fix demonstrably worked — opam went from refusing to +start to synchronising both repositories — and the reward for that was a new, +truer error message. + +Related: [[a-trigger-that-omits-its-own-file-cannot-verify-its-own-repair]]. diff --git a/.claude/skills/ci-gates/incoming/2026-09-05-a-trigger-that-omits-its-own-file-cannot-verify-its-own-repa.md b/.claude/skills/ci-gates/incoming/2026-09-05-a-trigger-that-omits-its-own-file-cannot-verify-its-own-repa.md new file mode 100644 index 0000000000..0ddbee24e0 --- /dev/null +++ b/.claude/skills/ci-gates/incoming/2026-09-05-a-trigger-that-omits-its-own-file-cannot-verify-its-own-repa.md @@ -0,0 +1,30 @@ +## a trigger that omits its own file cannot verify its own repair + +`coq-proofs.yml` listed itself in `push:`: + +```yaml + push: + paths: + - 'proofs/trinity/**.v' + - '.github/workflows/coq-proofs.yml' + pull_request: + paths: + - 'proofs/trinity/**.v' # <-- and NOT itself +``` + +The two triggers disagreed, and only the `pull_request` side matters to someone +fixing it: **a PR that repairs this workflow does not run it.** Any repair +therefore ships unverified, is reported as done, and the workflow stays broken. +That is a plausible account of how this one stayed red from August. + +Adding the file to `pull_request` paths is what made the next PR self-checking — +and it immediately earned its keep by proving the first repair incomplete rather +than letting it merge as finished. + +This is the same shape as a gate whose `paths:` is narrower than its subject, +with one extra turn: the subject here is *the workflow itself*, so the omission +specifically disables the case where someone is trying to fix it. The failure +mode is silent and self-perpetuating. + +Check both triggers list the workflow file whenever either does. A disagreement +between `push:` and `pull_request:` paths is the signature. diff --git a/.claude/skills/ci-gates/incoming/2026-09-05-the-population-is-the-spelling-on-disk-not-the-one-you-joine.md b/.claude/skills/ci-gates/incoming/2026-09-05-the-population-is-the-spelling-on-disk-not-the-one-you-joine.md new file mode 100644 index 0000000000..7ecd65300b --- /dev/null +++ b/.claude/skills/ci-gates/incoming/2026-09-05-the-population-is-the-spelling-on-disk-not-the-one-you-joine.md @@ -0,0 +1,33 @@ +## the population is the spelling on disk, not the one you joined + +`skill_files()` built its population by joining a name: + +```rust +let p = e.path().join("SKILL.md"); +if p.is_file() { out.push(p); } +``` + +Five skill files are tracked in this repository and **two are spelled +`skill.md`**. On Linux that reads 3 of 5. On a case-insensitive filesystem it is +worse than missing them: `is_file()` returns true, and the path pushed is one +**git has never heard of** — so `git show origin/master:` fails and the +file reads as newly added rather than as tracked. + +The fix is to take the name that is there rather than assert one: + +```rust +for f in std::fs::read_dir(e.path())?.flatten() { + if f.file_name().eq_ignore_ascii_case("SKILL.md") { out.push(f.path()); break; } +} +``` + +Both lowercase files carry **zero** numbered headings, so the missing population +was empty and no past check gave a wrong answer. That is luck, not design: the +first numbered heading added to either would have been unguarded, and the gate +would have kept printing a clean result over it. + +Two habits fall out. **Enumerate, do not construct** — read the directory and +filter, rather than composing a path and testing it. And when a population turns +out to have been short, **say whether the missing part was empty**, because "the +gate read 3 of 5" and "the gate was wrong" are different findings and only one +of them is true here. diff --git a/docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md b/docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md new file mode 100644 index 0000000000..cf59f72f0c --- /dev/null +++ b/docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md @@ -0,0 +1,6 @@ +# NOW -- four lessons spooled, and deliberately not folded (2026-09-06) + +## four lessons spooled, and deliberately not folded (Refs #3236) + +- Four lessons from this pass written with tri skill add. Not folded: a branch that runs add AND fold picks its number against its own base and collides exactly like a direct append, which is what the new guard refuses. Folding belongs after the merge. +- The spool already held one file from an earlier pass, so it is accumulating as designed rather than being a tool nobody reaches for.