docs/active-work.md says the dark-test figure "moves with every merge
and must be re-measured, not quoted." That instruction has never had a
tool, so every re-measurement was a hand-rolled `--list` pipeline
written from scratch.
Hand-rolling it is not safe. Writing this lane's census by hand, the
first attempt filtered libtest's list with `/ : test$/` — but the output
is `name: test` with NO space before the colon, so it matched nothing,
reported zero targets, and looked like a clean run. A census that
silently reports nothing is the same failure class as the dark tests
themselves: no signal, presented as a result.
scripts/feature-census diffs `cargo test --list` between two feature
configurations and reports what the second has that the first cannot
see. Its header records each parsing trap, because every one of them was
hit while writing it:
* `name: test` has no space before the colon.
* `--list` also emits `: benchmark` lines.
* cargo's `Running` lines have two shapes — `unittests src/lib.rs` and
`tests/foo.rs` — so a fixed field index handles one and mangles the
other.
* a target with zero tests prints its `Running` line and nothing else,
so counting only test lines DROPS it from the diff — losing exactly
the finding worth surfacing.
* `--list` includes #[ignore]d tests, which are dark in the same sense
but are NOT recovered by adding a feature to an ordinary test job.
That last one needed a second correction after the script was running.
Counting only B's ignored set attributed pre-existing ignores to the
feature: `rope::tests::perf_smoke_*` are ignored under both configs and
are not "dark and ignored." Both sides now get an ignored pass and the
figure is the difference, which is what turns a flat "279 dark" into
"268 recovered by a plain leg, 11 needing --ignored."
The script also corrected a claim in this lane's own framing doc. The
framing said eight test binaries contain zero tests under CI's flags,
derived from a target-count difference (93 vs 101). The truth is that
ELEVEN targets run with zero tests under those flags; eight of them gain
tests under crdt and three are helper binaries with no tests in either
configuration. Two different true statements, and the framing had
merged them.
Fail-closed on a build failure (exit 3) rather than reporting a census.
A configuration that does not compile yields no test list, which is
indistinguishable by counting from "this configuration has no tests" and
would render as a spectacular and entirely false "every test is dark."
That is not a small error; it is a number that would get quoted.
All five documented exit codes are exercised rather than asserted: 0 on
a clean census and a holding --covers claim, 1 when the claim fails
(both for a test present under both configs and for a misspelled name),
2 on usage, 3 on a configuration that fails to build.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
P2 --- the MIXED arm said "OK" and exited 0 while its likeliest cause
is vacuity. Reaching it means cargo failed, at least one `test result:`
line exists, and none says FAILED --- i.e. the named tests may have run
CLEAN against the old tree, the vacuous outcome, with an unrelated
failure supplying the exit status. The message admitted as much while
the exit code contradicted it, so a scripted caller, or a framing doc
quoting "bite exited 0", would record a certified bite. It now exits 4
and is labelled INCONCLUSIVE rather than OK. The exit ladder in the
header gains the code.
While exercising that arm I found the review's stated trigger --- and
my own comment repeating it --- is WRONG, which is worth more than the
fix. `--test A --test B`, where B's swapped file will not build, does
NOT produce MIXED: cargo builds every named target before running any,
so B's build failure stops A from running too and the swapped run
emits no summary at all. Verified by running exactly that shape
against an ancient `tests/m4_acceptance.rs`; it lands in COMPILE, as
it should. What genuinely reaches MIXED is a run that prints summaries
and *then* fails --- doc-tests failing to compile after the lib tests
pass, or a harness dying after its summary line.
So the arm stays as defence but is documented as defensive, and the
ledger lists it as the one path NOT reproduced rather than implying
the validation was complete. Manufacturing a doc-test failure to reach
it would test the arm at the cost of a contrived fixture; saying which
paths were executed and which were not is the more useful record.
Two wording fixes from the same round. The COMPILE message said the
file "does not build against the current tree", but the no-summary
condition also covers a harness that built and then died before
printing one; it now says "produced no test summary (build failure, or
a harness that died before printing one)" so the label never overstates
the observation. And the colour comment no longer overclaims: exporting
CARGO_TERM_COLOR=never defeats an ambient variable, but an explicit
`--color always` in the passed-through args still beats the
environment. Self-inflicted and fail-closed, and now said so.
P1 --- the classifier could mislabel a genuine bite, and this repo
manufactures the trigger. It grepped the swapped run's output for
`^error\[E...\]` / `^error: could not compile`, but a failing test can
print those lines itself: `tests/compile_mode_acceptance.rs:572` has a
fixture that emits `error[E0308]: mismatched types` at column 0, and
any suite that dumps buffer or PTY text on failure does the same. A
clean assertion failure --- the strong evidence --- would then be
stamped `OK (COMPILE)`, "weaker evidence", while the new handoff text
tells the reader to trust the label. The verdict was never wrong; the
label was.
Classification now reads libtest's own summary instead:
`test result: FAILED` present means the harness ran and tests failed;
no `test result:` line at all means nothing ran. A third `MIXED` arm
covers "some target ran clean but cargo still failed", which the
two-way split silently folded into the wrong side. This also removes
two latent portability bugs for free: `\|` alternation in a BRE is a
GNU extension, so on BSD grep every failure would have labelled as
assertion; and cargo's coloured `error:` output would have evaded the
grep entirely. libtest's summary lines stay uncoloured when piped, and
`CARGO_TERM_COLOR=never` is now exported so `--color always` in the
passed-through args cannot break the parse either --- that would
otherwise have zeroed `count_passed` and produced a spurious
NO CONTROL.
Verified rather than reasoned: a test made to print BOTH
`error[E0308]: mismatched types` and ``error: could not compile
`probe` `` at column 0, then failed by swap, is still classified
`OK (assertion)`.
P2 --- the ledger cited a file that is not in the tree. The lane
scoped itself by `TEST_IMPROVEMENT.md` §8, which is untracked and
machine-local: not on `main`, not in this PR's tree. That is a
dangling reference for any other machine, which is the failure this
ledger exists to prevent. The entry is now self-contained and says so;
if that audit is to scope later lanes it needs committing in its own
PR first.
P3 --- a comment records that both runs are captured rather than
streamed, and why, so nobody "fixes" it back to streaming and breaks
the parser. Double blank line before the parked lane collapsed.
Also, on review's prompting: the #165 wiped-round incident is now
UNEXPLAINED, and the handoff says so rather than leaving a gap the
next reader will fill by re-deriving the false mechanism. Work was
lost; not by the cause this file blamed. SIGKILL bypassing the trap
and a stash collision in the same round are both candidates, and the
note declines to pick one.
Lane 6 of the test-improvement arc, pulled ahead of its own priority
list because every later lane's evidence is bite-shaped. A verifier
that cannot fail is worth no more than the claims it certifies.
The defect. The script ran only the SWAPPED tree, so "the tests failed
against the old file" was the only thing it ever checked. It could not
distinguish a load-bearing fix from a broken test: a typo, an unrelated
compile break, or a filter matching nothing all make the swapped run
fail, and each printed `bite: OK`.
The control now asserts two things, because passing alone is not
enough --- `cargo test` with a filter matching zero tests exits 0, and
a compile error in the old tree would then still read as OK:
* the named tests PASS against the working tree, and
* at least one test actually RAN,
exiting 3 as NO CONTROL otherwise. The swapped run additionally
distinguishes `OK (assertion)` from `OK (COMPILE)`, since an old file
that will not build against the current tree is much weaker evidence:
the tests may never have run at all.
Validated on all three paths rather than the happy one alone. A
zero-match filter reports NO CONTROL. A genuine bite --- PR #190's
`rd1`, which is known to fail against `main` --- reports `control OK
--- 1 test(s) pass` then `OK (assertion)`. A test deliberately broken
so it fails on BOTH trees reports NO CONTROL at exit 3; the previous
script printed `bite: OK` for exactly that case.
Handoff correction, verified rather than inherited. §5 claimed the
script "restores by `git checkout --`, which reverts the file to HEAD",
destroying uncommitted work, and cited a wiped review round during
#165. The mechanism description is false: the script copies the file to
a mktemp path before swapping and restores from that copy under an
`EXIT INT TERM` trap, touching no git state beyond a read-only
`git show`. The commit-before-gating rule is kept --- it stands on
gate-results-describe-the-pushed-tree --- but the false mechanism is
removed, because a reader who believes bite eats uncommitted work will
reach for `git stash` to protect themselves, which is the repo-global
trap the script exists to avoid.
No product code. No tests changed.
Typing `\alpha` in a Lean 4 buffer gives `α`; `\<>` gives `⟨⟩` with the
point between them. The abbreviation table is vendored from
vscode-lean4 and the expander is a typed-edit consumer registered on
the Stage 4a chain at priority 50, ahead of auto-pairing.
The ordering is load-bearing. 64 abbreviation keys contain a character
in the `lean4` pair set, so with pairing first, typing `\[` would
insert `[]` and corrupt the pending key to `\[]` before the second `[`
arrives — `\[[]]` becomes unreachable. The consumer therefore claims
every keystroke that EXTENDS a pending abbreviation, not only one that
completes an expansion; claiming only completions would hand each
intermediate `[` to pairing by a different route.
The vendored table is an ORDERED SEQUENCE, not a map. Upstream breaks
equal-length ties by source declaration order — 101 prefixes depend on
it, and `\f` resolves through `f<` rather than `f>` — which a
`pairs`-iterated Lua table cannot express. `scripts/regen-lean-abbrev`
takes a vscode-lean4 commit, emits the file with its provenance header,
and aborts on a duplicate key, invalid UTF-8, or a round-trip mismatch.
Undo is cross-peer-degraded on CRDT frontends and that is accepted and
named, not papered over (Q#LN21): `\alpha` arrives as six source-peer
optimistic inserts while the expansion is one daemon-peer replace.
`set_round_trip_input` would fix it and also makes `dispatch_idle`
report false, so RET would stop inserting a newline.
Round 9 corrects three approved acceptance criteria that the real table
contradicts, found by simulating the state machine over all 1,855
entries and re-reading upstream at the pinned commit rather than
re-reading the prose. `\to` is not eager — `top`, `to0` and `toa`
extend it. `\zzzz` expands to `ζzzz ` because `ze`, `zeta` and
`zsqrtd` exist; only `$ % , ; @ W` open no key at all. And `\alpha`'s
undo does not restore `\alpha ` because `alpha` IS eager, so the
terminator is a separate edit. Criteria 38, 41 and 42 now state both
paths, and the false halves are asserted too: they read as correct
until the table is consulted.
Three implementation traps worth the record. The generator's own
round-trip check was broken twice and failed closed both times:
`str.splitlines()` splits on U+2028, which 53 symbols contain, and
escaping through `chr(byte)` produced a latin-1-shaped string that the
UTF-8 write re-encoded. The first check compared in-memory strings and
agreed with itself; it now stages the file, re-reads the bytes from
disk, and renames into place only on a match. And the expansion SHRINKS
the buffer, so the point must be placed explicitly — pairing's
no-cursor-motion rule holds only for an insert AT the cursor, and
without this every self-insert after the first expansion is silently
rejected and the editor looks dead.
25 acceptance tests plus one `--lib` test for the optimistic CRDT
producer (45f), which is where the gate list's `--features crdt` run
reaches it; a crdt-gated integration test would be dark in CI and in
the gates both. Fifteen mutations bite, each failing its target. Three
of these tests were vacuous when first written and biting is what
found them: the abandonment test asserted text a surviving record
would also produce, the re-arm test used an example that never reaches
the re-arm branch, and both switch tests ran through
`find_or_open`'s fresh-load path rather than `buffer.after-switch`.
No protocol change (Q#LN14). Also reconciles the handoff and ledger
for Stage 4a (#179) and adds `lean.abbrev` to COHERENCE.md's
config-registry adoption census, now nine settings.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
A trap-guarded one-file swap over read-only git show: run the named
tests against an older version of one file and exit 0 iff they FAIL
there (the fix bites); exit 1 flags a vacuous fix. The file is
restored on every exit path including interrupts; the ./ pathspec
prefix makes it work from any directory inside the repo. Never
touches git stash — the stash namespace is repo-global, shared
across worktrees and with humans (a #111-round mishap popped a
PR-#17-era user stash; hence the tool).
Dogfooded three ways against the merged #111 history: the round-1
fix commit bites (exit 0), the same tests against HEAD read as
vacuous (exit 1), and a docs/-relative invocation restores cleanly.
Handoff: section 1 snapshot (editops #111 merged, worktree folded),
section 5 lessons (repo-global stash; worktree-per-lane for
parallel work).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018vF4gQVozBWi38y1SJiGfQ
Levi Neuwirth