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.
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".
Parser coverage and performance against the latest Archive of Formal Proofs release, refreshed weekly by the metrics
workflow (and on demand via Run workflow):
| Metric | Value |
|---|---|
| AFP snapshot | afp-2026-07-05 |
| Files sampled | 500 |
| Parse coverage | 29.2% (146 parsed) |
| Timeouts (> 15s) | 25.4% (127) |
| Throughput | 0.74 files/s · 0.022 MB/s (×4 workers) |
| Median parse time (parsed files) | 2.371 s |
| Measured | 2026-07-06 05:44 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.
- Python >= 3.10
- lark
From a clone of the repository:
pip install .For a development checkout (tests, linters):
pip install -e ".[dev]"The CLI parses a file or a literal string and prints the resulting tree:
# 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
SECONDSand 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.
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_textand return a LarkTree. Ifparseris omitted a default parser is built for thestartrule.timeout(seconds) bounds the parse and raisesParsingErrorif exceeded; it relies onSIGALRMand 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.UnexpectedInputsubclasses for structurally invalid input.
pytest # run the test suite
ruff check . # lint
ruff format . # format
isort . # import orderingThe grammar lives in isabelle_parser/thy_grammar.lark.
MIT. See the LICENSE file.