Conversation
The extractor's `extractContextOpens` naively matched any line beginning with `open ` while scanning toward the target theorem, so an `open Classical in` inside an earlier `def` body was hoisted into the generated `Challenge.lean` and `Submission.lean` as a dangling `open Classical in`. That is a parse error which cascaded into confusing `Missing name after 'end'` failures. Recognize the scoped form by looking for an `in` token after the `open` keyword (ignoring trailing `--` line comments), and also peek past blank and comment-only lines to catch the multi-line variant where `in` sits on its own line. Closes #277. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`isScopedOpenLine` tokenized the raw stripped line, so a top-level `open Foo /- mentions in here -/` was misclassified as scoped (the `in` token landed inside the block comment) and silently dropped. Strip nested-balanced single-line `/- … -/` blocks before line comments, then tokenize. Multi-line block comments straddling an `open` command are still a gap; deferring those until something hits the case in practice. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
1 participant
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.
This PR fixes the extractor so that
open … inlines inside earlier definition bodies are no longer hoisted into the generatedChallenge.lean/Submission.leanas danglingopen … inlines.extractContextOpenspreviously matched any line starting withopen, so an indentedopen Classical ininside adefbody (as in PR #273's Sturm problem) leaked out and produced parse errors likeMissing name after 'end'.Two heuristics now classify a line as scoped and skip it:
openand anintoken appears after the keyword.--line comments are stripped first so that comments containing the word "in" don't cause false positives.openline, we peek past blank and comment-only lines; if the next syntactic line isinor starts within, we treat the whole thing as scoped.Regression tests in
tests/lean/EvalToolsTests/GenerateTest.leancover the original Sturm-style reproduction, the multi-lineinform, and the comment-with-infalse-positive case.Closes #277.
🤖 Prepared with Claude Code