Give a disproved claim a home the next round will read - #603
Merged
Conversation
A decline that carries proof proves something about this tree, and the thread it was written in closes with the pull request. The next round starts without it, and the second occurrence of a claim reaches a maintainer with no way to tell it from a first. The Copilot review runbook gains a `Disproved Claims` record, so the proof is read rather than built twice. An entry names the claim, what was run or read to disprove it, the revision it was proved against, and what ends it. A disproof is true of one tree at one revision, so an entry whose subject moves is deleted by the change that moves it rather than edited to look current: an entry outliving the code it was proved against becomes a reason not to check, which is strictly worse than proving the claim again. The record answers a repeated claim and never dismisses a new one, so a finding is judged on its merits first and matched against the record second. Three worked examples ship with it. - `keys_unsorted` requires jq 1.6, so `check_ruleset` cannot compile on jq 1.5. Re-run in this session on `jq-1.5-1-a5b5cbe`, the build that reproduces the `walk/1` failure: `keys_unsorted` evaluates there and `walk(.)` answers `jq: 1 compile error`. - Splitting the write-guard's fallback parse a line at a time mis-reads a newline inside a quoted argument. The arm cannot execute below the 3.7 floor `install.py` enforces, and the alternative degrade is worse where it counts. It earned a test case rather than a change. - A description's stale commit claims are found by extracting the bare SHAs it quotes. This one came from this repository's own backlog rather than from a reviewer, and the corpus rejected it 4 out of 4. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Adds a durable place in the GitHub Copilot review runbook to record disproved findings, and updates the TODO backlog entry to track the remaining governance-level routing gap (provider-agnostic contract does not yet point at the record).
Changes:
- Extend
.github/copilot-instructions.mdto direct that evidence for disproved findings should be recorded under a new “Disproved Claims” section (in addition to the PR thread). - Add a new “Disproved Claims” section with worked examples, including what was tested, which revision it was proved against, and what would invalidate the proof.
- Update the corresponding
TODO.mdcluster to reflect that the remaining work is governance-level (byte-locked) guidance for non-Copilot reviewers/agents.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| TODO.md | Reframes the backlog cluster to target governance-level routing of disproof records beyond the Copilot-specific runbook. |
| .github/copilot-instructions.md | Introduces a “Disproved Claims” section and updates guidance so evidence is preserved beyond the PR thread lifecycle. |
Uh oh!
There was an error while loading. Please reload this page.
ptr727 added a commit
that referenced
this pull request
Aug 8, 2026
… that blocks on what it cannot read (#609) Promotes 14 commits from `develop`. Merge with a **merge commit** (`gh pr merge --merge`), never a squash, and **without `--delete-branch`**, since this pull request's head is `develop` itself. Closes#607 through the closing keyword already carried in `530cf71`, which is why it is not repeated here. ## The prose backlog, cleared end to end `#600`, `#604`, `#605`, `#606` took the tree from **557 findings across 45 files to 0 across 0**, in four batches ordered by surface: snippets, comments, hub-only Markdown, then the carried files. Each batch measured the checker's own exemption against the live corpus *before* sweeping, and twice the measured answer was **"do not change the checker"**, which is a result of that pass rather than a skipped one. `#594` added the floor that makes those numbers trustworthy: a diff-scoped run now asserts what it actually scanned, since a check whose scan matches nothing reports zero findings and reads exactly like a pass. One finding from that work is worth carrying up: an exemption that is too **loose** produces silence rather than false positives. #519 recorded the governance files as clean; today's checker reports 38 findings against those same files as they stood at the commit that measured them. ## A review loop that fails closed `#599`, `#601`, `#602`, `#603` and `#608` are one arc on `scripts/pr_review.py`, each removing a shape in which the loop reported a clean pass over a review it had misread: - **`#599`** removed the shape a reply kept failing in, by taking the thread's *words* rather than an id, so there is no argument a hand-typed `PRRT_...` fits in. - **`#602`** made `claims` resolve what a description points at rather than what it looks like. - **`#603`** gave a disproved claim a home the next round reads. - **`#608`** reads the file-coverage line, and then generalizes: every reader keys on a structural marker, so a marker that changes spelling is a section the reader stops finding and reports as absent. The digest now vets headings, `<summary>` texts, metadata labels, coverage wordings and the reviewer login against an inventory measured from **332 review bodies**, and **blocks on anything outside it**, exit `43`, with the remedy stated as filing an issue on the hub. Whether to merge regardless is the maintainer's decision. `GOVERNANCE.md` merge gate went from four preconditions to **five** accordingly. ## Governance and tooling - **`#593`** states which checkout an agent works in and what the hub is, which is the host-wide routing the repositories that most need it cannot carry. - **`#596`** gates the pattern-detectable half of the representative-data rule, honest that no pattern closes the name-shaped case. - **`#598`** declares where a repository states what CI cannot verify. - **`#592`** regrouped `TODO.md` by what ships rather than by what it touches, so a `###` heading is one pull request. - **`#601`** ended a `gh push` argument list at a newline rather than only at `&&`, fixing a write-guard over-block. ## Verification Run on `develop` at `530cf71` immediately before opening this: `test_pr_review.py` (174), `test_prose_lint.py`, `test_repo_gate.py`, `spec/audit.py --selftest`, `gh-write-guard.py --selftest`, `spec/validate.py`, `repo_gate.py`, the prose gate in both CI invocations, markdownlint and editorconfig-checker. All clean. ## Not carried by this promotion - **#519 is complete and still open.** `TODO.md` holds its closing evidence under "Verified Complete, Awaiting Close". Closing it is the maintainer's call, so no keyword for it appears here. - **The re-vendor debt is now nine files.** `#606` queued seven, and `#608` changed `GOVERNANCE.md` "PR Review Etiquette" (`verbatim`) and `.github/copilot-instructions.md` (`intent`) on top. The `intent` half produces no hash and therefore no audit finding, which is why the Fleet Sweeps entry names those files by hand. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Clears the
A Home for a Disproved Findingcluster fromTODO.md. ItsCheckedanchor was re-verified againstdevelopat756a53ebefore anything was written: the file still says the reviewer is sometimes factually wrong, still requires a decline to carry evidence, and still keeps its list of known non-working request paths, with nowhere to put the proof itself.The gap
A decline that carries proof proves something about this tree, and GOVERNANCE.md "Every Finding Ends in an Action" is right that the thread is where it belongs while the pull request is open. Afterwards the thread is the wrong place. The pull request merges, the next round starts with no memory of the last, and the second occurrence of the same claim reaches a maintainer with no way to tell it from a first.
Disproved Claimsis a new###under the runbook, so the three declared##sections inspec/files.jsonare unchanged. An entry names the claim, what was run or read to disprove it, the revision it was proved against, and what ends it. It is deliberately not a list to append to: an entry outliving the code it was proved against becomes a reason not to check, which is strictly worse than proving the claim again, so an entry whose subject moves is deleted by the change that moves it rather than edited to look current. Two guards ride with it. The record answers a repeated claim and never dismisses a new one, so a finding is judged on its merits first and matched second, and a reply carries the proof re-read rather than a pointer to a file the reviewer cannot open. And the entries are this repository's own, so a repository holding a copy carries the shape and deletes an entry whose subject it does not carry.The three worked examples
keys_unsortedrequires jq 1.6. A suppressed finding on #555 against the normalizer inrepo-config/configure.sh, reasoning by analogy from thewalk/1failure #553 fixed. Re-run in this session rather than quoted from the thread, onjq-1.5-1-a5b5cbeinubuntu:18.04, the build that reproduceswalk/1:The write-guard's fallback parse, from #601. Declined on the ground that the arm cannot execute, since
punctuation_charsarrived in Python 3.6, the module uses f-strings throughout, andinstall.pyrefuses below 3.7. That is exactly the kind of disproof that expires, which is why the entry names the floor as what ends it. It also records that the finding earned a test case rather than a change, since onlyValueErrorfrom unbalanced quoting reaches that path in practice and nothing covered it.The bare-SHA design, from #602. This one came from this repository's own backlog rather than from a reviewer, and it is here because a rejected method costs the same to re-propose as a declined finding costs to re-derive, while a backlog has a place for a claim the tree contradicts and none for a method a measurement rejects. Over the 25 most recent merged pull requests the bare-SHA arm raised four references and all four were correct prose, and a path arm flagged 54 of 215 backticked candidates.
Both #601 and #602 are folded under disposition Amends "Record what was tested and against which revision, and delete an entry whose subject changes." They land as the second and third worked examples in the shipped section rather than as
Settledbullets, because the entry ships in the same change.Verification
python3 scripts/prose_lint.py . --diff developclean,markdownlint-cli2clean on both files.python3 -m unittest discover -s scriptsreports 372 tests OK andpython3 spec/audit.py --selftestpasses, neither touched by this change but both run because the file is carried.756a53e: thekeys_unsortedcall inrepo-config/configure.sh,_git_subcommand_arglistsand_PUNCTUATION_CHARSingh-write-guard.py, the(3, 7)floor ininstall.py, and the verb alternation inpr_review.py.TODO.md
The cluster is deleted per the file's own step 9. What this change does not carry becomes a new
readycluster:GOVERNANCE.mdoutcome 2 ends at the thread and nothing agent-agnostic points at the record, so an agent that never opens the provider runbook posts a decline and has nowhere to put the proof. That is a byte-locked carried section and a fleet re-vendor, which is why it is a separate change rather than a second surface in this one.Downstream
.github/copilot-instructions.mdis carriedwholeatintentwithappliesTo: "*", so this joins the re-vendor the ledger already lists. A repository taking it carries the section and its rules, and starts its own entries empty.🤖 Generated with Claude Code