A module name is a name: reading all of it unblocked six specs - #2882
Merged
Conversation
`module github::auth {` did not parse. The module-name reader took one
identifier plus its hyphenated tail and stopped, so the parser met a colon at
module level and reported something else entirely. Nine specs on master declare
a path-qualified module and none of them parsed.
The repair is not to give `::` a meaning -- it is to read the whole NAME. The
reader is now a loop over `::`-separated segments, each of which may still be
hyphenated, because `module tritype-base;` was already legal.
BOTH colons are required before either is consumed. A single `:` after a module
name is not a path, and swallowing it would turn a real error into a stranger
one further down. The path reader elsewhere in this file consumes one colon and
then optionally a second; copying that idiom verbatim would have inherited the
looser rule.
specs that parse 621 -> 627, ZERO regressions
seal drift 537 -> 543, exactly the six new specs
hollow seals 187 -> 175
specs that generate 626 -> 632
debt ledger 90 -> 84
The drift figure is the control that matters: a module name is emitted into
generated code, so the change could have moved output for specs that already
parsed. It moved for exactly the six and no others.
Three of the nine still do not parse -- audio_overview, youtube_transcript and
relay_observer have further obstacles past the module line, named in the PR.
FROZEN_HASH is updated in the same commit, per M5 and per the practice: the
last 20 commits to compiler.rs all update it, and none is marked GOLD-RING.
Also adds `tri unparsed report [--list]`: the work queue, ranked by the
construct on the failing line rather than by the compiler's message. Its own
first three readings were wrong and are fixed here -- it counted 21
deliberately-broken `fixtures/` files as debt when the repository's ledger
already omits them, lost upstream statements like `return x;` into "not
decided", and dropped four rows through a bare `continue`. The printed parts
now sum to the printed total.
Refs #2864
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
August 29, 2026 20:40
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 20:40:26 UTC
Summary
Seal Status
|
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
Adding the four github_* entries fired a second ratchet:
vacuous completeness theorems rose 40 -> 44. A theorem about an
empty module says nothing about its spec; the ledger's max_vacuous
moves down only.
The mark is correct, and I checked it after setting it rather than
before, which is the wrong order. `github_auth_module` in
Completeness.lean is `functions := [], globals := [], tests := []`. All
four are genuinely empty models.
Those four were ALWAYS vacuous. They became COUNTABLE, because #2882
made their specs parse and the classifier could finally disagree with
the theorem. Nothing new became vacuous.
Raised to 44 with the reason written into the ledger itself, including
the part that matters: this is the SECOND-BEST answer. The ratchet
exists to stop this number growing, and the right repair is to write
real Lean models for those four rather than to raise the cap. A raise
with a reason is not a raise that is justified -- it is one the next
reader can argue with.
Suite 2455 passed, 0 failed. `--test icarus_lowerable` 358 passed, 0
failed.
Refs #2882
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
* ledger: four github specs became classifiable, and the theorem is the stale side
`corpus_classifier_matches_lean_completeness` is red on master:
NEW Rust/Lean lowerability disagreement(s), not in the ledger:
github_auth, github_comments, github_issues, github_prs
-- Rust=false, Lean theorem=true
Not new work of mine: reproduced on a clean `origin/master` checkout
before touching anything, and none of the four specs contains the word
`else`, so the parser change in the branch this was found from cannot
reach them.
The cause is #2882, which taught the parser to read a hyphenated module
name whole and thereby unblocked six specs. Four of them are these. A
spec that did not parse could not be classified; now it can be, and the
classifier says `false`.
The classifier is right. `t27c gen-rust specs/github/auth.t27` exits 1
and emits 0 lines. The Lean theorem, written while the spec did not
parse at all, is the stale side.
So this is the same shape as #2862: not a regression, a measurement that
started working. Recorded with the reason each entry carries, in the
same field shape the other 73 use, and `max_entries` raised to match --
`--bless` equivalents in this repo do not raise the cap, and a blessed
ledger that still fails on the cap is not blessed.
Refs #2882
* ledger: raise max_vacuous 40 -> 44, and say why in the file
Adding the four github_* entries fired a second ratchet:
vacuous completeness theorems rose 40 -> 44. A theorem about an
empty module says nothing about its spec; the ledger's max_vacuous
moves down only.
The mark is correct, and I checked it after setting it rather than
before, which is the wrong order. `github_auth_module` in
Completeness.lean is `functions := [], globals := [], tests := []`. All
four are genuinely empty models.
Those four were ALWAYS vacuous. They became COUNTABLE, because #2882
made their specs parse and the classifier could finally disagree with
the theorem. Nothing new became vacuous.
Raised to 44 with the reason written into the ledger itself, including
the part that matters: this is the SECOND-BEST answer. The ratchet
exists to stop this number growing, and the right repair is to write
real Lean models for those four rather than to raise the cap. A raise
with a reason is not a raise that is justified -- it is one the next
reader can argue with.
Suite 2455 passed, 0 failed. `--test icarus_lowerable` 358 passed, 0
failed.
Refs #2882
This was referenced Aug 29, 2026
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
#2887) The corpus ratchet was red on master: UNEXPECTED FAILURES: 1 + specs/api/sdk_contract.t27 [parse-no-discard] UNEXPECTED PASSES : 19 - specs/api/c_api_contract.t27 [parse] (fixed -- remove from the ledger) ... eighteen more ... All nineteen are `[parse]`, and all nineteen are specs #2877 and #2882 unblocked -- thirteen by reading `#` as a line comment and six by reading a hyphenated module name whole. The ratchet fails on an improvement exactly as it fails on a regression, because an entry that starts passing must be removed, and that is the design. The one new failure is the same story from the other side. `specs/api/sdk_contract.t27` is in the passes list for `[parse]`: it now parses, and a spec that could not be parsed could not be measured for discard either. Not new loss -- newly countable loss. The entry says so. ledger 169 -> 151 max_entries 169 -> 151 RATCHET FAIL -> CLEAN `--bless-expectations` still does not raise `max_entries` and still writes `unclassified: blessed by --bless-expectations` as the reason. Both set by hand, as in #2862. Refs #2882
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
2 participants
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.
module github::auth {did not parse. The module-name reader took oneidentifier plus its hyphenated tail and stopped, so the parser met a colon at
module level and reported something else entirely. Nine specs on master
declare a path-qualified module and none of them parsed.
The repair is not to give
::a meaning — it is to read the whole name. Thereader is now a loop over
::-separated segments, each of which may still behyphenated, because
module tritype-base;was already legal and had to stay so.Both colons are required before either is consumed. A single
:after amodule name is not a path, and swallowing it would turn a real error into a
stranger one further down. The path reader elsewhere in
compiler.rsconsumesone colon and then optionally a second; copying that idiom verbatim would have
inherited the looser rule.
Result
The drift figure is the control that matters. A module name is emitted into
generated code, so this change could have moved output for specs that already
parsed. It moved for exactly the six new ones and no others — 543 − 537 = 6.
Controls
module github::auth { }module portable::relay_observer;module a::b::c { }module tritype-base;(hyphen, pre-existing)module Foo { }(plain, pre-existing)The three that still do not parse
They have obstacles past the module line, and the census now names them:
tri unparsed report [--list]The work queue, ranked by the construct on the failing line rather than by the
compiler's message — because the message names the state the parser recovered
into, not what stopped it.
Its own first three readings were wrong, and all three are fixed here:
fixtures/, brokenon purpose as detector inputs —
tools/specs_generate_baseline.txtalreadyomits all 21. They now get their own line rather than being dropped.
return x;orlet y = 1;inside a body fell into "not decided" when it is plainlyupstream.
through a bare
continue. The printed parts now sum to the printed total.On the freeze
FROZEN_HASHis updated in the same commit.FROZEN.md§5 asks for a[GOLD-RING]marking and a milestone or Architect approval; the commit historysays otherwise — the last 50 commits touching
compiler.rsinclude eight fromtoday,
FROZEN_HASHis updated in 20 of the last 20, and GOLD-RING appearsin none. I followed the practice and am saying so rather than assuming it.
Gates, run locally
specs generate 0 · specs parse 0 · conflict markers 0 · seal coverage
--self-check0 · seals fresh 0 · types ratchet 0 · skill check 0 ·cargo test -p tri0 (7 new tests inunparsed.rs) · bootstrap test ratchet 0 ·rustfmt --check cli/tri/src/unparsed.rs0.compiler.rsgains 10 lines of the file's pre-existing rustfmt churn (4064 onmaster); that file has never been formatted and doing so here would be unrelated.
Refs #2864