From 21a027f9ad2005476146b4f4412d3dd74cc3ded9 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 17:49:10 +0100 Subject: [PATCH 1/2] 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 2/2] 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