tri discard classify: what the parser stopped on, grouped - #2775
Merged
Conversation
A ranked list says WHERE the tokens are. It does not say whether the top six
entries are six problems or one. They were one:
class specs tokens
forall/==> (quantified) 38 20991
var/const statement 18 7020
assert 17 1853
other 14 587
TOTAL 87 30451
Sixty-nine percent of what is left is a construct the grammar does not contain --
quantified invariants, `forall x : T ... ==> ...`, in 38 specs mostly under
specs/igla/race/. That is a language decision, not a parser rung: what a
universally quantified invariant means at codegen commits four backends, and
`==>` lowered to `!a || b` makes a false antecedent a pass, which is the vacuous
shape `no-vacuous-invariant` exists to catch arriving through the front door.
Filed as #2774 rather than implemented.
Two things worth pinning, and both are tested:
* CLASSES is ordered and first match wins. A quantified invariant whose body
also declares a `var` must land in the quantified bucket; reordering the list
silently re-attributes thousands of tokens.
* `==>` NEVER APPEARS IN A DROP TRACE. The lexer splits it, so the trace reads
`== 4 == >`. A matcher for the source spelling finds zero of the 38, and the
conclusion would have been that the construct is rare.
A spec that yields no trace is counted separately and NOT as `other`: no trace
was read, so no cause is claimed.
Skill 159-161: rank to find the biggest, classify before deciding what KIND of
work it is; match what the trace says rather than what the source says, because
the lexer sits between them and is the thing under investigation; and a number
written before it was measured is still a wrong number.
Refs #2774
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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 01:41:07 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.
Refs #2774
A ranked list says where the tokens are. It does not say whether the top six entries are six problems or one.
They were one. Sixty-nine percent of the remaining discard is a construct the grammar does not contain:
Thirty-eight specs, mostly under
specs/igla/race/. Filed as #2774 rather than implemented — what a universally quantified invariant means at codegen commits four backends, and==>lowered to!a || bmakes a false antecedent a pass, which is the vacuous shapeno-vacuous-invariantexists to catch, arriving through the front door.Two things worth pinning, both tested
Order matters.
CLASSESis tested first-match-wins: a quantified invariant whose body also declares avarmust land in the quantified bucket. Reordering the list silently re-attributes thousands of tokens.==>never appears in a drop trace. The lexer splits it, so the trace readsA matcher for the source spelling would have found zero of the thirty-eight and I would have concluded the construct was rare. Match what the trace says, not what the source says — there is a lexer between them and it is the thing under investigation.
A spec that yields no trace is counted separately and not as
other: no trace was read, so no cause is claimed.Cross-checked
The numbers above were first produced by a throwaway Python script, then reproduced exactly by this command. Two independent implementations agreeing is the only reason I am quoting them.
🤖 Generated with Claude Code