From c8b896e6825d8103091672b6e5e16dc8d1dcb4be Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:17:19 +0100 Subject: [PATCH 01/33] Support ML/FFI commands (ML, ML_file, ML_val, setup, ...) The `ml` rule only matched the lowercase literal "ml", but Isabelle's command is uppercase `ML`, so every `ML \...\` 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) --- isabelle_parser/thy_grammar.lark | 3 ++- tests/test_parser.py | 28 ++++++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6b5da08..c91ade4 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2176,7 +2176,8 @@ spec: name ("\\" | "==") term ("(" "unchecked" ")")? # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.10 # -ml : ("ml" | "setup") (name | cartouche) +ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" + | "SML_file" | "setup" | "local_setup" ) (name | cartouche | QUOTED_STRING) # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.12.2 diff --git a/tests/test_parser.py b/tests/test_parser.py index 4ea2206..5a79b25 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -548,6 +548,34 @@ "end", True, ), + # ----------------------------------------------------------------------- + # ML / FFI commands (ML body delimited by a cartouche) + # ----------------------------------------------------------------------- + ( + "ml_block", + "theory T imports Main begin\nML \\val x = 1\\\nend", + True, + ), + ( + "ml_val_block", + "theory T imports Main begin\nML_val \\writeln \"hi\"\\\nend", + True, + ), + ( + "ml_file_cartouche", + "theory T imports Main begin\nML_file \\foo.ML\\\nend", + True, + ), + ( + "ml_file_quoted", + 'theory T imports Main begin\nML_file "foo.ML"\nend', + True, + ), + ( + "setup_block", + "theory T imports Main begin\nsetup \\Foo.bar\\\nend", + True, + ), ], ) def test_parse(name, test_input, expected): From 36714829f40229f869db6fe755b82eff1f40fe4a Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:18:57 +0100 Subject: [PATCH 02/33] Allow class definitions without a begin..end body 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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index c91ade4..f9b67c2 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2139,7 +2139,7 @@ definitions: "defines" definitions_item ("and" definitions_item)* # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.8 # -class: "class" class_spec "begin" local_theory "end" +class: "class" class_spec ("begin" local_theory "end")? class_spec: name "=" ( (name opening? "+" context_elem+) | (name opening?) diff --git a/tests/test_parser.py b/tests/test_parser.py index 5a79b25..c40feba 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -576,6 +576,23 @@ "theory T imports Main begin\nsetup \\Foo.bar\\\nend", True, ), + # ----------------------------------------------------------------------- + # class definitions without a begin..end body + # ----------------------------------------------------------------------- + ( + "class_no_body", + "theory T imports Main begin\n" + 'class c = ord + assumes le: "x \\ x"\n' + "end", + True, + ), + ( + "class_with_body", + "theory T imports Main begin\n" + "class c = ord\nbegin\nend\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 3a10f58ee0020b389dadbb8ce004666214e9de46 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:20:01 +0100 Subject: [PATCH 03/33] Allow quoted class names in sorts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index f9b67c2..122b41f 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1787,7 +1787,7 @@ typespec_sorts: typeargs_sorts? name # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 3.3.6 # -sort: ID +sort: ID | QUOTED_STRING sort_list_comma_sep: sort ("," sort)* diff --git a/tests/test_parser.py b/tests/test_parser.py index c40feba..6a9376c 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -593,6 +593,24 @@ "end", True, ), + # ----------------------------------------------------------------------- + # quoted sort/class names in arities + # ----------------------------------------------------------------------- + ( + "instantiation_quoted_sort", + "theory T imports Main begin\n" + 'instantiation vec :: ("show") "show"\nbegin\ninstance sorry\nend\n' + "end", + True, + ), + ( + "instantiation_quoted_multi_sort", + "theory T imports Main begin\n" + 'instantiation sq_matrix :: ("semiring_0", finite) semiring_0\n' + "begin\ninstance sorry\nend\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From ff0201deca7f294ac0bb05949092007af8c8c1b0 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:20:58 +0100 Subject: [PATCH 04/33] Support the (output) print mode 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) --- isabelle_parser/thy_grammar.lark | 1 + tests/test_parser.py | 10 ++++++++++ 2 files changed, 11 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 122b41f..4475654 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2534,6 +2534,7 @@ notation: name mixfix # TODO mode: ID | "(" "input" ")" + | "(" "output" ")" | "(" "ASCII" ")" # diff --git a/tests/test_parser.py b/tests/test_parser.py index 6a9376c..923ed3c 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -611,6 +611,16 @@ "end", True, ), + # ----------------------------------------------------------------------- + # abbreviation with an (output) print mode + # ----------------------------------------------------------------------- + ( + "abbreviation_output_mode", + "theory T imports Main begin\n" + 'abbreviation (output) foo where "foo = x"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 2135561cdcf6cf5f6c4098bb072e051c5606945d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:22:07 +0100 Subject: [PATCH 05/33] Add the inductive_simps command `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) --- isabelle_parser/thy_grammar.lark | 3 +++ tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 4475654..6e0c035 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1621,6 +1621,7 @@ statement: abbreviation | hide_declarations | inductive | inductive_cases + | inductive_simps | instantiation | instantiation | interpretation_block @@ -2705,6 +2706,8 @@ param_arg_value: embedded inductive_cases: "inductive_cases" (thmdecl? prop+ ("and" thmdecl? prop+)*) +inductive_simps: "inductive_simps" (thmdecl? prop+ ("and" thmdecl? prop+)*) + # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 13 # diff --git a/tests/test_parser.py b/tests/test_parser.py index 923ed3c..c6dcd93 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -621,6 +621,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # inductive_simps command + # ----------------------------------------------------------------------- + ( + "inductive_simps", + "theory T imports Main begin\n" + 'inductive_simps foo: "P x"\n' + "end", + True, + ), + ( + "inductive_simps_and", + "theory T imports Main begin\n" + 'inductive_simps bar: "P x" and baz: "Q y"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From d690ed557ce2477bfe3d07396a82eaf29c58e96d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:23:56 +0100 Subject: [PATCH 06/33] Support option blocks on datatype/primrec/primcorec 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) --- isabelle_parser/thy_grammar.lark | 11 ++++++++--- tests/test_parser.py | 25 +++++++++++++++++++++++++ 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6e0c035..54eaa12 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2576,9 +2576,9 @@ inductive: ("inductive" | "inductive_set" | "coinductive" | "coinductive_set") ( # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 11.2 # -primrec: "primrec" ("(" "transfer" ")")? specification +primrec: "primrec" spec_opts? specification -primcorec: "primcorec" ("(" "transfer" ")")? specification +primcorec: "primcorec" spec_opts? specification fun_block: "fun" opts? specification | ("function" | "nominal_function") opts? specification proof_prove @@ -2589,7 +2589,12 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" generic_type "=" constructors +datatype: "datatype" spec_opts? generic_type "=" constructors + +# Option block for spec commands, e.g. (plugins del: size), (nonexhaustive), +# (transfer). The excluded apostrophe keeps this from matching a leading type +# argument list such as ('a, 'b), which would otherwise be ambiguous. +spec_opts: "(" /[^()']+/ ")" generic_type : (type | ("(" type ("," type)*")")) name? diff --git a/tests/test_parser.py b/tests/test_parser.py index c6dcd93..b4087d6 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -638,6 +638,31 @@ "end", True, ), + # ----------------------------------------------------------------------- + # datatype / primrec option blocks + # ----------------------------------------------------------------------- + ( + "datatype_plugins_option", + "theory T imports Main begin\n" + "datatype (plugins del: size) 'a t = A 'a\n" + "end", + True, + ), + ( + "datatype_type_args_not_options", + "theory T imports Main begin\n" + "datatype ('a, 'b) pair = Pair 'a 'b\n" + "end", + True, + ), + ( + "primrec_nonexhaustive_option", + "theory T imports Main begin\n" + "datatype t = A | B\n" + 'primrec (nonexhaustive) f where "f A = A"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From e99d0202cc8701ee9c53e991cdef3a12d918851c Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 07:34:45 +0100 Subject: [PATCH 07/33] Apply ruff format to new test cases 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) --- tests/test_parser.py | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/tests/test_parser.py b/tests/test_parser.py index b4087d6..c97698f 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -558,7 +558,7 @@ ), ( "ml_val_block", - "theory T imports Main begin\nML_val \\writeln \"hi\"\\\nend", + 'theory T imports Main begin\nML_val \\writeln "hi"\\\nend', True, ), ( @@ -588,9 +588,7 @@ ), ( "class_with_body", - "theory T imports Main begin\n" - "class c = ord\nbegin\nend\n" - "end", + "theory T imports Main begin\nclass c = ord\nbegin\nend\nend", True, ), # ----------------------------------------------------------------------- @@ -626,9 +624,7 @@ # ----------------------------------------------------------------------- ( "inductive_simps", - "theory T imports Main begin\n" - 'inductive_simps foo: "P x"\n' - "end", + 'theory T imports Main begin\ninductive_simps foo: "P x"\nend', True, ), ( @@ -650,9 +646,7 @@ ), ( "datatype_type_args_not_options", - "theory T imports Main begin\n" - "datatype ('a, 'b) pair = Pair 'a 'b\n" - "end", + "theory T imports Main begin\ndatatype ('a, 'b) pair = Pair 'a 'b\nend", True, ), ( From cae865695d948e4642ff6b725ec6dea37f1ec7d1 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:02:34 +0100 Subject: [PATCH 08/33] Add the attribute_setup command `attribute_setup` had no grammar rule, so any theory defining a custom attribute failed to parse. Add a rule mirroring `method_setup` (`name = [description]`, the ML body being a cartouche) and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 3 +++ tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 54eaa12..73fea30 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1631,6 +1631,7 @@ statement: abbreviation | lifting_update | locale_block | locale_theory_context + | attribute_setup | marker | method_block | method_setup @@ -2447,6 +2448,8 @@ terminal_proof_steps: "." | ".." | "sorry" method_setup: "method_setup" name "=" text text? +attribute_setup: "attribute_setup" name "=" text text? + # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 6.5.1 # diff --git a/tests/test_parser.py b/tests/test_parser.py index c97698f..0db84f4 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -657,6 +657,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # attribute_setup (ML body delimited by a cartouche) + # ----------------------------------------------------------------------- + ( + "attribute_setup", + "theory T imports Main begin\n" + "attribute_setup foo = \\Attrib.thms\\\n" + "end", + True, + ), + ( + "attribute_setup_with_description", + "theory T imports Main begin\n" + 'attribute_setup foo = \\Attrib.thms\\ "a description"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 44417e665cd3191bf3a1a9f437ff769c1925f1b2 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:03:43 +0100 Subject: [PATCH 09/33] Add the simproc_setup command `simproc_setup` had no grammar rule. Add one for the `name (pattern | ...) = ` 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) --- isabelle_parser/thy_grammar.lark | 3 +++ tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 20 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 73fea30..405862a 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1634,6 +1634,7 @@ statement: abbreviation | attribute_setup | marker | method_block + | simproc_setup | method_setup | ml | named_theorems @@ -2450,6 +2451,8 @@ method_setup: "method_setup" name "=" text text? attribute_setup: "attribute_setup" name "=" text text? +simproc_setup: "simproc_setup" name "(" term ("|" term)* ")" "=" text + # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 6.5.1 # diff --git a/tests/test_parser.py b/tests/test_parser.py index 0db84f4..408f51f 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -674,6 +674,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # simproc_setup (pattern list + ML body) + # ----------------------------------------------------------------------- + ( + "simproc_setup", + "theory T imports Main begin\n" + 'simproc_setup foo ("x + y") = \\K (K (K NONE))\\\n' + "end", + True, + ), + ( + "simproc_setup_multi_pattern", + "theory T imports Main begin\n" + 'simproc_setup foo ("x + y" | "x * y") = \\K (K (K NONE))\\\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From a7db2ddd025dbc6299fca95afca0deecc7b5e962 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:04:56 +0100 Subject: [PATCH 10/33] Add syntax/AST translation commands 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) --- isabelle_parser/thy_grammar.lark | 5 +++++ tests/test_parser.py | 20 ++++++++++++++++++++ 2 files changed, 25 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 405862a..63bea48 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1634,6 +1634,7 @@ statement: abbreviation | attribute_setup | marker | method_block + | ml_translation | simproc_setup | method_setup | ml @@ -2453,6 +2454,10 @@ attribute_setup: "attribute_setup" name "=" text text? simproc_setup: "simproc_setup" name "(" term ("|" term)* ")" "=" text +ml_translation: ( "parse_translation" | "print_translation" + | "typed_print_translation" | "parse_ast_translation" + | "print_ast_translation" ) text + # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 6.5.1 # diff --git a/tests/test_parser.py b/tests/test_parser.py index 408f51f..9cc9f4f 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -691,6 +691,26 @@ "end", True, ), + # ----------------------------------------------------------------------- + # syntax/AST translation commands (ML body) + # ----------------------------------------------------------------------- + ( + "parse_translation", + "theory T imports Main begin\nparse_translation \\[]\\\nend", + True, + ), + ( + "print_translation", + "theory T imports Main begin\nprint_translation \\[]\\\nend", + True, + ), + ( + "typed_print_translation", + "theory T imports Main begin\n" + "typed_print_translation \\[]\\\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 292b0dad6946f8fd689bf49d0166bb63789ccc1a Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:06:17 +0100 Subject: [PATCH 11/33] Add the oracle command `oracle` had no grammar rule. Add one for the `name = ` form and wire it into the statement dispatch. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 3 +++ tests/test_parser.py | 10 ++++++++++ 2 files changed, 13 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 63bea48..a08ab90 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1635,6 +1635,7 @@ statement: abbreviation | marker | method_block | ml_translation + | oracle | simproc_setup | method_setup | ml @@ -2458,6 +2459,8 @@ ml_translation: ( "parse_translation" | "print_translation" | "typed_print_translation" | "parse_ast_translation" | "print_ast_translation" ) text +oracle: "oracle" name "=" text + # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 6.5.1 # diff --git a/tests/test_parser.py b/tests/test_parser.py index 9cc9f4f..1888433 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -711,6 +711,16 @@ "end", True, ), + # ----------------------------------------------------------------------- + # oracle (ML body) + # ----------------------------------------------------------------------- + ( + "oracle", + "theory T imports Main begin\n" + "oracle myoracle = \\fn _ => @{cterm True}\\\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 95214d29a10fb58a70e91b2a91ecb613530e5071 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:20:01 +0100 Subject: [PATCH 12/33] Support \<^marker> on goal commands MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Markers (\<^marker>\…\) 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) --- isabelle_parser/thy_grammar.lark | 6 +++--- tests/test_parser.py | 26 ++++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index a08ab90..ddfead9 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1807,7 +1807,7 @@ vars: var ("and" var)* var: name+ ("::" type)? comment_block? | name ("::" type)? mixfix comment_block? -props: comment_block* thmdecl? comment_block* (prop prop_pat? is_syntax?)+ comment_block* +props: comment_block* thmdecl? marker? comment_block* (prop prop_pat? is_syntax?)+ comment_block* prop_list_with_pat: prop prop_pat? is_syntax? ("and"? prop prop_pat? is_syntax?)* @@ -2365,7 +2365,7 @@ assms : "assms" # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 6.2.4 # -goal: ("lemma" | "theorem" | "corollary" | "proposition" | "schematic_goal") ("(" "in" name ")")? "%invisible"? (long_statement | short_statement) +goal: ("lemma" | "theorem" | "corollary" | "proposition" | "schematic_goal") ("(" "in" name ")")? "%invisible"? marker? (long_statement | short_statement) have: "have" stmt cond_stmt? for_fixes? @@ -2381,7 +2381,7 @@ cond_stmt: ("if" | "when") stmt short_statement: stmt ("if" stmt)? for_fixes? -long_statement: thmdecl? comment_block? statement_context conclusion +long_statement: thmdecl? marker? comment_block? statement_context conclusion statement_context: includes? context_elem* diff --git a/tests/test_parser.py b/tests/test_parser.py index 1888433..1a0ddeb 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -721,6 +721,32 @@ "end", True, ), + # ----------------------------------------------------------------------- + # \<^marker> attached to goal commands + # ----------------------------------------------------------------------- + ( + "marker_after_thmdecl", + "theory T imports Main begin\n" + "lemma foo: \\<^marker>\\contributor \\A Name\\\\\n" + ' "x = x" by simp\n' + "end", + True, + ), + ( + "marker_after_thmdecl_with_attrs", + "theory T imports Main begin\n" + "lemma foo[simp]: \\<^marker>\\tag value\\ " + '"x = x" by simp\n' + "end", + True, + ), + ( + "marker_after_keyword", + "theory T imports Main begin\n" + 'lemma \\<^marker>\\tag value\\ foo: "x = x" by simp\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 2336a8a342516c451a271b03159d8b04fe2f456d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:21:36 +0100 Subject: [PATCH 13/33] Support \<^marker> on definition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index ddfead9..c661057 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2052,7 +2052,7 @@ unbundle: "unbundle" name* decl: name ("::" (ID | QUOTED_STRING | cartouche))? comment_block? mixfix? comment_block? "where" comment_block? -definition: "definition" local_theory_target? decl? thmdecl? prop spec_prems? for_fixes? +definition: "definition" marker? local_theory_target? decl? thmdecl? marker? prop spec_prems? for_fixes? abbreviation: "abbreviation" local_theory_target? mode? decl? prop for_fixes? diff --git a/tests/test_parser.py b/tests/test_parser.py index 1a0ddeb..bf2f61f 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -747,6 +747,21 @@ "end", True, ), + ( + "marker_on_definition_after_keyword", + "theory T imports Main begin\n" + "definition\\<^marker>\\tag value\\ foo " + 'where "foo = (0::nat)"\n' + "end", + True, + ), + ( + "marker_on_definition_after_where", + "theory T imports Main begin\n" + 'definition foo where \\<^marker>\\tag value\\ "foo = (0::nat)"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 0b80d9341d35bd8a413761b494dd28c91339f405 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 11:59:02 +0100 Subject: [PATCH 14/33] Add the code_printing command `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 (\, \, =>); - 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) --- isabelle_parser/thy_grammar.lark | 24 ++++++++++++++++ tests/test_parser.py | 49 ++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index c661057..cd1e9e6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1611,6 +1611,7 @@ statement: abbreviation | declaration | declare | definition + | code_printing | doc_block | experiment | export_code @@ -2731,6 +2732,29 @@ inductive_simps: "inductive_simps" (thmdecl? prop+ ("and" thmdecl? prop+)*) # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 13 # +code_printing: "code_printing" code_print_decl ("|" code_print_decl)* + +code_print_decl: code_symbol (code_arrow code_printings?)? + +code_arrow: "\" | "\" | "=>" + +code_symbol: "constant" (name | QUOTED_STRING) + | "type_constructor" (name | QUOTED_STRING) + | "type_class" (name | QUOTED_STRING) + | "class_relation" (name | QUOTED_STRING) + | "class_instance" (name | QUOTED_STRING) "::" (name | QUOTED_STRING) + | "code_module" (name | QUOTED_STRING) + +code_printings: code_target_print ("and" code_target_print)* + +code_target_print: "(" name ")" code_template? + +# A printing is a template string/cartouche, an optional infix declaration, or +# "-" to erase the printing for that target. +code_template: ("infix" | "infixl" | "infixr") NAT (QUOTED_STRING | cartouche) + | (QUOTED_STRING | cartouche) + | "-" + export_code : "open" const_expr_list export_target_list | const_expr_list export_target_list diff --git a/tests/test_parser.py b/tests/test_parser.py index bf2f61f..b17f316 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -762,6 +762,55 @@ "end", True, ), + # ----------------------------------------------------------------------- + # code_printing + # ----------------------------------------------------------------------- + ( + "code_printing_constant", + "theory T imports Main begin\n" + 'code_printing constant the \\ (Haskell) "MaybeExt.fromJust"\n' + "end", + True, + ), + ( + "code_printing_multi_entry", + "theory T imports Main begin\n" + "code_printing\n" + ' type_constructor bool \\ (Go) "bool"\n' + '| constant "True::bool" \\ (Go) "true"\n' + "end", + True, + ), + ( + "code_printing_infixl", + "theory T imports Main begin\n" + 'code_printing constant HOL.conj \\ (Go) infixl 1 "&&"\n' + "end", + True, + ), + ( + "code_printing_ascii_arrow_and_erase", + "theory T imports Main begin\n" + 'code_printing class_instance bit :: "HOL.equal" => (Haskell) -\n' + "end", + True, + ), + ( + "code_printing_module_cartouche", + "theory T imports Main begin\n" + "code_printing code_module MaybeExt \\ (Haskell)\n" + " \\module MaybeExt(fromJust) where\n\n" + " import Data.Maybe(fromJust);\\\n" + "end", + True, + ), + ( + "code_printing_multi_target", + "theory T imports Main begin\n" + 'code_printing constant c \\ (Haskell) "a" and (OCaml) "b"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 02946248aca7cf2286d1dede7785fbb31cad64fd Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 14:05:17 +0100 Subject: [PATCH 15/33] Don't leak the "source_hint" placeholder into error messages 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) --- isabelle_parser/error.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/isabelle_parser/error.py b/isabelle_parser/error.py index 9b78bf1..91efd90 100644 --- a/isabelle_parser/error.py +++ b/isabelle_parser/error.py @@ -26,7 +26,7 @@ def _source_hint(self) -> str: print(line) underline = " " * (self.column - 1) + "^" * len(self.token) return f"\n\n{line}\n{underline}\n" - return "source_hint" + return "" def __str__(self) -> str: location_info = "" From 79444bee90282b28137c37d1e178cb7e4d1ea8e1 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 14:05:17 +0100 Subject: [PATCH 16/33] Add an opt-in parse timeout to guard against Earley blow-up 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) --- isabelle_parser/cli.py | 10 +++++- isabelle_parser/thy_parser.py | 57 +++++++++++++++++++++++++++++++-- tests/test_thy_parser.py | 60 ++++++++++++++++++++++++++++++++++- 3 files changed, 122 insertions(+), 5 deletions(-) diff --git a/isabelle_parser/cli.py b/isabelle_parser/cli.py index 9fa8889..917f458 100644 --- a/isabelle_parser/cli.py +++ b/isabelle_parser/cli.py @@ -14,6 +14,14 @@ def main() -> None: arg_parser.add_argument( "-f", "--file", action="store_true", help="Interpret input as a filename" ) + arg_parser.add_argument( + "-t", + "--timeout", + type=float, + default=None, + help="Abort the parse after this many seconds (guards against " + "pathological inputs that grow the Earley chart super-linearly)", + ) # Parse arguments args = arg_parser.parse_args() @@ -31,7 +39,7 @@ def main() -> None: # Lex and parse try: - result = parse(data) + result = parse(data, timeout=args.timeout) except ParsingError as e: print("Parsing failed due to errors.") print(f"Error: {e.with_source_code(data)}") diff --git a/isabelle_parser/thy_parser.py b/isabelle_parser/thy_parser.py index c23a94b..8f6feb3 100644 --- a/isabelle_parser/thy_parser.py +++ b/isabelle_parser/thy_parser.py @@ -1,13 +1,52 @@ import logging import os -from typing import Any, List +import signal +import threading +from contextlib import contextmanager +from typing import Any, Iterator, List from lark import Lark, Transformer, Tree from lark.tree import Meta +from .error import ParsingError + logger = logging.getLogger(__name__) +class _ParseTimeout(Exception): + """Internal signal that a parse exceeded its time budget.""" + + +@contextmanager +def _time_limit(seconds: float | None) -> Iterator[None]: + """Abort the wrapped block after ``seconds`` using SIGALRM. + + The Earley parser can grow its chart super-linearly with input size, so a + large/ambiguous theory file can take minutes. SIGALRM interrupts the + pure-Python parse loop cleanly. It is only available on the main thread of a + Unix process; in any other context (worker threads, platforms without + SIGALRM) the limit is silently skipped and parsing proceeds without a bound. + """ + if ( + not seconds + or not hasattr(signal, "SIGALRM") + or threading.current_thread() is not threading.main_thread() + ): + yield + return + + def _handler(signum: int, frame: Any) -> None: + raise _ParseTimeout() + + previous = signal.signal(signal.SIGALRM, _handler) + signal.setitimer(signal.ITIMER_REAL, seconds) + try: + yield + finally: + signal.setitimer(signal.ITIMER_REAL, 0) + signal.signal(signal.SIGALRM, previous) + + def load_parser(start: str = "start") -> Lark: # Construct the path to the .lark file grammar_path = os.path.join(os.path.dirname(__file__), "thy_grammar.lark") @@ -21,10 +60,22 @@ def load_parser(start: str = "start") -> Lark: return parser -def parse(input_text: str, parser: Lark | None = None) -> Any | None: +def parse( + input_text: str, parser: Lark | None = None, timeout: float | None = None +) -> Any | None: + """Parse ``input_text`` into a tree. + + ``timeout`` (seconds) bounds the parse: if it is exceeded a + :class:`ParsingError` is raised instead of letting a pathological file hang + the caller. See :func:`_time_limit` for its limitations. + """ if parser is None: parser = load_parser() - tree = parser.parse(input_text) + try: + with _time_limit(timeout): + tree = parser.parse(input_text) + except _ParseTimeout: + raise ParsingError(f"parsing timed out after {timeout}s") transformer = PositionPrinter() return transformer.transform(tree) diff --git a/tests/test_thy_parser.py b/tests/test_thy_parser.py index 0b66493..e99b435 100644 --- a/tests/test_thy_parser.py +++ b/tests/test_thy_parser.py @@ -14,10 +14,14 @@ test_thy_grammer.py. """ +import signal +import threading +import time + import pytest from lark import Lark, Tree -from isabelle_parser import load_parser +from isabelle_parser import ParsingError, load_parser from isabelle_parser.thy_parser import parse as _raw_parse @@ -64,3 +68,57 @@ def test_invalid_input_raises(src): """Invalid theory inputs must raise rather than return a result.""" with pytest.raises(Exception): _raw_parse(src, None) + + +class _SlowParser: + """Stand-in Lark parser whose parse() sleeps, to test the timeout path + deterministically without depending on a real pathological input.""" + + def __init__(self, seconds: float) -> None: + self.seconds = seconds + + def parse(self, _text: str): + time.sleep(self.seconds) + return Tree("start", []) + + +class TestParseTimeout: + def test_timeout_not_hit_returns_tree(self): + result = _raw_parse( + "theory T imports Main begin end", load_parser(), timeout=30 + ) + assert isinstance(result, Tree) + + def test_timeout_none_is_default(self): + result = _raw_parse("theory T imports Main begin end", load_parser()) + assert isinstance(result, Tree) + + def test_timeout_exceeded_raises_parsing_error(self): + with pytest.raises(ParsingError): + _raw_parse("ignored", _SlowParser(5), timeout=0.2) + + def test_timeout_exceeded_is_fast(self): + start = time.time() + with pytest.raises(ParsingError): + _raw_parse("ignored", _SlowParser(10), timeout=0.2) + assert time.time() - start < 2 # aborted promptly, not after 10s + + def test_sigalrm_handler_restored_after_parse(self): + sentinel = signal.getsignal(signal.SIGALRM) + _raw_parse("theory T imports Main begin end", load_parser(), timeout=30) + assert signal.getsignal(signal.SIGALRM) is sentinel + + def test_timeout_ignored_off_main_thread(self): + # SIGALRM is main-thread only; off-thread the limit is skipped and a + # normal (fast) parse still succeeds rather than erroring. + results = {} + + def run(): + results["tree"] = _raw_parse( + "theory T imports Main begin end", load_parser(), timeout=30 + ) + + t = threading.Thread(target=run) + t.start() + t.join() + assert isinstance(results["tree"], Tree) From 7489b86099e26347c3de70b60aaa03ff6221db37 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 14:20:44 +0100 Subject: [PATCH 17/33] Add a README 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) --- README.rst | 116 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) diff --git a/README.rst b/README.rst index e69de29..99a2387 100644 --- a/README.rst +++ b/README.rst @@ -0,0 +1,116 @@ +================ +isabelle_parser +================ + +A parser for `Isabelle/Isar `_ theory (``.thy``) +artifacts, implemented in pure Python on top of `Lark `_ +using an Earley grammar. + +It turns the outer syntax of a theory file — the theory header, document +markup, specifications (``definition``, ``datatype``, ``fun``, ``locale``, +``class``, …), Isar proofs and FFI/ML commands — into a Lark parse tree that you +can walk programmatically. + +Status +====== + +Work in progress. The grammar covers a large and growing share of the outer +syntax found in the `Archive of Formal Proofs `_, but +it is not yet complete: inner-syntax terms with exotic notation, some proof +methods, and a few rarely-used commands are still rejected. Treat a successful +parse as authoritative and a failure as "not yet supported" rather than "invalid +Isabelle". + +Requirements +============ + +* Python >= 3.10 +* `lark `_ + +Installation +============ + +From a clone of the repository: + +.. code-block:: bash + + pip install . + +For a development checkout (tests, linters): + +.. code-block:: bash + + pip install -e ".[dev]" + +Command-line usage +================== + +The CLI parses a file or a literal string and prints the resulting tree: + +.. code-block:: bash + + # parse a theory file + python -m isabelle_parser.cli -f path/to/Theory.thy + + # parse a literal string + python -m isabelle_parser.cli "theory T imports Main begin end" + +Options: + +``-f``, ``--file`` + Interpret the input argument as a filename rather than a literal string. + +``-t``, ``--timeout SECONDS`` + Abort the parse after ``SECONDS`` and report a failure instead of hanging. + The Earley chart can grow super-linearly on large or highly ambiguous files, + so this is a useful guard when parsing a whole corpus. + +The command exits non-zero if parsing fails. + +Library usage +============= + +.. code-block:: python + + from isabelle_parser import parse, load_parser, ParsingError + + source = "theory T imports Main begin\nlemma \"x = x\" by simp\nend" + + try: + tree = parse(source) + print(tree.pretty()) + except ParsingError as error: + print(f"parsing failed: {error}") + +``parse(input_text, parser=None, timeout=None)`` + Parse ``input_text`` and return a Lark ``Tree``. If ``parser`` is omitted a + default parser is built for the ``start`` rule. ``timeout`` (seconds) bounds + the parse and raises ``ParsingError`` if exceeded; it relies on ``SIGALRM`` + and therefore applies only on the main thread of a Unix process (it is + silently skipped elsewhere). + +``load_parser(start="start")`` + Build and return the underlying Lark parser, optionally starting from a + specific grammar rule. Reuse a single instance when parsing many files — + building the parser is the expensive part. + +``ParsingError`` + Raised for invalid input and on timeout. Lark may also raise its own + ``lark.exceptions.UnexpectedInput`` subclasses for structurally invalid input. + +Development +=========== + +.. code-block:: bash + + pytest # run the test suite + ruff check . # lint + ruff format . # format + isort . # import ordering + +The grammar lives in ``isabelle_parser/thy_grammar.lark``. + +License +======= + +MIT. See the ``LICENSE`` file. From 21a027f9ad2005476146b4f4412d3dd74cc3ded9 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 17:49:10 +0100 Subject: [PATCH 18/33] Reduce ambiguity: drop the duplicate context path in the theory rule `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) --- isabelle_parser/thy_grammar.lark | 1 - 1 file changed, 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index cd1e9e6..fb331bb 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1594,7 +1594,6 @@ context: ( print_locale | print_state )* theory: ( goal proof_prove - | context | statement | class_instance proof_prove | derive )* From 9e8ecc8da7ddd178f1dcc265662e44a1a15efc8c Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 18:11:09 +0100 Subject: [PATCH 19/33] Reduce ambiguity: drop the redundant terminal `by` in proof_prove `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) --- isabelle_parser/thy_grammar.lark | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index fb331bb..f278373 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2337,8 +2337,7 @@ proof_prove: ( show | with proof_chain )* ( terminal_proof_steps | qed | "oops" - | "done" - | by)? doc_block? + | "done")? doc_block? # QUOTED_STRING only found in AFP, not in Isabelle/Isar grammar conclusion: "shows" stmt From d38f705df01c8aac6bf0e973da8e79e397405aa3 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:22:56 +0100 Subject: [PATCH 20/33] Support Greek-letter type variables MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TYPE_IDENT only matched ASCII type variables (`'a`), so type variables written with Greek symbols (`'\`, `'\`) — common in the AFP — were rejected wherever type variables appear (type_synonym, datatype, typedef, …). Extend TYPE_IDENT to allow a `\` symbol after the apostrophe. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index f278373..aab0796 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1573,7 +1573,7 @@ TERM_VAR: /\?[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ TYPE_VAR: /'[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ // Other predefined tokens -TYPE_IDENT: /\'[a-zA-Z](_?\d*[a-zA-Z_\']*)*/ +TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(_?\d*[a-zA-Z_\']*)*/ SUBSCRIPT: "\\<^sub>" diff --git a/tests/test_parser.py b/tests/test_parser.py index b17f316..c411b33 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -811,6 +811,24 @@ "end", True, ), + # ----------------------------------------------------------------------- + # Greek type variables (e.g. '\) + # ----------------------------------------------------------------------- + ( + "type_synonym_greek_tvars", + "theory T imports Main begin\n" + "type_synonym ('\\, '\\) psubst = " + "\"'\\ \\ '\\\"\n" + "end", + True, + ), + ( + "datatype_greek_tvar", + "theory T imports Main begin\n" + "datatype '\\ wrap = Wrap '\\\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 141c20e531e684c1b524ac7402292cba61ede192 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:24:27 +0100 Subject: [PATCH 21/33] Support multiple superclasses in class declarations 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 `+ `. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 3 +-- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index aab0796..6fcab6d 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2146,8 +2146,7 @@ definitions: "defines" definitions_item ("and" definitions_item)* class: "class" class_spec ("begin" local_theory "end")? -class_spec: name "=" ( (name opening? "+" context_elem+) - | (name opening?) +class_spec: name "=" ( (name ("+" name)* opening? ("+" context_elem+)?) | (opening? "+" context_elem+) | context_elem+ ) instantiation? diff --git a/tests/test_parser.py b/tests/test_parser.py index c411b33..090f9ce 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -829,6 +829,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # class with multiple superclasses + # ----------------------------------------------------------------------- + ( + "class_multiple_superclasses", + "theory T imports Main begin\n" + "class c = ordered_ab_semigroup_add + comm_monoid_add + linorder\n" + "end", + True, + ), + ( + "class_superclasses_then_assumes", + "theory T imports Main begin\n" + 'class c = foo + bar + assumes le: "x \\ x"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From e1a7d8b3fad4ce378a938898b0af7e84f3c4e08e Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:27:44 +0100 Subject: [PATCH 22/33] Support sort-annotated type variables in datatype declarations `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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6fcab6d..d036a4c 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2601,7 +2601,7 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" spec_opts? generic_type "=" constructors +datatype: "datatype" spec_opts? typespec_sorts "=" constructors # Option block for spec commands, e.g. (plugins del: size), (nonexhaustive), # (transfer). The excluded apostrophe keeps this from matching a leading type diff --git a/tests/test_parser.py b/tests/test_parser.py index 090f9ce..3c0ebf5 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -846,6 +846,21 @@ "end", True, ), + # ----------------------------------------------------------------------- + # datatype with sort-annotated type variables + # ----------------------------------------------------------------------- + ( + "datatype_sort_annotated_tvar", + "theory T imports Main begin\ndatatype ('a::type) box = Box 'a\nend", + True, + ), + ( + "datatype_multi_sort_annotated_tvars", + "theory T imports Main begin\n" + "datatype ('a::type, 'b::finite) pair = Pair 'a 'b\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From da90f34a5c1ceb014f6b554eb3fa200813acd4cf Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:45:38 +0100 Subject: [PATCH 23/33] Support BNF type-argument annotations in datatype 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) --- isabelle_parser/thy_grammar.lark | 10 +++++++++- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index d036a4c..6b46ae6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2601,7 +2601,15 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" spec_opts? typespec_sorts "=" constructors +datatype: "datatype" spec_opts? dt_typespec "=" constructors + +# Type specification for datatype left-hand sides. Beyond plain and +# sort-annotated type variables it allows the BNF annotations `dead 'a` and +# selector-style `name: 'a`. +dt_typespec: dt_typeargs? name +dt_typeargs: dt_typearg + | "(" dt_typearg ("," dt_typearg)* ")" +dt_typearg: "dead"? (name ":")? TYPE_IDENT ("::" sort)? # Option block for spec commands, e.g. (plugins del: size), (nonexhaustive), # (transfer). The excluded apostrophe keeps this from matching a leading type diff --git a/tests/test_parser.py b/tests/test_parser.py index 3c0ebf5..b385624 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -861,6 +861,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # datatype BNF type-argument annotations (dead / selectors) + # ----------------------------------------------------------------------- + ( + "datatype_dead_tvars", + "theory T imports Main begin\n" + "datatype ('s, dead 'p, dead 'f) t = A 's\n" + "end", + True, + ), + ( + "datatype_selector_tvars", + "theory T imports Main begin\n" + "datatype (dverts: 'a, darcs: 'b) graph = G\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 9a521606db6388a2b227a123d5b31c7f85b885e3 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:46:49 +0100 Subject: [PATCH 24/33] Support the nominal_datatype command `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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6b46ae6..9935c05 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2601,7 +2601,7 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" spec_opts? dt_typespec "=" constructors +datatype: ("datatype" | "nominal_datatype") spec_opts? dt_typespec "=" constructors # Type specification for datatype left-hand sides. Beyond plain and # sort-annotated type variables it allows the BNF annotations `dead 'a` and diff --git a/tests/test_parser.py b/tests/test_parser.py index b385624..7cc87b5 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -878,6 +878,16 @@ "end", True, ), + # ----------------------------------------------------------------------- + # nominal_datatype (same shape as datatype) + # ----------------------------------------------------------------------- + ( + "nominal_datatype", + "theory T imports Main begin\n" + "nominal_datatype pi = PiNil | Tau pi | Sum pi pi\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From c7d5420fa143e8ad9e9708ebfa500a8ab361485d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:47:58 +0100 Subject: [PATCH 25/33] Support `for` parameters on the method command 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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 9935c05..ad86b67 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1670,7 +1670,7 @@ statement: abbreviation | value | values -method_block: "method" name "=" instruction +method_block: "method" name for_fixes? "=" instruction instruction: single_instruction | single_instruction instruction_modifier diff --git a/tests/test_parser.py b/tests/test_parser.py index 7cc87b5..3abc09d 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -888,6 +888,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # method definition with `for` parameters + # ----------------------------------------------------------------------- + ( + "method_with_for_param", + "theory T imports Main begin\n" + 'method interval_split for x :: "nat" = (rule x)\n' + "end", + True, + ), + ( + "method_with_for_and", + "theory T imports Main begin\n" + 'method m for a :: "\'a" and b :: "\'b" = (simp)\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 08086d85a8e689653ab3a0a06a29c9213fe7e324 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:49:53 +0100 Subject: [PATCH 26/33] Support the (in target) qualifier on unbundle `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) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index ad86b67..10aae13 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2044,7 +2044,7 @@ includes: "includes" name* opening: "opening" name* -unbundle: "unbundle" name* +unbundle: "unbundle" ("(" "in" name ")")? name* # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.4 diff --git a/tests/test_parser.py b/tests/test_parser.py index 3abc09d..19a3286 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -905,6 +905,14 @@ "end", True, ), + # ----------------------------------------------------------------------- + # unbundle with an (in target) qualifier + # ----------------------------------------------------------------------- + ( + "unbundle_in_target", + "theory T imports Main begin\nunbundle (in foo) no funcset_syntax\nend", + True, + ), ], ) def test_parse(name, test_input, expected): From 86a7afd6d255a6c08daf71134ca4fb1076f4df04 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 09:09:02 +0100 Subject: [PATCH 27/33] Add status badges to the README Add CI/CD build status (GitHub Actions), Python-version, and license badges below the title. Co-Authored-By: Claude Opus 4.8 (1M context) --- README.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/README.rst b/README.rst index 99a2387..ff728cd 100644 --- a/README.rst +++ b/README.rst @@ -2,6 +2,18 @@ isabelle_parser ================ +.. image:: https://github.com/christiankissig/python-isabelle-parser/actions/workflows/ci.yml/badge.svg?branch=master + :target: https://github.com/christiankissig/python-isabelle-parser/actions/workflows/ci.yml + :alt: CI/CD status + +.. image:: https://img.shields.io/badge/python-3.10%2B-blue.svg + :target: https://www.python.org/downloads/ + :alt: Python 3.10+ + +.. image:: https://img.shields.io/badge/license-MIT-green.svg + :target: https://github.com/christiankissig/python-isabelle-parser/blob/master/LICENSE + :alt: License: MIT + A parser for `Isabelle/Isar `_ theory (``.thy``) artifacts, implemented in pure Python on top of `Lark `_ using an Earley grammar. From 874eba70b242a4ca4f1b69866db078b35fa6b2d2 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:28:10 +0100 Subject: [PATCH 28/33] Add weekly metrics workflow (AFP coverage + performance) published to 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) * 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) --- .github/workflows/metrics.yml | 75 +++++++++++++++++++ .gitignore | 1 + README.rst | 13 ++++ metrics/fetch_corpus.sh | 27 +++++++ metrics/measure.py | 135 ++++++++++++++++++++++++++++++++++ metrics/update_readme.py | 67 +++++++++++++++++ 6 files changed, 318 insertions(+) create mode 100644 .github/workflows/metrics.yml create mode 100755 metrics/fetch_corpus.sh create mode 100644 metrics/measure.py create mode 100644 metrics/update_readme.py diff --git a/.github/workflows/metrics.yml b/.github/workflows/metrics.yml new file mode 100644 index 0000000..d3f0b5f --- /dev/null +++ b/.github/workflows/metrics.yml @@ -0,0 +1,75 @@ +name: metrics + +on: + workflow_dispatch: + inputs: + sample: + description: "Number of AFP files to sample" + default: "500" + schedule: + - cron: '0 4 * * 1' # 04:00 UTC every Monday + +# Allow the job to commit the refreshed README back to the repo. +permissions: + contents: write + +concurrency: + group: metrics + cancel-in-progress: false + +jobs: + metrics: + runs-on: ubuntu-latest + timeout-minutes: 60 + + steps: + - uses: actions/checkout@v4 + + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: "3.12" + + - name: Install Poetry + uses: snok/install-poetry@v1 + with: + version: latest + virtualenvs-create: true + virtualenvs-in-project: true + + - name: Install dependencies + run: poetry install --all-extras --no-interaction + + - name: Compute cache week + id: week + run: echo "week=$(date -u +%G-%V)" >> "$GITHUB_OUTPUT" + + - name: Cache AFP corpus + uses: actions/cache@v4 + with: + path: corpus + # Weekly key: refreshes the corpus each ISO week, reused within the + # week (e.g. for manual re-runs). No restore-keys, so a new week is a + # genuine miss and the fetch script downloads the latest release. + key: afp-corpus-${{ steps.week.outputs.week }} + + - name: Fetch AFP corpus + run: bash metrics/fetch_corpus.sh corpus + + - name: Measure coverage and performance + env: + METRICS_SAMPLE: ${{ github.event.inputs.sample || '500' }} + run: poetry run python metrics/measure.py + + - name: Update README + run: poetry run python metrics/update_readme.py + + - name: Commit refreshed metrics + run: | + git config user.name "metrics-bot" + git config user.email "metrics-bot@users.noreply.github.com" + git add README.rst metrics/metrics.json + # Pushing with the default GITHUB_TOKEN does not retrigger workflows; + # [skip ci] is belt-and-suspenders. No-op stays green. + git commit -m "chore: update AFP metrics [skip ci]" || { echo "no changes"; exit 0; } + git push diff --git a/.gitignore b/.gitignore index a928965..4c06dae 100644 --- a/.gitignore +++ b/.gitignore @@ -46,3 +46,4 @@ pip-wheel-metadata/ pytestdebug.log scripts/ src/_pytest/_version.py +corpus/ diff --git a/README.rst b/README.rst index ff728cd..2e68460 100644 --- a/README.rst +++ b/README.rst @@ -33,6 +33,19 @@ methods, and a few rarely-used commands are still rejected. Treat a successful parse as authoritative and a failure as "not yet supported" rather than "invalid Isabelle". +Metrics +======= + +Parser coverage and performance against the latest `Archive of Formal Proofs +`_ release, refreshed weekly by the ``metrics`` +workflow (and on demand via *Run workflow*): + +.. METRICS:START + +*Not measured yet — the* ``metrics`` *workflow populates this on its first run.* + +.. METRICS:END + Requirements ============ diff --git a/metrics/fetch_corpus.sh b/metrics/fetch_corpus.sh new file mode 100755 index 0000000..d6195d5 --- /dev/null +++ b/metrics/fetch_corpus.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +# Download and extract the latest AFP release into the corpus directory. +# No-op if the corpus is already present (e.g. restored from cache). +set -euo pipefail + +DEST="${1:-corpus}" +URL="${AFP_URL:-https://isa-afp.org/release/afp-current.tar.gz}" + +mkdir -p "$DEST" +if find "$DEST" -name '*.thy' -print -quit 2>/dev/null | grep -q .; then + echo "Corpus already present in '$DEST' ($(find "$DEST" -name '*.thy' | wc -l) .thy files) - skipping download." + exit 0 +fi + +echo "Downloading $URL ..." +tmp="$(mktemp --suffix=.tar.gz)" +curl -fsSL "$URL" -o "$tmp" + +echo "Extracting ..." +tar -xzf "$tmp" -C "$DEST" +rm -f "$tmp" + +# Record the release name: the extracted top-level directory (e.g. afp-2026-06-01). +version="$(find "$DEST" -maxdepth 1 -mindepth 1 -type d -name 'afp-*' -printf '%f\n' | head -1 || true)" +[ -n "$version" ] && echo "$version" > "$DEST/AFP_VERSION" + +echo "Extracted $(find "$DEST" -name '*.thy' | wc -l) .thy files (${version:-unknown})." diff --git a/metrics/measure.py b/metrics/measure.py new file mode 100644 index 0000000..d9d43dd --- /dev/null +++ b/metrics/measure.py @@ -0,0 +1,135 @@ +"""Measure parser coverage and performance against an AFP corpus. + +Parses a fixed (seeded) random sample of theory files from the corpus, recording +how many parse successfully and how fast, and writes the figures to +``metrics/metrics.json``. A per-file timeout bounds the run; timeouts count as +"not parsed" (the Earley chart can grow super-linearly on large files). + +Configuration via environment variables: + CORPUS_DIR corpus location (default: corpus) + METRICS_SAMPLE number of files to sample (default: 500; 0 = all) + METRICS_TIMEOUT per-file timeout in seconds (default: 15) + METRICS_SEED RNG seed for the sample (default: 42) + METRICS_OUT output path (default: metrics/metrics.json) +""" + +import datetime +import glob +import json +import os +import random +import signal +import statistics +import sys +import time +from concurrent.futures import ProcessPoolExecutor, as_completed +from typing import Any + +# Make isabelle_parser importable in pool workers regardless of start method +# (spawn/forkserver re-import this module, re-running this line) or whether the +# package is installed. +sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +CORPUS = os.environ.get("CORPUS_DIR", "corpus") +SAMPLE = int(os.environ.get("METRICS_SAMPLE", "500")) +TIMEOUT = int(os.environ.get("METRICS_TIMEOUT", "15")) +SEED = int(os.environ.get("METRICS_SEED", "42")) +OUT = os.environ.get("METRICS_OUT", "metrics/metrics.json") + +_parser = None + + +def _get_parser() -> Any: + global _parser + if _parser is None: + from isabelle_parser import load_parser + + _parser = load_parser() + return _parser + + +def _parse_one(path: str) -> tuple[str, int, float]: + try: + data = open(path, errors="replace").read() + except Exception: + return ("error", 0, 0.0) + size = len(data.encode("utf-8", "replace")) + + def _alarm(signum: int, frame: Any) -> None: + raise TimeoutError() + + signal.signal(signal.SIGALRM, _alarm) + signal.setitimer(signal.ITIMER_REAL, TIMEOUT) + start = time.time() + try: + _get_parser().parse(data) + status = "ok" + except TimeoutError: + status = "timeout" + except Exception: + status = "fail" + finally: + signal.setitimer(signal.ITIMER_REAL, 0) + return (status, size, time.time() - start) + + +def main() -> None: + files = sorted(glob.glob(os.path.join(CORPUS, "**", "*.thy"), recursive=True)) + if not files: + raise SystemExit(f"No .thy files found under '{CORPUS}'.") + random.seed(SEED) + random.shuffle(files) + if SAMPLE: + files = files[:SAMPLE] + + version = "unknown" + vfile = os.path.join(CORPUS, "AFP_VERSION") + if os.path.exists(vfile): + version = open(vfile).read().strip() + + workers = os.cpu_count() or 2 + counts = {"ok": 0, "fail": 0, "timeout": 0, "error": 0} + ok_times = [] + total_bytes = 0 + wall_start = time.time() + with ProcessPoolExecutor(max_workers=workers) as ex: + for fut in as_completed([ex.submit(_parse_one, f) for f in files]): + status, size, dt = fut.result() + counts[status] += 1 + total_bytes += size + if status == "ok": + ok_times.append(dt) + wall = time.time() - wall_start + + attempted = len(files) + metrics = { + "afp_version": version, + "sample_size": attempted, + "workers": workers, + "timeout_budget_s": TIMEOUT, + "ok": counts["ok"], + "fail": counts["fail"], + "timeout": counts["timeout"], + "error": counts["error"], + "coverage_pct": round(100 * counts["ok"] / attempted, 1), + "timeout_pct": round(100 * counts["timeout"] / attempted, 1), + "wall_seconds": round(wall, 1), + "files_per_sec": round(attempted / wall, 2) if wall else None, + "mb_per_sec": round(total_bytes / 1e6 / wall, 3) if wall else None, + "median_ok_parse_s": round(statistics.median(ok_times), 3) + if ok_times + else None, + "measured_at": datetime.datetime.now(datetime.timezone.utc).strftime( + "%Y-%m-%d %H:%M UTC" + ), + } + + os.makedirs(os.path.dirname(OUT), exist_ok=True) + with open(OUT, "w") as fh: + json.dump(metrics, fh, indent=2) + fh.write("\n") + print(json.dumps(metrics, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/metrics/update_readme.py b/metrics/update_readme.py new file mode 100644 index 0000000..7b0bfed --- /dev/null +++ b/metrics/update_readme.py @@ -0,0 +1,67 @@ +"""Inject the latest metrics into README.rst between the METRICS markers. + +Reads metrics/metrics.json and rewrites the block delimited by +``.. METRICS:START`` and ``.. METRICS:END`` with an RST table. +""" + +import json +import os +from typing import Any + +README = os.environ.get("README", "README.rst") +METRICS = os.environ.get("METRICS_OUT", "metrics/metrics.json") + + +def build_table(m: dict[str, Any]) -> str: + def row(metric: str, value: Any) -> str: + return f" * - {metric}\n - {value}\n" + + fps = m.get("files_per_sec") + mbs = m.get("mb_per_sec") + throughput = ( + f"{fps} files/s · {mbs} MB/s (×{m.get('workers', '?')} workers)" + if fps is not None + else "n/a" + ) + median = m.get("median_ok_parse_s") + median_s = f"{median} s" if median is not None else "n/a" + + table = ".. list-table::\n :header-rows: 1\n :widths: 45 55\n\n" + table += row("Metric", "Value") + table += row("AFP snapshot", m.get("afp_version", "unknown")) + table += row("Files sampled", m.get("sample_size", "?")) + table += row("Parse coverage", f"{m.get('coverage_pct')}% ({m.get('ok')} parsed)") + table += row( + f"Timeouts (> {m.get('timeout_budget_s')}s)", + f"{m.get('timeout_pct')}% ({m.get('timeout')})", + ) + table += row("Throughput", throughput) + table += row("Median parse time (parsed files)", median_s) + table += row("Measured", m.get("measured_at", "?")) + table += ( + "\n*Coverage is the share of a seeded random sample of AFP theory files " + "that parse within the timeout; a whole file counts as failed if any " + "statement fails. Updated weekly by the metrics workflow.*\n" + ) + return table + + +def main() -> None: + m = json.load(open(METRICS)) + text = open(README).read() + block = build_table(m) + start, end = ".. METRICS:START", ".. METRICS:END" + i = text.find(start) + j = text.find(end) + if i == -1 or j == -1 or j < i: + raise SystemExit( + "METRICS markers not found in README; expected " + "'.. METRICS:START' and '.. METRICS:END'." + ) + new = text[: i + len(start)] + "\n\n" + block + "\n" + text[j:] + open(README, "w").write(new) + print(f"Updated {README}.") + + +if __name__ == "__main__": + main() From fbd42e4570ef5dfe8073d69ab32ea977793f26e2 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:30:43 +0100 Subject: [PATCH 29/33] Accept Isabelle symbol identifiers (\) in term/name positions (#11) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The grammar only recognised a hardcoded list of Greek letters inside identifiers, so terms, names and variables written with other Isabelle symbols — `\`, `\`, `\

`, `\` (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 `\` (negative lookahead excludes the `\`/`\`/`\` 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) --- isabelle_parser/thy_grammar.lark | 6 +++++- tests/test_parser.py | 25 +++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 10aae13..816fd25 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1515,6 +1515,7 @@ COMMENT_CARTOUCHE: "\\" MARKER: "\\<^marker>" // Greek symbols +SYMBOL: /\\<(?!open>)(?!close>)(?!comment>)(?!\^)[A-Za-z][A-Za-z0-9]*>(\\<\^sub>[A-Za-z0-9_\x27]*)?/ GREEK: "\\" | "\\" | "\\" @@ -1709,6 +1710,7 @@ subgoal_params: "for" "..."? ("_" | name)+ # name: QUOTED_STRING + | SYMBOL | /[*]+/ | /[+]+/ | SYM_IDENT @@ -1737,6 +1739,7 @@ embedded: QUOTED_STRING | SYM_IDENT | TERM_VAR | TYPE_IDENT + | SYMBOL | cartouche # @@ -1752,7 +1755,8 @@ text: embedded type: embedded term: embedded - | "?"? (GREEK | ID)+ (SUBSCRIPT (FLOAT | ID))* "'"? + | SYMBOL + | "?"? (GREEK | ID | SYMBOL)+ (SUBSCRIPT (FLOAT | ID))* "'"? | "\\" | "\\" | "\\" diff --git a/tests/test_parser.py b/tests/test_parser.py index 19a3286..06e38a9 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -913,6 +913,31 @@ "theory T imports Main begin\nunbundle (in foo) no funcset_syntax\nend", True, ), + # ----------------------------------------------------------------------- + # Isabelle symbol identifiers (\) in term/name positions + # ----------------------------------------------------------------------- + ( + "symbol_term", + 'theory T imports Main begin\ndefinition "u = \\"\nend', + True, + ), + ( + "symbol_interpretation_args", + "theory T imports Main begin\n" + "interpretation g: foo \\ leq \\ .\n" + "end", + True, + ), + ( + "symbol_case_vars", + "theory T imports Main begin\n" + 'lemma "x = x"\n' + "proof (induct x)\n" + " case (step \\

\\) then show ?case by simp\n" + "qed\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 2db2bea2c43ec32bb027a7892617e74bcab09303 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:47:52 +0100 Subject: [PATCH 30/33] metrics: rebase-and-retry the commit-back push (#13) * 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 --- .github/workflows/metrics.yml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/.github/workflows/metrics.yml b/.github/workflows/metrics.yml index d3f0b5f..df519af 100644 --- a/.github/workflows/metrics.yml +++ b/.github/workflows/metrics.yml @@ -72,4 +72,12 @@ jobs: # Pushing with the default GITHUB_TOKEN does not retrigger workflows; # [skip ci] is belt-and-suspenders. No-op stays green. git commit -m "chore: update AFP metrics [skip ci]" || { echo "no changes"; exit 0; } - git push + # master may have advanced during the (multi-minute) run, which would + # reject the push; rebase onto the latest and retry a few times. + for attempt in 1 2 3 4 5; do + if git push; then exit 0; fi + echo "push rejected (attempt $attempt) - rebasing on origin/master ..." + git pull --rebase --autostash origin master + done + echo "failed to push metrics after retries" >&2 + exit 1 From baba51e93da3fcfb00f6f5cb9d3f0f06c591273b Mon Sep 17 00:00:00 2001 From: metrics-bot Date: Wed, 3 Jun 2026 09:58:46 +0000 Subject: [PATCH 31/33] chore: update AFP metrics [skip ci] --- README.rst | 23 ++++++++++++++++++++++- metrics/metrics.json | 17 +++++++++++++++++ 2 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 metrics/metrics.json diff --git a/README.rst b/README.rst index 2e68460..e8468f7 100644 --- a/README.rst +++ b/README.rst @@ -42,7 +42,28 @@ workflow (and on demand via *Run workflow*): .. METRICS:START -*Not measured yet — the* ``metrics`` *workflow populates this on its first run.* +.. list-table:: + :header-rows: 1 + :widths: 45 55 + + * - Metric + - Value + * - AFP snapshot + - afp-2026-06-01 + * - Files sampled + - 500 + * - Parse coverage + - 33.6% (168 parsed) + * - Timeouts (> 15s) + - 21.2% (106) + * - Throughput + - 0.81 files/s · 0.024 MB/s (×4 workers) + * - Median parse time (parsed files) + - 2.785 s + * - Measured + - 2026-06-03 09:58 UTC + +*Coverage is the share of a seeded random sample of AFP theory files that parse within the timeout; a whole file counts as failed if any statement fails. Updated weekly by the metrics workflow.* .. METRICS:END diff --git a/metrics/metrics.json b/metrics/metrics.json new file mode 100644 index 0000000..ab27fc8 --- /dev/null +++ b/metrics/metrics.json @@ -0,0 +1,17 @@ +{ + "afp_version": "afp-2026-06-01", + "sample_size": 500, + "workers": 4, + "timeout_budget_s": 15, + "ok": 168, + "fail": 226, + "timeout": 106, + "error": 0, + "coverage_pct": 33.6, + "timeout_pct": 21.2, + "wall_seconds": 614.6, + "files_per_sec": 0.81, + "mb_per_sec": 0.024, + "median_ok_parse_s": 2.785, + "measured_at": "2026-06-03 09:58 UTC" +} From 6285ac7d4b48f0999c750924056e7e8dc511ddaf Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 17:34:36 +0100 Subject: [PATCH 32/33] Grammar coverage: cartouches, modifiers, subscripts, qualified names, legacy markup (#14) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Accept cartouche RHS in type_synonym declarations `type_synonym name = \...\` (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) * 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) * Accept \<^sub> subscripts in type variables and typespec names TYPE_IDENT only matched plain/Greek type variables (`'a`, `'\`), 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) * 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 (`\\<^sub>\`) 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) * 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) * 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) * 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) * 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) * 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) * 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) --------- Co-authored-by: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 27 +++++---- tests/test_parser.py | 99 ++++++++++++++++++++++++++++++++ 2 files changed, 115 insertions(+), 11 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 816fd25..9fac9d6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -7,6 +7,9 @@ QUOTED_STRING: "\"" /[\s\S]*?/ "\"" | "`" /[\s\S]*?/ "`" +// Legacy (pre-2016) verbatim document/source text: {* ... *} +VERBATIM_TEXT: /\{\*[\s\S]*?\*\}/ + // Tokens for cartouche CARTOUCHE_OPEN: "\\" CARTOUCHE_TEXT: /[^\\]+/ @@ -1574,7 +1577,7 @@ TERM_VAR: /\?[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ TYPE_VAR: /'[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ // Other predefined tokens -TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(_?\d*[a-zA-Z_\']*)*/ +TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(\\<\^sub>[a-zA-Z0-9_\']*|_?\d*[a-zA-Z_\']*)*/ SUBSCRIPT: "\\<^sub>" @@ -1594,8 +1597,8 @@ context: ( print_locale | print_locales | print_state )* -theory: ( goal proof_prove - | statement +theory: ( ("private" | "qualified")? goal proof_prove + | ("private" | "qualified")? statement | class_instance proof_prove | derive )* @@ -1715,7 +1718,7 @@ name: QUOTED_STRING | /[+]+/ | SYM_IDENT // | (ID | GREEK | SUBSCRIPT | "." | "_" | NAT | "'" | letter)+ - | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)?)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/ + | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)*)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/ | "\\" par_name: "(" name ")" @@ -1796,7 +1799,7 @@ typespec_sorts: typeargs_sorts? name # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 3.3.6 # -sort: ID | QUOTED_STRING +sort: ID | LONG_IDENT | QUOTED_STRING sort_list_comma_sep: sort ("," sort)* @@ -1879,6 +1882,7 @@ attribute: "OF" thms args: arg* arg: ID + | LONG_IDENT | cartouche | "False" | "for" @@ -1945,7 +1949,7 @@ doc_block: ( "chapter" | "text" | "text_raw" | "txt" - | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | ID) + | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | VERBATIM_TEXT | ID) comment_block: COMMENT_CARTOUCHE cartouche @@ -2030,7 +2034,7 @@ thy_bounds: name | ("(" name ("|" name)* ")") locale_theory_context: "context" comment_block? name opening? "begin" local_theory "end" | "context" comment_block? includes? context_elem* "begin" local_theory "end" -local_theory_target: "(" "in" name ")" +local_theory_target: "(" "in" (name | "-") ")" # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.3 @@ -2185,7 +2189,7 @@ spec: name ("\\" | "==") term ("(" "unchecked" ")")? # ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" - | "SML_file" | "setup" | "local_setup" ) (name | cartouche | QUOTED_STRING) + | "SML_file" | "setup" | "local_setup" ) (name | cartouche | VERBATIM_TEXT | QUOTED_STRING) # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.12.2 @@ -2193,7 +2197,7 @@ ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" typedecl : "typedecl" typespec mixfix? -type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | QUOTED_STRING) mixfix? +type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | LONG_IDENT | TYPE_IDENT | QUOTED_STRING | cartouche) mixfix? # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.13 @@ -2553,6 +2557,7 @@ mode: ID | "(" "input" ")" | "(" "output" ")" | "(" "ASCII" ")" + | "(" name ")" # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 8.5.2 @@ -2624,8 +2629,8 @@ generic_type : (type | ("(" type ("," type)*")")) name? constructors : constructor ("|" constructor)* -constructor : comment_block? ID TYPE_IDENT mixfix? comment_block? - | comment_block? ( name +constructor : comment_block? (name ":")? ID TYPE_IDENT mixfix? comment_block? + | comment_block? (name ":")? ( name | cartouche | ("(" (cartouche | (name ":" name) | (name ":" QUOTED_STRING)) ")") )+ mixfix? comment_block? diff --git a/tests/test_parser.py b/tests/test_parser.py index 06e38a9..6043582 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -264,6 +264,40 @@ "theory T imports Main begin\ntype_synonym 'a mylist = \"'a list\"\nend", True, ), + ( + "type_synonym_cartouche", + "theory T imports Main begin\n" + "type_synonym int_poly = \\int mpoly\\\nend", + True, + ), + ( + "type_synonym_subscripted_type_vars", + "theory T imports Main begin\n" + "type_synonym ('a\\<^sub>h, 'b\\<^sub>h) sum\\<^sub>h = " + "\"'a\\<^sub>h + 'b\\<^sub>h\"\nend", + True, + ), + ( + "type_synonym_type_var_rhs", + "theory T imports Main begin\ntype_synonym 'a blindable = 'a\nend", + True, + ), + ( + "type_synonym_qualified_rhs", + "theory T imports Main begin\ntype_synonym error = String.literal\nend", + True, + ), + ( + "qualified_toplevel_definition", + "theory T imports Main begin\n" + 'qualified definition bar :: nat where "bar = 0"\nend', + True, + ), + ( + "private_toplevel_lemma", + 'theory T imports Main begin\nprivate lemma l: "x = x" by simp\nend', + True, + ), # ----------------------------------------------------------------------- # Constant declarations # ----------------------------------------------------------------------- @@ -609,6 +643,23 @@ "end", True, ), + ( + "instance_qualified_class_name", + "theory T imports Main begin\ninstance unit :: heap.rep ..\nend", + True, + ), + ( + "definition_global_target_dash", + "theory T imports Main begin\n" + 'definition (in -) foo :: nat where "foo = 0"\nend', + True, + ), + ( + "inductive_cases_qualified_attribute_arg", + "theory T imports Main begin\n" + 'inductive_cases fooCases[simplified bar.inject]: "P x"\nend', + True, + ), # ----------------------------------------------------------------------- # abbreviation with an (output) print mode # ----------------------------------------------------------------------- @@ -619,6 +670,25 @@ "end", True, ), + ( + "abbreviation_custom_print_mode", + "theory T imports Main begin\n" + 'abbreviation (latex) foo where "foo = x"\n' + "end", + True, + ), + ( + "legacy_verbatim_doc_markup", + "theory T imports Main begin\n" + "subsubsection {* Monotonicity *}\n" + "text {* some legacy text *}\nend", + True, + ), + ( + "legacy_verbatim_ml_block", + "theory T imports Main begin\nML {* val x = 1; fun f y = y + x *}\nend", + True, + ), # ----------------------------------------------------------------------- # inductive_simps command # ----------------------------------------------------------------------- @@ -830,6 +900,22 @@ True, ), # ----------------------------------------------------------------------- + # identifiers with repeated / symbol subscripts in name position + # ----------------------------------------------------------------------- + ( + "definition_repeated_subscript_name", + "theory T imports Main begin\n" + "definition lang\\<^sub>M\\<^sub>2\\<^sub>L :: nat where " + '"lang\\<^sub>M\\<^sub>2\\<^sub>L = 0"\nend', + True, + ), + ( + "lemmas_greek_symbol_subscript_name", + "theory T imports Main begin\n" + "lemmas \\\\<^sub>\\_cong = foo\nend", + True, + ), + # ----------------------------------------------------------------------- # class with multiple superclasses # ----------------------------------------------------------------------- ( @@ -854,6 +940,12 @@ "theory T imports Main begin\ndatatype ('a::type) box = Box 'a\nend", True, ), + ( + "datatype_constructor_discriminators", + "theory T imports Main begin\n" + "datatype pr_op = is_PUSH: PUSH | is_RELABEL: RELABEL\nend", + True, + ), ( "datatype_multi_sort_annotated_tvars", "theory T imports Main begin\n" @@ -861,6 +953,13 @@ "end", True, ), + ( + "datatype_subscripted_type_var_and_constructor", + "theory T imports Main begin\n" + "datatype 'a\\<^sub>h blindable\\<^sub>h = Content 'a\\<^sub>h\n" + "end", + True, + ), # ----------------------------------------------------------------------- # datatype BNF type-argument annotations (dead / selectors) # ----------------------------------------------------------------------- From 8b1c9d127c3181d2fec718cca18fbae50199b67e Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 17:42:43 +0100 Subject: [PATCH 33/33] Add Python 3.14 support - 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) --- .github/workflows/ci.yml | 8 ++++---- pyproject.toml | 5 +++++ 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5c39ff2..7b8df36 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,13 +13,13 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - python-version: ["3.10", "3.11", "3.12", "3.13"] + python-version: ["3.10", "3.11", "3.12", "3.13", "3.14"] steps: - uses: actions/checkout@v4 - name: Set up Python ${{ matrix.python-version }} - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: ${{ matrix.python-version }} @@ -68,7 +68,7 @@ jobs: - uses: actions/checkout@v4 - name: Set up Python - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: "3.11" @@ -94,7 +94,7 @@ jobs: - uses: actions/checkout@v4 - name: Set up Python - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 with: python-version: "3.11" diff --git a/pyproject.toml b/pyproject.toml index 183751c..f2c8574 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -19,6 +19,11 @@ dependencies = [ ] classifiers = [ "Programming Language :: Python :: 3", + "Programming Language :: Python :: 3.10", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Programming Language :: Python :: 3.13", + "Programming Language :: Python :: 3.14", "License :: OSI Approved :: MIT License", "Operating System :: OS Independent" ]