gHashTag · gHashTag · Sep 5, 2026 · Sep 5, 2026
@@ -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 <head>:<file>`, 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} -- <files>`, 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]].
@@ -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.
@@ -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]].
@@ -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.
@@ -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:<path>` 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.
@@ -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.