Fix Lean character literal token scanning - #809
Conversation
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e0a441b1a7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
|
|
||
| def _skip_char_literal(source: str, index: int, length: int) -> int: | ||
| return _skip_quoted_literal(source, index, length, "'") |
There was a problem hiding this comment.
Because proof accepts newlines, an input such as by exact True.intro\n'\n#eval <IO action>\n' makes this helper consume everything through the final apostrophe, so _validate_source never sees the forbidden # command. Lean treats the malformed character token as an error and can recover to process later top-level commands, allowing injected evaluation or other side effects before the inspection is marked incomplete; bound character scanning to Lean's single-character escape grammar and reject a missing immediate closing delimiter rather than searching arbitrarily far ahead.
AGENTS.md reference: AGENTS.md:L16-L17
Useful? React with 👍 / 👎.
1 participant
Fixes #753.
The previous character-literal scanner only skipped a backslash and one following character. Valid Lean
\xHHand\uHHHHliterals could therefore leak hexadecimal characters into source-token inspection.This change routes string and character literals through one delimiter-aware scanner. It skips escaped characters and scans through the matching closing delimiter, preserving the existing behavior for strings while correctly handling every current Lean character escape form.
The issue mentions
\u{...}; Lean itself uses\uHHHH. The fix is grammar-agnostic within quoted literals, rather than adding a brace-escape special case.Validation:
make test-component TESTS=tests/component/providers/lean/test_lean_proof_axioms.pymake lint-fullThe repository test plan selected suite fallback because this module is transitively re-exported; the focused component regression suite directly exercises the modified behavior.