Parser robustness: guard against Earley chart blow-up with an opt-in timeout#5
Merged
Conversation
ParsingError._source_hint() returned the literal string "source_hint" when no source location was available, which got appended verbatim to the error message (e.g. "...timed out after 2.0ssource_hint"). Return an empty string instead so location-less errors read cleanly. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Earley parser's chart grows super-linearly with input size, so a large/ambiguous theory file can take minutes in predict_and_complete and hang the caller (~15% of the AFP corpus exceeds 15s, correlating with file size). The parse loop is pure Python, so SIGALRM interrupts it cleanly. Add a `timeout` parameter to parse() (and a `--timeout/-t` CLI flag) that aborts with a ParsingError when exceeded, leaving normal parsing unchanged by default. The limit uses SIGALRM and so applies only on the main thread of a Unix process; elsewhere it is silently skipped. The SIGALRM handler and timer are always restored. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
christiankissig
added a commit
that referenced
this pull request
Jul 7, 2026
Parser robustness: guard against Earley chart blow-up with an opt-in timeout
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Investigation
Profiled the ~15–20% "timeout" bucket from the coverage sweeps. Findings:
lark/parsers/earley.py:predict_and_complete— the Earley chart computation, pure Python. RSS climbs as the chart grows. It is not a regex/C wedge and not one pathological construct.Karatsuba_Runtime_Lemmas.thy(8 KB) finishes in 11.7 s. Parse time grows super-linearly with total file size (5.4 KB→4.4 s, 6.8 KB→7.9 s, 7.8 KB→11.7 s) — global grammar ambiguity, not a single line.contextualis unsupported withearley;basiccan't tokenize the grammar (it relies on the dynamic lexer's context sensitivity).The proper performance fix is reducing grammar ambiguity (a larger, separate effort). This PR delivers the robustness fix so a pathological file fails cleanly instead of hanging the caller.
Changes
parse(text, parser=None, timeout=None)— new opt-intimeout(seconds). On exceed, raisesParsingError("parsing timed out after Ns"). DefaultNone= unchanged behaviour.--timeout/-tCLI flag.setitimer; it applies only on the main thread of a Unix process (documented), is skipped elsewhere, and always restores the prior handler/timer.ParsingError._source_hint()no longer leaks the literal"source_hint"placeholder into location-less messages.Testing
cli … --timeout 3on a wedge file exits cleanly in ~3.4 s withError: parsing timed out after 3.0s; normal files unaffected.ruff check/ruff format/isortclean.Follow-up (not in this PR)
Reduce Earley ambiguity for an actual speed-up — candidate sources: overlapping
name/embedded/term regexes and the many optional/comment_block*/marker?slots that fan out the chart.🤖 Generated with Claude Code