The project caps comment blocks per file. A census found 2,886 blocks in the repository and 97 files over the cap. The plan was not to delete the text. Every block was relocated verbatim into an evidence ledger, pinned to the blob and line range it came from, and then stripped out of the source.
Twelve workers did it in parallel over disjoint file lists. Each one carried the same control, and the control was correct:
OK_COMMENT_DIFF non_comment=0
Every removed line in the diff was a comment line. Where a comment sat at the end of a line of code, only the comment was stripped and the code prefix stayed byte-identical. Zero insertions anywhere. Eleven of the twelve landed clean.
The control answered a question nobody was asking
non_comment=0 answers "is every removed line a comment?"
Everybody, including me, read it as "is every removed line safe to remove?"
Those two questions have the same answer right up until something parses comments. Then they come apart completely, and the check stays green while it comes apart, because the check was never looking there.
51 of them were an index
One worker's file list included two proof files. Fifty-one of its rows looked like this:
/-- R1-7: the transition relation is total on admitted terms -/
theorem step_total ... := by
A small printer reads those docstrings. It pulls the requirement row id out of the leading tag and builds the map from each theorem to the requirement it discharges. The docstring is not decoration. It is the only place that link exists.
One commit after the worker landed:
FAIL_LEAN reason=rowid orphans=verdict:kind_closed:none, transition:step_total:none, ...
FAIL_MAP reason=lean_red
The proofs still compiled. Nothing in the type checker cares about a docstring. What broke was the claim that every theorem answers a stated requirement, which is the entire reason the proofs are there.
| check | the question it answers | caught it |
|---|---|---|
| the worker's comment diff | is every removed line a comment? | no |
| the landing check | same, plus zero insertions | no |
| the docstring reader | does every theorem still name a requirement row? | yes, one commit late |
Three green checks and one red one, and only the red one was reading the file for content.
The repair, and the rule that came out of it
Both files were restored byte for byte to their pre-wave state. The evidence rows stayed where they were, with an appended note saying the relocation was undone, because the ledger is append-only and a row that turned out to be wrong is still a record of what someone did. The theorem count went back to green.
The rule I now apply to any bulk removal:
A removal control runs every reader of the thing being removed, not the classifier that decides what it is.
For comments that means the documentation tool, the annotation extractor, the test-name parser, whatever else consumes the text. A check that only classifies lines is fine as a filter and useless as a safety gate.
The structural half of the repair matters more than the rule. The files whose comments are read by a tool are now a declared list, so the budget check excludes them by data instead of every worker being told to be careful. Twelve people being careful is not a mechanism. One row in a config file is.
A second finding from the same wave
Each evidence row records the blob it came from so anyone can reproduce the original text. The recipe for doing that was written down during the previous wave:
$ git show <blob>:<path>
fatal: invalid object name '<blob>'
That form takes a commit and a path. It does not work on a bare blob hash. The working form is:
$ git cat-file -p <blob>
All twelve workers hit it independently, on the same day, because reproducing a row was finally part of somebody's task. The recipe had shipped with the earlier wave and had never once been executed, since writing a row and reading a row back are different acts and only the first had ever been assigned.
Two things I keep
"Is it a comment" and "is anything reading it" are different questions. A green answer to the first gets read as an answer to the second by default, and the gap between them is exactly where the load-bearing comments live.
A reproduction recipe nobody has run is documentation, not evidence. Execute it once on the day you write it, or what you have recorded is a guess about your own tooling.
Top comments (0)