Add Python 3.14 support#15
Open
christiankissig wants to merge 43 commits into
Open
Conversation
The `ml` rule only matched the lowercase literal "ml", but Isabelle's command is uppercase `ML`, so every `ML \<open>...\<close>` block (and the `ML_file`/`ML_val`/`local_setup` variants) failed to parse, taking the whole theory file down with an UnexpectedEOF. Recognise the uppercase command keywords and the common variants, and allow a quoted-string body for `ML_file "path"`. The cartouche body machinery already handled the `setup` case, so it covers these too. This is the single largest coverage gap in the AFP corpus (~930 files). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `class` rule required a trailing `begin local_theory end` block, but the body is optional in Isabelle: classes are commonly declared as a bare `class c = ord + assumes ...` with their instances proved separately. Make the body optional so bare class declarations parse. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
A `sort` could only be a bare identifier, so arities written with
string-quoted class names — e.g. `instantiation vec :: ("show") "show"`
or `("semiring_0", finite) semiring_0` — failed to parse. Accept a
QUOTED_STRING as a sort in addition to an identifier.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `mode` rule accepted `(input)` and `(ASCII)` but not `(output)`, so declarations such as `abbreviation (output) ...` and notations using the output-only print mode failed. Add `(output)`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`inductive_simps` had no grammar rule (only its sibling `inductive_cases` did), so any theory using it failed to parse. Add a rule mirroring `inductive_cases` and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
These commands only accepted a bare specification (primrec/primcorec
allowed just `(transfer)`), so option blocks like
`datatype (plugins del: size) ...` and `primrec (nonexhaustive) ...`
failed. Add a shared `spec_opts` rule. Its content regex excludes the
apostrophe so a leading type-argument list such as `('a, 'b)` is not
ambiguously consumed as an option block.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CI's `ruff format --check` flagged the test cases added in this branch (string-quote normalization and collapsing short implicitly-concatenated strings). No behavioural change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: support ML/FFI, bare class, quoted sorts, (output), inductive_simps, datatype options
`attribute_setup` had no grammar rule, so any theory defining a custom attribute failed to parse. Add a rule mirroring `method_setup` (`name = <ML text> [description]`, the ML body being a cartouche) and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`simproc_setup` had no grammar rule. Add one for the `name (pattern | ...) = <ML text>` form, where the patterns are inner- syntax terms and the body is a cartouche, and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
parse_translation, print_translation, typed_print_translation, parse_ast_translation and print_ast_translation had no grammar rule, so theories defining custom syntax translations failed. Add a shared `ml_translation` rule (command keyword followed by an ML text body) and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`oracle` had no grammar rule. Add one for the `name = <ML text>` form and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: add attribute_setup, simproc_setup, *_translation, oracle
Markers (\<^marker>\<open>…\<close>) attached to lemma/theorem/corollary/ proposition were not accepted, despite being widespread in the AFP (~460 occurrences, almost all of the form `lemma name: \<^marker>… "…"`). Allow an optional marker in the three positions where it occurs on a goal: right after the command keyword (`goal`), after the thmdecl inside `props` (the common short-statement path), and after the thmdecl in `long_statement` (the `shows`-form). Markers begin with the distinctive \<^marker> terminal, so the added optional slots introduce no ambiguity. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Markers also appear on `definition`, both right after the keyword (`definition\<^marker>… name where …`) and after `where` (`definition name where \<^marker>… "…"`). Add an optional marker in both positions. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: support \<^marker> on goal commands and definition
`code_printing` had no grammar rule, so any theory with target-language code setup failed outright. Add rules covering the forms found across the AFP: - entities: constant / type_constructor / type_class / class_relation / class_instance (with `:: sort`) / code_module, with quoted-string names; - all three mapping arrows (\<rightharpoonup>, \<rightleftharpoons>, =>); - printings per target `(T) template`, multiple joined by `and`, multiple entries joined by `|`; - templates: a string/cartouche body, an `infix[l|r] N` declaration, or `-` to erase the printing for a target. Targets use the permissive `name` (real code uses targets beyond the SML/OCaml/Haskell/Scala/Eval set, e.g. Go). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: add code_printing
ParsingError._source_hint() returned the literal string "source_hint" when no source location was available, which got appended verbatim to the error message (e.g. "...timed out after 2.0ssource_hint"). Return an empty string instead so location-less errors read cleanly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Earley parser's chart grows super-linearly with input size, so a large/ambiguous theory file can take minutes in predict_and_complete and hang the caller (~15% of the AFP corpus exceeds 15s, correlating with file size). The parse loop is pure Python, so SIGALRM interrupts it cleanly. Add a `timeout` parameter to parse() (and a `--timeout/-t` CLI flag) that aborts with a ParsingError when exceeded, leaving normal parsing unchanged by default. The limit uses SIGALRM and so applies only on the main thread of a Unix process; elsewhere it is silently skipped. The SIGALRM handler and timer are always restored. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Parser robustness: guard against Earley chart blow-up with an opt-in timeout
The package referenced README.rst as its readme but the file was empty. Document what the parser is (Lark/Earley parser for Isabelle/Isar outer syntax), its work-in-progress status, installation, CLI usage (incl. --timeout), the public API (parse/load_parser/ParsingError), and the dev workflow. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add a README
`context` was reachable both as a direct alternative of the top-level `theory` rule and via `theory -> statement -> context`, so every theory had (at least) two parses at the root, multiplying the Earley chart for the whole file. `statement` already provides `context`, so the direct alternative is removed. Measured on proof snippets: ambiguous-node counts drop ~33% (e.g. a nested proof 6682 -> 4455), with 0 regressions and 2 of 6 sampled timeouts recovered. Full unit suite still green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`by` appeared both as a repeated proof step and as a terminal proof step in `proof_prove`, so any proof ending in `by ...` had two parses, compounding through nested proofs. The repeated-step `by` already covers the terminal position, so the terminal copy is removed. Measured on proof snippets (on top of the previous fix): ambiguous-node counts drop a further ~40% (nested proof 4455 -> 2707; by simp 7 -> 3), with 0 real regressions (ok->fail) on the sampled corpus. Full unit suite still green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar hygiene: remove two redundant parse paths (ambiguity reduction)
TYPE_IDENT only matched ASCII type variables (`'a`), so type variables written with Greek symbols (`'\<alpha>`, `'\<beta>`) — common in the AFP — were rejected wherever type variables appear (type_synonym, datatype, typedef, …). Extend TYPE_IDENT to allow a `\<name>` symbol after the apostrophe. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
class_spec only allowed a single parent class name before the context elements, so `class c = foo + bar + linorder` (a chain of superclasses, common in algebraic-hierarchy entries) failed. Allow a `+`-separated list of parent class names, optionally followed by `+ <context elements>`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`datatype` used `generic_type` for its left-hand side, which treats type
arguments as opaque types and rejects sort annotations like
`datatype ('a::type) box = ...`. Switch to `typespec_sorts`, which is the
correct shape for a type specification (`(tvar::sort, ...) name`) and
already handles plain and Greek type variables.
Verified against a corpus sample of real datatype declarations: 0 new
regressions vs the previous grammar (one additional declaration now
parses). Full unit suite green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: multiple superclasses, sort-annotated & Greek type variables
datatype type arguments could be plain or sort-annotated type variables,
but not the BNF annotations `dead 'a` (dead variable) or selector-style
`name: 'a` (set-function name), e.g.
`datatype ('s, dead 'p) t` / `datatype (dverts: 'a, darcs: 'b) graph`.
Introduce a datatype-specific `dt_typespec` that allows these.
Regression-checked against a corpus sample of real datatype declarations:
0 new regressions. Full unit suite green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`nominal_datatype` (Nominal2 entries) has the same outer shape as `datatype`, so accept it through the same rule. Binder annotations in constructors remain out of scope, but plain nominal datatypes now parse. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `method` definition command can bind parameters, e.g. `method m for x :: "'a" and y = ...`. Allow an optional `for_fixes` clause between the method name and `=`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`unbundle` could only take a list of bundle names; the optional `(in target)` qualifier (e.g. `unbundle (in foo) no bar`) was rejected. Allow it before the bundle list. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Grammar coverage: niche form gaps (datatype BNF annotations, nominal_datatype, method for-params, unbundle in-target)
Add CI/CD build status (GitHub Actions), Python-version, and license badges below the title. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add status badges to the README
… the README (#12) * Add weekly metrics workflow (AFP coverage + performance) A new `metrics` GitHub Actions workflow measures parser coverage and performance against the latest AFP release and publishes the figures into the README: - Triggers: weekly cron (Mon 04:00 UTC) + manual workflow_dispatch (with an optional sample-size input). Not on push, so normal CI is unaffected. - Corpus: downloads afp-current.tar.gz via metrics/fetch_corpus.sh, cached per ISO week (refreshes weekly, reused for same-week re-runs). - Measurement: metrics/measure.py parses a seeded random sample with a per-file timeout and records coverage %, timeout %, throughput, and median parse time to metrics/metrics.json. - Publishing: metrics/update_readme.py rewrites the block between the `.. METRICS:START` / `.. METRICS:END` markers in README.rst with an RST table; the job commits it back with the default GITHUB_TOKEN and `[skip ci]` (no workflow retrigger), staying green on no-op weeks. corpus/ is gitignored. The metrics scripts pass ruff/isort/mypy. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci: re-trigger checks [empty] * Fix mypy str/bytes error in update_readme (avoid re.subn overload) CI's mypy flagged the re.subn lambda's overload resolution as bytes. Replace the regex-callable replacement with a plain marker splice; drop the now-unused re import. * Fix fetch_corpus.sh aborting on tar|head SIGPIPE under pipefail Found by actually running the fetch: 'tar -tzf | head -1' under set -o pipefail makes tar receive SIGPIPE (head closes early), failing the pipeline and aborting before extraction. Detect the release name from the extracted directory instead (drop --strip-components so the afp-* dir is present); verified end-to-end against the live AFP tarball (10098 .thy files, version afp-2026-06-01, idempotent re-run). --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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>
* metrics: rebase-and-retry the commit-back push The metrics run takes several minutes; if master advances meanwhile (e.g. a PR is merged), the bot's push is rejected with 'fetch first'. Rebase onto origin/master and retry the push a few times. * ci: trigger
… legacy markup (#14) * Accept cartouche RHS in type_synonym declarations `type_synonym name = \<open>...\<close>` (cartouche-delimited inner syntax, as opposed to a "..." string) failed to parse: the type_synonym rule only allowed `ID | QUOTED_STRING` on the right of `=`, while every other inner-syntax position already routes through `embedded`, which accepts cartouches. Add `cartouche` to the alternatives. 43 AFP thy files use this form. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept private/qualified modifiers on top-level commands `private` and `qualified` are local-theory command modifiers. The `local_theory` rule (block bodies of context/locale/instantiation) already allowed them, but the top-level `theory` rule did not, so a bare `qualified definition ...` / `private lemma ...` directly under `theory ... begin` failed to parse. Mirror the optional `("private" | "qualified")?` prefix onto the top-level goal/statement alternatives. 328 AFP thy files use these modifiers (qualified is standard in HOL/Library at the global theory level). Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept \<^sub> subscripts in type variables and typespec names TYPE_IDENT only matched plain/Greek type variables (`'a`, `'\<alpha>`), not subscripted ones (`'a\<^sub>h`), even though inner-syntax type positions already accept them. As a result `datatype`/`type_synonym`/ `typedecl` declarations whose type arguments or constructor names carry `\<^sub>` subscripts failed to parse (e.g. AFP's ADS_Construction: `datatype 'a\<^sub>h blindable\<^sub>h = ...`). Extend the TYPE_IDENT terminal with a `\<^sub>...` segment (ordered first in the repeat group so the empty-matching alternative doesn't pre-empt it). Also allow a bare TYPE_IDENT on the type_synonym RHS (`type_synonym 'a foo = 'a`). Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept repeated and symbol subscripts in identifier names The `name` terminal allowed at most one `\<^sub>X` segment per identifier and its standalone-subscript alternative had a stray backslash (so it never matched). Identifiers with multiple subscripts (`Seq\<^sub>p\<^sub>t\<^sub>i`, `lang\<^sub>M\<^sub>2\<^sub>L`) or a symbol after the subscript marker (`\<Delta>\<^sub>\<epsilon>`) therefore truncated mid-name, failing every command that names such an entity (definition, lemmas, abbreviation, interpretation, ...). Make the subscript segment repeatable (`?` -> `*`) and fix the standalone `\<^sub>` alternative so subscripts can chain into following Greek/symbol glyphs. 142 AFP files use multi-subscript command names; 773 use a subscript-then-symbol identifier somewhere. Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept qualified class names in sort/arity positions `sort` only allowed a bare ID or quoted string, so a qualified class name (`heap.rep`) in an arity failed: `instance unit :: heap.rep ..`. Add the existing LONG_IDENT terminal (dotted identifier) as a sort alternative, which also covers qualified classes anywhere a sort is accepted. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept (in -) target, ctor discriminators, qualified attribute args Three independent gaps found by statement-level localization: - `(in -)` local-theory target (global scope) on definition/abbreviation/ etc. — the target rule only allowed `(in name)`. ~94 AFP files. - datatype constructor discriminators: `datatype t = is_PUSH: PUSH | ...` — a constructor may carry a leading `discr:` name. Added the optional `(name ":")?` prefix to both constructor alternatives. - qualified fact names as attribute arguments: `[simplified bar.inject]`, `[OF foo.bar]` — the `arg` rule accepted ID but not LONG_IDENT, so a dotted fact reference inside `[...]` failed. Very common (~960 files use a dotted name inside an attribute bracket). Adds regression tests for each. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept custom print-mode names in mode annotations The `mode` rule only allowed the literal modes `input`/`output`/`ASCII` inside parentheses, so a custom print mode — `abbreviation (latex) ...`, `notation (do_notation) ...`, the modal-logic `(uniA_i)` modes — failed. Add the general `"(" name ")"` form. ~104 AFP files use a custom print mode on abbreviation/notation. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept qualified type names on the type_synonym RHS `type_synonym error = String.literal` (and other `A.b` qualified type names) failed: the RHS allowed ID/TYPE_IDENT/QUOTED_STRING/cartouche but not LONG_IDENT. Add it. ~21 AFP files. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Accept legacy {* ... *} verbatim markup in document and ML blocks Pre-2016 Isabelle used {* ... *} (rather than cartouches) for document text and ML/source bodies. Neither parsed: section/subsection/text/etc. accepted only cartouche/string/ID, and the ML/setup/local_setup rule only cartouche/name/string. Add a VERBATIM_TEXT terminal (/\{\*...\*\}/, non-greedy) and wire it into doc_block and the ml rule. Deliberately NOT added to the hot `embedded` rule (rare legacy method_setup bodies aren't worth the Earley breadth). ~66 AFP files use {* — 22 in doc commands, ~56 in ML/ML_val/setup blocks. Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Apply ruff format to test additions CI `ruff format --check` flagged the new test cases. No semantic change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
- CI: add 3.14 to the test matrix and bump actions/setup-python v4 -> v5 (v5 reliably provides the 3.14 toolchain; v4 is legacy). - Declare the supported interpreters (3.10-3.14) via project classifiers; requires-python = ">=3.10" already permits 3.14. Verified locally on CPython 3.14.4: full test suite (166 passed) and `ruff check` are green; CI mypy scope (isabelle_parser/) is unaffected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
Adds CPython 3.14 to the supported/tested set.
Changes
.github/workflows/ci.yml): add"3.14"to the test matrix; bumpactions/setup-pythonv4→v5so the runner reliably provisions the 3.14toolchain (v4 is legacy).
pyproject.toml): declare supported interpreters 3.10–3.14 viaclassifiers.
requires-python = ">=3.10"already permits 3.14.Verification (local, CPython 3.14.4)
pip install -e ".[test]"— clean installpytest— 166 passedruff check .— cleanisabelle_parser/(thescripts/dir is gitignored andnot in CI's checkout), which is clean on 3.14.
No source changes were needed — the parser runs as-is on 3.14.
🤖 Generated with Claude Code