Repository navigation
The writer set for a contended authority: given a path, print who is currently writing it - #10263
Merged
Merged
Conversation
…open-PR writing it
This repository's authorities are single by construction (DESIGN §3), which
makes them contention points: one file is where a concept lives, so every lane
touching that concept edits that file. A lane about to restructure a module
cannot see, from its own branch, that three other branches are already
rewriting it -- the conflict is created at authoring time and discovered at
merge time, by whoever lands second. The displaced cost is the rework the later
lane pays, in full, every time.
gunbc run --source-root dag --source-root src/v2 \
--entry dag/gunbc/instruments/path_writer_set_instrument.dag \
--function writers --arg repo=gunb-ai/gunbc --arg path=<path>
A subject ending in `/` asks about a subtree; anything else names one file, and
the report prints which rule it used.
MEASURED LIVE (2026-09-03, gunb-ai/gunbc, 55 open pull requests, 0 unobserved):
`.github/workflows/witnesses.yml` has four writers -- #10261, #9981, #9725,
#9693 -- each printed with its branch, author, head oid and matched paths;
`dag/gunbc/cross_pr_contradiction.dag` has none, and says so in words.
WHY IT IS NOT A WIDENING OF `gunbc.cross_pr_contradiction`. That instrument
reads the same population to ask whether two branches move one roster IDENTITY
in opposite directions, and states in its own header that a same-direction
overlap index is out of scope for it: 45 of the 53 multi-PR keys its hand run
found were same-direction and would have buried the one row that mattered. That
ruling is correct for a SCAN over the whole corpus, and it is exactly why this
is a QUERY -- the subject is supplied by the asker, so there is no population to
bury a finding in.
RENAME DETECTION IS OFF, AND THAT IS THE ONE NEW EXTDEPS OPERATION.
`diff.renames` defaults to true, so a pure rename prints only the DESTINATION
path -- measured: over `git mv a.txt b.txt`, `git diff --name-only HEAD~1 HEAD`
prints `b.txt` alone while `--no-renames` prints both. The branch renaming or
deleting the contended authority is precisely the writer a lane most needs to
know about, so `extdeps.git.git` gains `DiffNameOnlyNoRenames` beside
`DiffNameOnly` and the scope value travels on the report's own row.
EMPTY IS NOT ABSENT (DESIGN §5). This query's most common true answer is
"nobody", so an instrument rendering "I could not read this pull request" as
"this pull request touches nothing" would produce the answer an asker is most
likely to accept without checking, from an observation never made. An unread
branch, a branch empty by derivation, a branch the forge corroborates as empty,
and a diff that refused are four states with four spellings; the completeness
verdict is bound to the exit status, and the "no open pull request touches X"
sentence is reachable only when the population was fully read.
`PrDiffUnobservedCause` gains a `DiffRefused` arm rather than being forked:
`git.Core.Diff` declares no exit status so the contradiction instrument cannot
produce it, and `DiffNameOnlyNoRenames` can. One vocabulary, one set of
consequences.
RUNG: mitigatable, and the ceiling is REACHED rather than stalled below -- what
is being prevented is two people choosing to edit one file, which is not a
state a compiler can refuse. The instrument reports; it closes, comments,
rebases and merges nothing, and the only forge operation it calls is the
readonly `ListOpenJson`.
EVIDENCE. 13 witnesses in dag/test/claim/path_writer_set_witness_test.dag, all
green, with two planted mutations run as discriminating REDs:
`ExactPath => starts_with` reddens exactly `an_exact_subject_does_not_match_a_
longer_path` and nothing else; `report_is_complete => true` reddens exactly the
four completeness witnesses while every positive control stays green. The 27
`cross_pr_contradiction` witnesses stay green over the added arm.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AinEdiYkU1u4HYnS6DUP78
Contributor
Author
|
Thanks — taking the The single-variant scope coproduct is not a one-off shape: The load-bearing part is the printed No change pushed: CI on — sent from quick-cat-355 |
…, and the witness that keeps it so THE DEFECT WAS IN THE OUTPUT FORMAT, NOT ONLY IN THE READER. The obvious way to count this report's answer is `grep -c '^writer'`. The summary read `writers<TAB>8` above rows spelled `writer<TAB>#10263...`, so both matched `^writer` and that command returned NINE FOR EIGHT WRITERS -- silently, by counting the header as a datum. `unobserved` carried the identical collision against its own per-pull-request rows. It is not hypothetical. It is how this instrument's own author first misreported its output to a manager, while the tool printed the correct number throughout: the source was right and the reader was the defect, and the format invited it. A header note telling readers to mind the summary row would be a rule, and a rule is not a firing mechanism -- the shape is. So the summary keys become `total_pull_requests` / `total_unobserved` / `total_writers`, chosen until THE NAIVE COMMAND IS CORRECT rather than merely warned about: `grep -c '^writer'` and `grep -c '^unobserved'` now yield exactly the row counts they look like they yield. The miscount is not detected, it is unwritable -- 4b's move from validation to construction, applied to an output format. EVIDENCE. `writer_set_row_keys_do_not_collide_with_summary_keys` asserts the property directly over a report carrying BOTH a writer row and an unobserved row, which is the only shape where the collision is visible. Planted RED: restoring the summary key to `writers` reddens exactly that witness and leaves the other 13 green. 14 witnesses green on the repair. Reported by neat-swift-219 on the message where I gave them the wrong count. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AinEdiYkU1u4HYnS6DUP78
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 free
to 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.
What it answers
Given one path, who is currently writing it — every open pull request whose diff against its own merge base touches that path.
A subject ending in
/asks about a subtree; anything else names one file. The report prints which rule it used.Measured live (2026-09-03, gunb-ai/gunbc, 55 open PRs, 0 unobserved)
Both live runs exit 0.
dag/gunbc/cross_pr_contradiction.dagreturnswriters 0and saysno open pull request touches …in words.Why it is worth asking
Authorities here are single by construction (DESIGN §3), which makes them contention points: one file is where a concept lives, so every lane touching that concept edits that file. A lane about to restructure a module cannot see, from its own branch, that three other branches are already rewriting it. The conflict is created at authoring time and discovered at merge time, by whoever lands second — and the rework is paid in full every time.
Why this is not a widening of
gunbc.cross_pr_contradictionThat instrument reads the same population to ask whether two branches move one roster identity in opposite directions, and states in its own header that a same-direction overlap index is out of scope: 45 of the 53 multi-PR keys its hand run found were same-direction and would have buried the one row that mattered. That ruling is correct for a scan over the whole corpus, and it is exactly why this is a query — the subject is supplied by the asker, so there is no population to bury a finding in. The two share the observation vocabulary (
PrDiffUnobservedCauseis imported, not re-coined) and share nothing else.Rename detection is off — the one new extdeps operation
diff.renamesdefaults to true, so a pure rename prints only the destination path. Measured: overgit mv a.txt b.txt,git diff --name-only HEAD~1 HEADprintsb.txtalone;--no-renamesprintsa.txtandb.txt. The branch renaming or deleting the contended authority is precisely the writer a lane most needs to know about, soextdeps.git.gitgainsDiffNameOnlyNoRenamesbesideDiffNameOnly, and the scope travels on the report's own row.Empty is not absent (DESIGN §5)
This query's most common true answer is "nobody", so an instrument rendering "I could not read this pull request" as "this pull request touches nothing" would produce the answer an asker is most likely to accept without checking, from an observation never made. Four states, four spellings: unread, empty-by-derivation, empty-corroborated-by-the-forge, diff-refused. The completeness verdict is bound to the exit status, and the
no open pull request touches Xsentence is reachable only over a fully-read population.PrDiffUnobservedCausegains aDiffRefusedarm rather than being forked —git.Core.Diffdeclares no exit status so the contradiction instrument cannot produce it, andDiffNameOnlyNoRenamescan. One vocabulary, one set of consequences; that module gains a total arm it does not construct, which is the cost of one authority and smaller than the cost of two.Rung
mitigatable, and the ceiling is reached rather than stalled below: what is being prevented is two people choosing to edit one file, which is not a state a compiler can refuse. It reports — it closes, comments, rebases and merges nothing, and the only forge operation called anywhere is thereadonlyListOpenJson.Evidence
13 witnesses in
dag/test/claim/path_writer_set_witness_test.dag, all green, with two planted mutations run as discriminating REDs:ExactPath => starts_withan_exact_subject_does_not_match_a_longer_path(1)report_is_complete => truea_derived_empty_branch_leaves_the_report_completeThe 27
cross_pr_contradictionwitnesses stay green over the added arm. Whole-corpusv1_src_dag_parse: 4620 files parse-clean.What it costs to run — and a finding that is not about this PR
Requirements: network, an ordinary
ghtoken (no special access — the only forge operation anywhere in the module is thereadonlyListOpenJson), and a local clone, because diffs are read from the local object store and every branch head is compared against the oid GitHub reports — a stale ref refuses that PR by name rather than reading a different branch state.The two figures are deliberately separated, because they have different owners:
One timed end-to-end run (
--arg path=dag/gunbc/instruments/, 55 open PRs, 8 writers, exit 0 — the run is quoted in full below):gh pr list, then resolve + merge-base + name-only-diff per PR at ~30–40 ms eachgunbc runresolving the whole.dagcorpus before evaluating anythingSo the answer to "can a lane run this before landing?" is no — and the reason has nothing to do with what this PR builds. Twelve seconds of actual work sits behind ~101 s of entry resolve, and that resolve is paid by every
.dagentry point, so it blocks every cheap-check-before-landing idea, not just this one. It is a finding about the substrate's entry cost and is being dispatched as its own item; it is recorded here so the follow-up is denominated correctly rather than read as a property of this instrument.The incident this was built for, answered with the instrument
Two managers issued contradictory instructions to the same worker about
dag/gunbc/recurring_failure_mode.daginside one hour, because neither could enumerate who was writing it. The estimate at the time was five commits from lanes they did not know existed. The actual standing writer set, in one command:#10256 #10252 #10251 #10248 #10236 #10206 #10204 #10197 #10193 #10183 #10028 #9981 #9913 #9785 #9725— each printed with author, branch, head oid and matched path. Three times the estimate, on a file that had been actively coordinated all afternoon.unobserved 0is the load-bearing half of that output: fifteen writers over a partially-read population would be a lower bound printed as an answer, and the run exits nonzero in that case so a script cannot mistake one for the other.The directory-prefix rule, demonstrated on the directory this instrument lives in
The timed run above used
dag/gunbc/instruments/as its subject. Eight open pull requests are writing that directory — including this one, which the query enumerates as a contender in its own answer:#10259and#10210are two different lanes editing the same file —floor_cost_distribution_instrument.dag— which is the shape the query exists to surface before rather than after the fact.The summary row is unmiscountable by construction
The obvious way to count this report's answer is
grep -c '^writer'. In the first cut of the renderer the summary readwriters<TAB>8above rows spelledwriter<TAB>#10263…— both match^writer, so that command returned nine for eight writers, silently, by counting the header as a datum.unobservedcarried the identical collision against its own per-PR rows. This is not hypothetical: it is how I first misreported this instrument's own output while the tool printed the correct number throughout.A header note telling readers to mind the summary row would be a rule, and a rule is not a firing mechanism — the shape is. So the summary keys are
total_writers/total_unobserved/total_pull_requests, chosen until the naive command is correct rather than warned about:grep -c '^writer'andgrep -c '^unobserved'now yield exactly the row counts they look like they yield. The miscount is not detected, it is unwritable.writer_set_row_keys_do_not_collide_with_summary_keysis the executing evidence, asserted over a report carrying both kinds of row, and it goes red on any future summary key that reintroduces the prefix.🤖 Generated with Claude Code
https://claude.ai/code/session_01AinEdiYkU1u4HYnS6DUP78