feat(tri): census audit says what it does not check, and why - #2947
Merged
Conversation
One row added and two refused, which is the more useful half.
ADDED -- `lean vacuous` prints 250 models, counted as `def NAME : Module := {`.
The counter counts `theorem` lines in Completeness.lean instead: a different
marker for the same population, and a real invariant -- one theorem per model --
that a hand-transcribed file of 250 entries can break in either direction.
Mutation: comment out one theorem and the row reads 250 against 249, exit 1.
REFUSED -- `types dup` prints 1180 struct definitions. A counter loose enough to
be independent reads 1182, and the two extra are
specs/lsp/schema.t27:155 struct = 21,
specs/lsp/schema.t27:204 struct = 22,
enum members named `struct`, which the census correctly rejects by requiring the
name to start with an ascii letter. The census is right. Any counter accurate
enough to agree with it is a copy of its matcher, which is the same reason
`seals hollow` was removed last pass.
REFUSED -- `discard classify` counts parser events produced at run time, not
artefacts on disk. Counting them a second way means running the same parser.
The pattern behind both refusals is worth naming: a census whose population is
defined by a MATCHER cannot have an independent counter, because any counter
precise enough to agree IS that matcher. Only a population defined by something
external -- files on disk, workspace members, a marker in a different file --
can honestly be counted twice.
So the audit now prints what it does not check and why. Its own coverage was the
same class it exists to catch: a page of green rows looks like the whole story
until somebody asks what is missing from it. Each exclusion carries the
measurement that produced it, because otherwise a reader cannot tell "looked and
could not" from "never looked".
lean vacuous 250 250 `theorem` lines in Completeness.lean
Not checked here, and why:
seals hollow built and removed; planting a seal moved BOTH numbers
types dup 1182 vs 1180, and the census is right
discard classify run-time events, not artefacts
A test refuses a census that appears in both lists, and refuses an exclusion
shorter than 60 characters -- an exclusion is a measurement, not a shrug. Both
mutation-checked.
cargo test -p tri 389 passed, 0 failed (was 387; two new)
cargo clippy 120 warnings, same as master
Refs #2864
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 13:40:06 UTC
Summary
Seal Status
|
…ed twice; an exclusion is a measurement (Refs #2864)
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 13:40:45 UTC
Summary
Seal Status
|
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.
One row added, two refused — and the refusals are the more useful half
Added:
lean vacuousThe census prints 250 models, counted as
def NAME : Module := {. Thecounter counts
theoremlines inCompleteness.leaninstead — a differentmarker for the same population, and a real invariant (one theorem per model)
that a hand-transcribed file of 250 entries can break in either direction.
Mutation: comment out one theorem →
250 vs 249, exit 1.Refused:
types dupThe census prints 1180 struct definitions. A counter loose enough to be
independent reads 1182, and the two extra are:
Enum members named
struct, which the census correctly rejects by requiringthe name to start with an ascii letter. The census is right. Any counter
accurate enough to agree with it is a copy of its matcher — the same reason
seals hollowwas removed last pass.Refused:
discard classifyIts population is parser events produced at run time, not artefacts on disk.
Counting them a second way means running the same parser, which is not a second
opinion.
The pattern behind both refusals
That is why the three original rows work:
.t27on disk,.rsunder workspacemembers, and the bare letters of a keyword.
The audit now states its own coverage
Its coverage was the same class it exists to catch — a page of green rows looks
like the whole story until somebody asks what is missing from it:
Each exclusion carries the measurement that produced it, because otherwise a
reader cannot tell "looked and could not" from "never looked".
Tests
nothing_is_both_checked_and_excusedrefuses a census in both lists, andrefuses an exclusion under 60 characters — an exclusion is a measurement, not
a shrug. Mutation-checked both ways:
mods orphanmods orphan is listed as unchecked and also has a row· FAIL"too hard"an exclusion is a measurement, not a shrug· FAILtheorem250 vs 249· exit 1Checks
cargo test -p tri— 389 passed, 0 failed (was 387; two new)cargo clippy --all-targets— 120 warnings, identical to masterRefs #2864