Conversation
Before this fix, when an `@[eval_problem]` theorem inherited binders from
a preceding `variable {n : Type*} [Fintype n] [DecidableEq n]` declaration,
`lake exe lean-eval generate` would slice only the literal theorem source
between `theorem <name>` and `:= by` into `Challenge.lean` / `Solution.lean`
/ `Submission.lean`, dropping the surrounding `variable` lines. With
`autoImplicit = false` in the generated workspace, identifiers like `n`
were then unbound and the build failed.
The new `extractContextVariables` walks the source up to the theorem,
tracking `section`/`namespace`/`end` frames and block-comment state, and
collects every still-in-scope `variable` declaration (including multi-line
ones, kept by absorbing indented continuation lines). A
`variableShadowedByTheorem` filter drops a `variable` whose named binders
are all already explicit binders on the theorem, so existing
`@[eval_problem]`s that inline binders (Gleason, etc.) do not pick up a
redundant `variable` line that would trigger the unused-variable linter.
Includes a regression sandbox problem `variable_binder_example` whose
theorem refers to a variable-introduced `n`, plus a closed `section` and
a docstring mention of `variable` to exercise the scoping and
block-comment handling.
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 makes the extractor re-emit
variabledeclarations in generated single-hole workspaces so a theorem that inherits binders from a precedingvariable {n : Type*} [Fintype n] [DecidableEq n]declaration still type-checks underautoImplicit = false.Closes #276.
The new
extractContextVariableswalks the source up to the theorem, trackingsection/namespace/endframes and block-comment state, and collects every still-in-scopevariabledeclaration (multi-line variables are kept by absorbing indented continuation lines). AvariableShadowedByTheoremfilter drops avariablewhose named binders are all already explicit on the theorem, so existing@[eval_problem]s that inline binders (Gleason, etc.) do not pick up a redundantvariableline that would trigger Lean's unused-variable linter.There is a sandbox regression problem
variable_binder_examplewhose theorem refers to a variable-introducedn, plus a closedsectionand a docstring mention ofvariableto exercise the scoping and block-comment handling.🤖 Prepared with Claude Code