fix(tri): one population for the census, and a control that walks it the other way - #2933
Closed
gHashTag wants to merge 5 commits into
Closed
fix(tri): one population for the census, and a control that walks it the other way#2933gHashTag wants to merge 5 commits into
gHashTag wants to merge 5 commits into
Conversation
…the other way
`unparsed report` said 5 typecheck failures; `unparsed locate`, in the same
binary, said 2. Measured independently: 5 is right.
Two causes, both in `locate`:
* it walked its own corpus. `parse_failures` was lifted out last week with a
doc comment claiming disagreement was "structurally impossible", but only
`prose` was moved onto it -- `report` and `locate` kept their own
`git ls-files` loops. The comment described an intention, not the code.
* it checked whether the error named a LINE before it checked which STAGE
refused the file. Three typecheck failures print `Typecheck FAILED (6
errors, 0 warnings):` and no line at all, so they never reached the stage
check and were reported as "nothing claimed" -- a bucket that reads as "the
parse question was asked and went unanswered", when the question does not
apply. Its buckets summed to 80 against a population of 76.
`report` and `locate` now read the shared scope, which carries the stage split;
`locate_one` takes the error text the scope already has, so the file is
compiled once for the population instead of three times per spec. Measured on
all 76 parse failures: the in-place run and the temp-copy run named the same
line every time and neither left a failure without one -- a reason to keep one
ruler, not two.
locate: 57 confirmed + 14 refuted + 5 silent = 76, the population exactly
(was 57 + 14 + 9 = 80)
stages: 5 typecheck + 4 lex + 1 semantic = 10, which is what `prose` prints
New `tri unparsed agree`: the census asks git, this walks the working tree, and
both must name the same population and the same stage split. Three commands
reading one variable agree by construction, so their agreement measures
nothing; this is the axis that can still be wrong. It also names what the
census is blind to -- a spec on disk that git does not track.
Mutation-checked, both directions:
* a silent `specs/fpga/` filter in `parse_failures` -> DISAGREE, exit 1
* an untracked failing spec on disk -> named, gate stays green (the census
legitimately speaks only of tracked
specs; the point is naming it)
* a second corpus walk in `prose.rs` -> `one_corpus_walk` FAILS
* stage made to depend on the line -> the guard-order test FAILS
Refs #2864
Contributor
PR DashboardGenerated at: 2026-08-30 00:43:45 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
…mbered to 371-373 (master took 370)
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-30 00:52:45 UTC
Summary
Seal Status
|
…dence precondition (#2933)
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-30 00:54:13 UTC
Summary
Seal Status
|
Owner
Author
|
Reopened as a clean branch: two commits carried |
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
1 participant
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.
The disagreement
tri unparsed reportandtri unparsed locatelive in the same file, run fromthe same binary, and gave different answers about the same corpus:
Measured independently (745 specs,
t27c checkeach, classify by message): 5typecheck, 4 lex, 1 semantic.
reportwas right.Two causes
1.
locatewalked its own corpus.parse_failureswas lifted out lastweek carrying a doc comment that says disagreement is now "structurally
impossible rather than merely tested for" — but only
prosewas moved ontoit.
reportandlocatekept their owngit ls-filesloops. The commentdescribed the intention; the code kept three walks.
2.
locatechecked the message FORMAT before the error's STAGE. Threetypecheck failures print no line at all:
locate_onedemanded a line number first, so those never reached the stagecheck and landed in "nothing claimed" — a bucket that reads as the parse
question was asked and went unanswered, when the question does not apply to
them at all. Its buckets summed to 80 against a population of 76.
The existing test
locate_answers_only_for_parse_failureswas green throughout.It asserts that
stage_ofclassifies correctly — the presence of the helper,not the order in which the caller applies it.
The change
reportandlocatenow read the shared scope, which carries the stage split.locate_onetakes the error text the scope already holds, so a spec iscompiled once for the population instead of once more per command.
Before changing the ruler I checked it: on all 76 parse failures the in-place
run and the temp-copy run named the same line every time, and neither left
a failure without one. Zero divergence — a reason to keep one ruler, not two.
tri unparsed agreeThree commands reading one variable agree by construction, so their agreement
measures nothing. The new command builds the population the other way —
walking the working tree instead of asking git — and demands the same numbers:
It also names what the census is structurally blind to: a
.t27on disk thatgit does not track is invisible to every command here. That is reported, not
failed on — the census legitimately speaks only about tracked specs.
Mutation-checked, both directions
specs/fpga/filter insideparse_failuresrefused at TYPECHECK 4 vs 5 <- DISAGREE, exit 1on disk, NOT tracked 1 (1 of them fail), gate greenprose.rsone_corpus_walkFAILSstage_ofmade to require a line numberagreegreenChecks
cargo test -p tri— 378 passed, 0 failedcargo clippy --all-targets— one warning fewer than master (Scope.trackedwas dead); no new onesrustfmton the two touched files only; every hunk is inside code this PR editstools/wp18_selftest_gate.py— exit 0 (its "unparsed" is about SSOT, unrelated)Refs #2864
After merging master (#2926, #2934)
feat(typecheck): a constant must fit the type it declaresmoved the typecheckcount while this PR was open. The finding above was measured at
21c7f7c06;re-measured on the merged tree, with
tri unparsed agreedoing exactly the jobit was built for:
locate57 + 14 + 5 = 76; stages 10 + 4 + 1 = 15, which is whatprosenow prints. The three still agree, and the independent walk still confirms them
— which is the point: the numbers move, the agreement is what must not.
.claude/skills/ci-gatessections renumbered 370–372 → 371–373; master took370 in #2932.