Repository navigation
filesystem: read-outcome adoption row prose corrected; no live remainder claimed - #13262
Conversation
briansrls
left a comment
There was a problem hiding this comment.
The class distinctions are directionally useful, but the change does not yet make them operative. Three blockers.
- The typed carrier is unconsumed.
At this exact head, filesystem_read_outcome_adoption_excluded_classes occurs only twice: once as a name inside filesystem_read_outcome_adoption_standing's String and once in its own data declaration. Nothing imports it, matches it, joins it to a site, or uses it to produce/refuse the census. FileSystemReadOutcomeExcludedClass likewise has no per-site carrier or exhaustive consumer.
Therefore the claim "a new exclusion is a new constructor, never a new sentence" is not true yet. Adding a constructor changes no classification, and adding an excluded site still requires editing only the prose. The instrument the row says "must classify" is not present in this PR.
Please add an operative typed relation, for example a row carrying { subject: DeclarationRef, class: FileSystemReadOutcomeExcludedClass, owner/trigger/evidence }, and have the census/classifier consume it or produce a total Target | Excluded { class } disposition. A new constructor must force an exhaustive consumer change, and an unclassified non-target site must refuse.
- The class-specific facts are still prose, and one class is described imprecisely.
DomainReadFold is an honest distinction: proc_read_outcome preserves error_kind, which the shared FilesystemReadOutcome currently lacks, so the named unification trigger is real. But its owner, trigger, and member population remain embedded only in the String row.
ExactReadTyped is actually the separate filesystem_exact_read -> FilesystemExactRead authority, a richer fold with path, admitted failure kind, and unrecognized-kind arms. It is not a site flowing through filesystem_read_outcome's own typed shape. Name that authority and its disposition explicitly in the typed relation rather than letting "typed" absorb any alternative fold.
ArguedCollapse has the same issue: belt_read_or_empty and attempt_launch_revision_hex, their argument owners, and the falsification condition all remain prose. The three-constructor enum does not carry or check either member. Type the membership and evidence, or do not describe the exclusions as typed.
- The PR's stated main-state premise and measurement form are inaccurate.
The base file at 69b0527f3a8 does not point at missing declarations named FileSystemReadOutcomeExcludedClass or filesystem_read_outcome_adoption_excluded_classes. It carries the labels exact_read_typed and domain_read_fold only as prose. This PR is introducing those declaration identities, not repairing dangling references; update the PR body accordingly.
The new 222 / 102 / 65 remainder is also transcribed directly into the String while no producing census or immutable receipt is added. That contradicts this PR's own section-6 rationale. Once the typed site/disposition relation exists, derive the live remainder from it; otherwise name the reproducible producer and keep the current numeric reading out of the standing authority.
No objection to keeping the fork standing or to the three conceptual classes once they are carried and consumed at site grain. The blocker is that the accepted program still derives none of the classifications it now claims are typed.
… argued sites cited, evidence-wire reads counted), remainder re-measured at this head
d55738b to
21cedd2
Compare
briansrls
left a comment
There was a problem hiding this comment.
The prose-classification correction is now honest, and the inert declarations are gone. One DESIGN §6 blocker remains, plus the PR metadata still describes the discarded version.
- The row still transcribes the census output.
222 unconverted consumption sites across 102 files, of which 65 are fixtures is a current-tree measurement copied into a String authority. The nearby RE-DERIVATION recipe is not an instrument: it names no executable entry point, run, label, or persisted receipt that owns and re-derives the reading. DESIGN §6 is explicit: name the producer, never copy its numbers into prose; if a measurement is worth re-deriving, it needs an entry point.
Please remove the live numeric remainder from this row and name the actual census producer once that producer exists. Since the typed site relation and consumer are intentionally moving to the census PR, the honest interim statement here is that no committed producer currently supplies a live remainder—not another hand-updated reading. The same rule applies to the copied baseline numbers unless they are replaced by a citation to their real producing instrument/receipt rather than the outputs themselves.
The class prose itself is acceptable for this corrective cut: exact_read_typed now names the separate filesystem_exact_read authority; domain_read_fold states the error-kind distinction and unification obligation; argued_collapse names its two members and falsifier; and the two belt-actuate sites remain explicitly counted debt with an owner.
- The GitHub PR body/title are still stale at this exact head.
The actual diff is one String-row replacement (+1/-1) and adds no declaration. The current body still says +14/-1, claims FileSystemReadOutcomeExcludedClass and filesystem_read_outcome_adoption_excluded_classes are added, and says main contains prose references to those nonexistent declarations. Please rewrite it to match the final one-line correction and the corrected premise the author intended.
All four exact-head lanes are green; these are authority/description blockers, not build failures.
…is the named procedure, the census PR names the executable producer
briansrls
left a comment
There was a problem hiding this comment.
Approved at 3eabb1a.
The prior blockers are resolved by narrowing this to the honest one-line prose correction:
- no inert carrier or unconsumed declaration is added;
- exact_read_typed now names the separate filesystem_exact_read authority;
- domain_read_fold records the richer error-kind fork and its later unification obligation;
- argued_collapse names its two current members, their owning arguments, and the condition that falsifies the exemption;
- the two belt evidence reads remain counted debt and name the wire/owner that must grow;
- the stale baseline/remainder numbers are gone. The row now says plainly that no committed producer supplies a live remainder and names the re-derivation recipe plus the future census obligation rather than transcribing another current-tree reading.
The title and body now match the actual +1/-1, prose-only diff and correctly state that main had stale prose/numbers, not dangling typed references. Exact-head floor, generated, emit-build, and witnesses passed.
Reshape of the row-repair follow-up to #13106, per reviews 5406814177 and the side-chat verdicts: one line — the row
filesystem_read_outcome_adoption_standing's prose, corrected. No carriers, no declarations, no transcribed numbers.The premise, accurately: on current main the row's classes are prose-only and honest; nothing on main points at declarations that do not exist (an earlier iteration of this PR claimed otherwise — that premise was wrong and is corrected). What was stale on main: the REMAINDER sentence transcribed a pre-#13106 count ("91 across 47"), and the BASELINE copied its run's numbers into the standing authority.
What this diff does instead, per DESIGN §6 (name the instrument, never transcribe its output):
exact_read_typednames its authority (filesystem_exact_read);domain_read_fold(machine_intakeproc_read_outcome, the DESIGN 3 fork recorded to be unified by growing the shared fold);argued_collapseadded with members and citations (belt_read_or_empty— the annotation above its definition, review 45271, exempted in the absence row;attempt_launch_revision_hex— the presentation note ingunbc.roadmap_presentationpinned bydag/test/claim/roadmap/roadmap_presentation_witness_test.dag); and thebelt_workflow_attempt_evidence_for_keyadmission/spawn-failure reads named as COUNTED DEBT (the attempt evidence wire has no cause slot; the wire and its consumers are owned bygunbc.roadmap_belt_actuate).The typed per-site relation
{ subject, class, owner, trigger, evidence }and the totalTarget | Excluded { class }disposition land together with the .dag census that consumes them, in the census PR; the row will name that instrument when it lands.Verification: a one-line String prose correction to
dag/extdeps/filesystem/filesystem_io.dag; the module compiles on this tree (exit 0, zero errors). CI is the verifier.