Coverage: accept Isabelle symbol identifiers in term/name positions#11
Merged
Conversation
The grammar only recognised a hardcoded list of Greek letters inside identifiers, so terms, names and variables written with other Isabelle symbols — `\<one>`, `\<bbbP>`, `\<P>`, `\<rho>` (with optional `\<^sub>` subscript) — were rejected in bare (unquoted) positions such as interpretation arguments and `case` bindings. Add a `SYMBOL` terminal for a non-structural `\<name>` (negative lookahead excludes the `\<open>`/`\<close>`/`\<comment>` cartouche markers and `\<^...>` control symbols) and accept it as an atom in `term`, `name`, and `embedded`. Before/after on a 400-file corpus sample: 0 regressions, +2 files now parse. Cartouche/comment handling unaffected; full unit suite green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
christiankissig
added a commit
that referenced
this pull request
Jul 7, 2026
The grammar only recognised a hardcoded list of Greek letters inside identifiers, so terms, names and variables written with other Isabelle symbols — `\<one>`, `\<bbbP>`, `\<P>`, `\<rho>` (with optional `\<^sub>` subscript) — were rejected in bare (unquoted) positions such as interpretation arguments and `case` bindings. Add a `SYMBOL` terminal for a non-structural `\<name>` (negative lookahead excludes the `\<open>`/`\<close>`/`\<comment>` cartouche markers and `\<^...>` control symbols) and accept it as an atom in `term`, `name`, and `embedded`. Before/after on a 400-file corpus sample: 0 regressions, +2 files now parse. Cartouche/comment handling unaffected; full unit suite green.
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.
Summary
First increment against the inner-syntax / proof long tail. From a clustered analysis of 259 real failure fragments, the largest addressable sub-pattern (beyond furthest-position artifacts and EOF) was Isabelle symbol identifiers used in bare positions:
\<one>,\<bbbP>,\<P>,\<rho>\<^sub>1, etc. The grammar only recognised a hardcoded Greek-letter list.This adds a
SYMBOLterminal — a non-structural\<name>(with optional\<^sub>subscript) whose negative lookahead excludes the\<open>/\<close>/\<comment>cartouche markers and\<^...>control symbols — and accepts it as an atom interm,name, andembedded. So e.g.interpretation g: foo \<bbbP> leq \<one> .andcase (step \<P> \<rho>)now parse.Testing
ruff/isortclean.Honest scope
This is the diffuse long tail: unlike the form-level PRs, individual fixes here yield small gains (≈+0.5% here) and there is no single high-value lever. The dominant remaining failure causes are furthest-position artifacts (the real failure is in a prior statement's content), unterminated/over-consuming constructs (EOF), and the broad space of inner-syntax/proof-method content — each needing its own incremental, well-regression-checked change. This PR is one such safe increment.
🤖 Generated with Claude Code