Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions dag/extdeps/git/git.dag
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,9 @@ type AdvertisedRef {

data advertised_ref_scan_note: String = "The scan REFUSES on a line it cannot read rather than skipping it, and the located line is carried so the refusal names what it choked on. Dropping unparseable lines is the shape DESIGN 5 calls the absorbing fallback: the answer would still be a well-formed ref list, so a consumer could not tell a complete advertisement from a partial one, and the deficit's frequency would be zero by construction. A partial ref list is exactly the input that makes an exact-head judgment answer `not published` about a branch that is in fact published."

data ls_remote_carries_no_exit_block_note: String = "WHY LsRemoteHeads DECLARES NO `exit` BLOCK WHILE EVERY SIBLING OPERATION DOES, which is the first thing a reader will notice. The `exit` arms are INERT AT RUN TIME - established by reading the seed, not assumed. The shell dispatch in v1_interpreter.rs maps declared output sources (`stdout`, `stderr`, `exit_success`, `exit_code`, `stdout_lines`) onto the process result and returns a record; it never consults the operation's exit arms and never raises on a nonzero exit. The only consumer of exit_props anywhere outside the parser is v1_compiler_emit_rust.rs, which round-trips them back to source so the self-host fixed point holds. So an exit arm is a declaration that is parsed, re-emitted, and never realized.\\n\\nThat makes this operation's OUTPUTS the realized authority for its outcome: a caller learns whether the read succeeded from `success`/`exit_code`/`stderr`, which are values it can match on. Adding an exit block beside them would be a second representation of the same fact where only one of the two executes - and since this operation is new, authoring one knowing it is inert would be minting a fresh declared-but-unrealized instance rather than inheriting an existing one. The corpus-wide inertness of exit blocks is a real finding and a separate correction; it is not fixed by making one operation diverge from a hundred siblings, and it is not made worse by declining to add the hundred-and-first."
data ls_remote_reports_termination_not_success_note: String = "IT REPORTS THE EXIT CODE AND NOT A SUCCESS BOOL, WHICH IS A NARROWING FROM ITS FIRST CUT. That cut declared `success: Bool from \"exit_success\"` beside `exit_code`, and the two are not independent: the seed derives exit_success as exactly `exit_code == 0` (v1_interpreter.rs, the shell dispatch output-source match), so the pair carried one fact twice.\\n\\nCARRYING IT TWICE WAS NOT MERELY REDUNDANT, IT MADE A CONTRADICTION WRITABLE. A caller of the deciding function could pass success true beside a nonzero exit code, and the function branched on success - so a failed advertisement read as a successful one and the branch reported unpublished rather than unreadable. That is the ignorance-as-answer conflation this operation exists to prevent, reachable through the operation own output shape. Dropping the Bool makes the contradictory pair unrepresentable rather than merely unlikely, which is why this is construction and not a check.\\n\\nWHICH LAYER OWNS SUCCESS, since something still has to answer it: the caller EXPECTATION does. Process termination, operation observation, caller expectation and log disposition are four facts, and a probe may legitimately use a nonzero exit as an ANSWER rather than a verdict - so an operation that pre-judges its own exit code as success has decided something only its caller can. See gunbc.plans.transport_argv_anemia_dissolution, which measures 148 sibling operations in dag/extdeps still carrying the Bool while 51 preserve the integer. This operation is the first consumer of that correction, not a local exception."

data ls_remote_carries_no_exit_block_note: String = "WHY LsRemoteHeads DECLARES NO `exit` BLOCK WHILE EVERY SIBLING OPERATION DOES, which is the first thing a reader will notice. The `exit` arms are INERT AT RUN TIME - established by reading the seed, not assumed. The shell dispatch in v1_interpreter.rs maps declared output sources (`stdout`, `stderr`, `exit_success`, `exit_code`, `stdout_lines`) onto the process result and returns a record; it never consults the operation's exit arms and never raises on a nonzero exit. The only consumer of exit_props anywhere outside the parser is v1_compiler_emit_rust.rs, which round-trips them back to source so the self-host fixed point holds. So an exit arm is a declaration that is parsed, re-emitted, and never realized.\\n\\nThat makes this operation's OUTPUTS the realized authority for its outcome: a caller learns whether the read succeeded from `exit_code`/`stderr`, which are values it can match on. (It carried a `success` Bool too until this operation narrowed - see ls_remote_reports_termination_not_success_note directly above, which is the authority for why. Left unfixed, this sentence would have been a stale citation inside the very PR that made it false.) Adding an exit block beside them would be a second representation of the same fact where only one of the two executes - and since this operation is new, authoring one knowing it is inert would be minting a fresh declared-but-unrealized instance rather than inheriting an existing one. The corpus-wide inertness of exit blocks is a real finding and a separate correction; it is not fixed by making one operation diverge from a hundred siblings, and it is not made worse by declining to add the hundred-and-first."

type AdvertisedRefScan
= AdvertisedRefsRead { refs: List<AdvertisedRef> }
Expand Down Expand Up @@ -584,7 +586,6 @@ service git.Core {
input { remote: String }
output {
advertised: List<String> from "stdout_lines"
success: Bool from "exit_success"
exit_code: Int from "exit_code"
stderr: String from "stderr"
}
Expand Down
46 changes: 43 additions & 3 deletions dag/gunbc/roadmap_publish.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import extdeps.github.pulls {
PullRequest,
PullRequestState, Open,
}
import v2.std.operation_argv { OperationRef, operation_ref_label }

data publish_producer_note: String = "PUBLICATION IS ADJUDICATED AGAINST AN EXACT HEAD, NOT LOOKED UP BY BRANCH (operator ruling, 2026-07-31). An earlier cut of this module answered 'which pull request belongs to this branch', which is a lookup rather than a judgment: it reported whatever head that pull request happened to carry and left the caller to compare. Every downstream obligation — verify, review, audit, acceptance — is about one exact commit, so the question Publication has to answer is whether THIS commit is the one on offer.\\n\\nThe branch is a lookup and publication handle. A completed judgment belongs to a head sha.\\n\\nTHE ARM THAT MOTIVATES THE REWRITE is PublicationHeadDiverged. A pull request exists, its branch matches, and its head is NOT the commit under judgment — the ordinary state after a worker pushes a revision while a review is in flight. Under a branch lookup that reads as a successful publication, and every later receipt binds to a commit nobody assessed. It is the one outcome a lookup cannot express and the one most likely to occur."

Expand All @@ -22,9 +23,48 @@ type PullRequestObservation
= PullRequestsRead { pulls: List<PullRequest> }
| PullRequestsUnreadable { detail: String }

data remote_branch_read_failure_note: String = "THREE CAUSES, THREE REMEDIES, PREVIOUSLY ONE STRING. RemoteBranchesUnreadable carried `detail: String` and three genuinely different failures were flattened into it at the point of construction: the ref advertisement was REFUSED by the transport, an advertised LINE did not parse, or an advertised ref PROJECTED to an empty branch name. Those are not three phrasings of one event. The first is an environment fact and says nothing about the repository; the second means the remote spoke a format this parser does not accept; the third means a ref exists whose name survives advertisement but not projection. A caller handed a sentence can only re-derive which of the three it holds by matching on the prose, which is the classifier-by-substring move the transport-anemia plan exists to remove.\\n\\nTHE ARGV WENT WITH IT, and that is the sharper half. Each of those three sentences was built by concatenating the literal `git ls-remote --heads` onto the remote name, so the command SPELLING was load-bearing in a domain refusal three times over. A domain layer reaches for a command spelling exactly when it has no stable operation identity to name; the operation is git.Core.LsRemoteHeads and naming it is both stabler and truer, since the spelling is one realization of it and will change when the invocation is derived rather than hand-written.\\n\\nSO THE CAUSE IS TYPED AND THE PROSE MOVES TO A RENDERER. render_remote_branch_read_failure is the only function here that produces a sentence, and it names the operation rather than the argv. What it renders is recoverable from the fields, which is what makes the rendering a projection rather than the authority.\\n\\nWHAT THIS DOES NOT FIX, stated so the seam is visible: RefAdvertisementRefused still carries exit_code and stderr as an Int and a String, because the typed process observation that would replace them does not exist yet — it is the substrate half of this same plan (Lane C) and is in flight separately. This arm is therefore honest about WHICH failure occurred while still anemic about what the process did. The other two arms have no such dependency: they are decided by this module's own decoding, downstream of the process, and are fully typed here."

type RemoteBranchReadFailure
= RefAdvertisementRefused { remote: NonEmptyStr, exit_code: Int, stderr: String }
| AdvertisedLineUnparsed { remote: NonEmptyStr, index: Int, line: String }
| AdvertisedRefProjectsEmptyBranch { remote: NonEmptyStr, ref_names: List<String> }

data ls_remote_operation: OperationRef = OperationRef {
path: "dag/extdeps/git/git.dag",
service: "git.Core",
operation: "LsRemoteHeads",
}

data ls_remote_operation_ref_note: String = "WHY A REF AND NOT THE STRING `git.Core.LsRemoteHeads`. An earlier cut of this module carried the identity as a free String, which is a second textual naming scheme for something the declaration already names, and which goes stale silently when the operation is renamed - nothing anywhere can tell that it did (DESIGN 3, cite the symbol). An OperationRef is the corpus's single vocabulary for `which operation`, and the difference is decidability rather than tidiness: shell_transport_operation_rows enumerates the declared rows each carrying its own `at`, so a ref naming nothing is findable from that enumeration, and a sentence fragment is not reachable from it at all.\\n\\nWHY THE REF IS WRITTEN HERE RATHER THAN DERIVED, which is the sharper question and is refused on purpose. Deriving it would mean selecting the row out of shell_transport_operation_rows, and that builtin reads the declarations in the live source tree. This module's whole property is that it adjudicates over values a caller already holds - see belt_observes_note - which is what makes every arm, including the refusals, reachable with no network, no token, and no tree. Buying a staleness check with that property would be a bad trade: it would move the module from pure to ReadsLiveTree, and the arms that a witness can currently construct directly would become dependent on what the tree happens to contain.\\n\\nSo the check belongs OUTSIDE this module, over the corpus's refs at once, where the enumeration is already being read for other reasons - not inlined at each site that names an operation."

fn render_remote_branch_read_failure(cause: RemoteBranchReadFailure) -> String {
let at = operation_ref_label(at: ls_remote_operation)
match cause {
RefAdvertisementRefused { remote, exit_code, stderr } =>
join([
at, " against ", remote as String,
" exited ", to_string(exit_code), ": ", stderr,
], "")
AdvertisedLineUnparsed { remote, index, line } =>
join([
at, " against ", remote as String,
" advertised a line at index ", to_string(index),
" that is not an object-id/ref pair: ", line,
], "")
AdvertisedRefProjectsEmptyBranch { remote, ref_names } =>
join([
at, " against ", remote as String,
" advertised ", to_string(count(ref_names)),
" head ref(s) projecting to an empty branch name: ",
join(ref_names, ", "),
], "")
}
}

type RemoteBranchObservation
= RemoteBranchesRead { branches: List<RemoteBranch> }
| RemoteBranchesUnreadable { detail: String }
| RemoteBranchesUnreadable { cause: RemoteBranchReadFailure }

data remote_ref_identity_note: String = "A REMOTE REF NAME IS NOT A PUBLICATION (review correction, 2026-07-31). The previous cut observed remote branches as bare strings, so the branch-without-pull-request arm established only that a ref with the right NAME existed — which is exactly the exact-head thesis this module claims to enforce, abandoned on the one path that had no pull request to compare against. A branch left over from an earlier attempt, or one the worker pushed and then rewrote, satisfied it.\\n\\nSo the observation carries ref identity, and the arm splits: at the expected head, or diverged from it. The diverged arm matters most on this path precisely because there is no pull request whose head would otherwise reveal the mismatch."

Expand Down Expand Up @@ -206,11 +246,11 @@ fn adjudicate_publication(
}
} else {
match remotes {
RemoteBranchesUnreadable { detail } =>
RemoteBranchesUnreadable { cause } =>
PublicationObservationRefused {
detail: join([
"no pull request targets this branch and base, and the remote refs could not be read, so whether the branch was pushed at all is unknown: ",
detail,
render_remote_branch_read_failure(cause: cause),
], ""),
}
RemoteBranchesRead { branches } =>
Expand Down
Loading
Loading