From f8828bb769f5a31be1782e1a9dc8136d1c368853 Mon Sep 17 00:00:00 2001 From: lab Date: Sun, 6 Sep 2026 01:52:13 +0700 Subject: [PATCH 1/3] skill: spool four lessons from this pass Refs #3236 Written with `tri skill add`, and deliberately NOT folded. A branch that runs `add` and `fold` together still picks its number against its own base and collides exactly like a direct append -- which is what the guard in #3323 refuses, correctly. Folding happens after the merge, on one branch, with the file in front of it. - a repair reveals the defect standing behind it coq-proofs: OPAMROOT fixed the first error and the job then failed on a package conflict that had never been printed in this repository, because opam had never got as far as computing a solution. "Fixed" and "green" are different claims. - a trigger that omits its own file cannot verify its own repair coq-proofs listed itself in `push:` paths and not in `pull_request:`, so a PR repairing it could not run it and any repair shipped unverified. - a diagnosis ages, and two of my four did not survive the log lean-proofs is not misconfigured (the two failures are marked LEFT FAILING, DELIBERATELY in the source) and release.yml was on a never-green list after run 33180327861 succeeded. Re-read the failure before applying a stored fix, including one you wrote. - the population is the spelling on disk, not the one you joined skill_files() read 3 of 5 tracked skill files; 2 are spelled `skill.md`, and on a case-insensitive filesystem it found them under a name git does not have. Both carry zero numbered headings, so the missing population was empty -- luck, not design. The spool already held one file from an earlier pass, so it is accumulating rather than being a tool nobody reaches for. `tri skill spooled --gate` 0 (this branch adds no section) - `skill check` 0 - `skill refs` 0. --- ...-two-of-my-four-did-not-survive-the-log.md | 34 +++++++++++++++++++ ...r-reveals-the-defect-standing-behind-it.md | 33 ++++++++++++++++++ ...its-own-file-cannot-verify-its-own-repa.md | 30 ++++++++++++++++ ...-spelling-on-disk-not-the-one-you-joine.md | 33 ++++++++++++++++++ ...ons-spooled-and-deliberately-not-folded.md | 6 ++++ 5 files changed, 136 insertions(+) create mode 100644 .claude/skills/ci-gates/incoming/2026-09-05-a-diagnosis-ages-and-two-of-my-four-did-not-survive-the-log.md create mode 100644 .claude/skills/ci-gates/incoming/2026-09-05-a-repair-reveals-the-defect-standing-behind-it.md create mode 100644 .claude/skills/ci-gates/incoming/2026-09-05-a-trigger-that-omits-its-own-file-cannot-verify-its-own-repa.md create mode 100644 .claude/skills/ci-gates/incoming/2026-09-05-the-population-is-the-spelling-on-disk-not-the-one-you-joine.md create mode 100644 docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md 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. From 3fe5edea33e4d4cf884fe4778be5486815008c0f Mon Sep 17 00:00:00 2001 From: lab Date: Sun, 6 Sep 2026 01:55:25 +0700 Subject: [PATCH 2/3] skill: spool a fifth lesson -- a control that deleted what it tested Refs #3236 While building the guard in #3323, a control built two commits with `git add -A` and cleaned up with `git reset --hard $BASE~1`. That swept an uncommitted fix into the discarded commit. Every control passed, the PR body described the fix, and the branch did not carry it -- visible only from `git cat-file` on the pushed head. Second instance this session of a git command chosen for safety destroying work, after `git checkout HEAD@{1} -- `. Both were cleanup steps, both exited zero, both were invisible until the tree was read on purpose. --- ...pass-while-deleting-the-thing-it-tested.md | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 .claude/skills/ci-gates/incoming/2026-09-05-a-control-can-pass-while-deleting-the-thing-it-tested.md 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]]. From c430e77dde9983c80bf783d29693391d32c2de48 Mon Sep 17 00:00:00 2001 From: lab Date: Mon, 14 Sep 2026 20:12:12 +0700 Subject: [PATCH 3/3] docs(now): re-date the entry after updating the branch from master The branch was 146 commits behind and the ruleset requires it up to date. The required freshness gate accepts only an entry dated yesterday..tomorrow UTC, and the shape gate requires the heading date to match the filename. The five spooled lessons are unchanged. Refs #3236 Co-Authored-By: Claude Opus 5 --- ...-14-four-lessons-spooled-and-deliberately-not-folded.md} | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) rename docs/now/{2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md => 2026-09-14-four-lessons-spooled-and-deliberately-not-folded.md} (62%) diff --git a/docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md b/docs/now/2026-09-14-four-lessons-spooled-and-deliberately-not-folded.md similarity index 62% rename from docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md rename to docs/now/2026-09-14-four-lessons-spooled-and-deliberately-not-folded.md index cf59f72f0c..069b977a13 100644 --- a/docs/now/2026-09-06-four-lessons-spooled-and-deliberately-not-folded.md +++ b/docs/now/2026-09-14-four-lessons-spooled-and-deliberately-not-folded.md @@ -1,6 +1,10 @@ -# NOW -- four lessons spooled, and deliberately not folded (2026-09-06) +# NOW -- four lessons spooled, and deliberately not folded (2026-09-14) ## 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. + +## Re-dated + +- Written 2026-09-06 and re-dated 2026-09-14, when the branch was updated from master 146 commits behind. The required freshness gate accepts only an entry dated yesterday..tomorrow UTC, and the shape gate requires the heading date to match the filename. The lessons themselves are unchanged.