fix: make theorem workspace generation robust to source context - #509
Merged
Conversation
The elaborated parameter list continues past the signature into the statement's own binders, so `bvp_comparison` delegated with the `x` bound by `∀ x ∈ Set.Icc 0 1` and `Solution.lean` failed to compile. Count the leading lambdas of the elaborated value instead — a hole's body is a `sorry`, so there is one per signature binder — and reconcile that list with the source signature and the re-emitted `variable` commands before using it, failing rather than under-applying when the two views cannot be lined up. Carry `include` and `omit` into the generated files too, since they decide which of those binders the declaration takes. Fix two further regressions in the same reconstruction. A statement can open a tactic block of its own (`substInv_X_sub_X_sq_eq_catalan`), so take the body marker to be the candidate whose body is a `sorry` running to the end of the declaration, and refuse to guess when there is no such candidate and more than one tactic block. And a `set_option … in` prefixing a removed declaration sits outside its `.ilean` range (`honeycomb_connective_constant`), so extend removals back over such prefixes, bounded by the end of the previous declaration. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CGyHZAhLAv6PVnV9vsqbxd
`by intro x; sorry` also elaborates to a lambda over `sorryAx`, so counting lambdas separates the signature from the statement only when the source body is a bare `sorry`. Decide that from the source text, which the body-marker scan already establishes, and report the parameters as `none` rather than `#[]` when the extractor cannot read them, so a declaration that takes no explicit parameters is distinguishable from one we know nothing about. Reject every disagreement between the elaborated parameters and the source signature instead of quietly replaying the source binders: the disagreement is itself evidence that one of the two is wrong, and delegating on either emits a workspace that does not compile. With no parameters reported and a `variable` in scope, fail for the same reason. Track block comments when walking back over `set_option … in` prefixes, so a comment between the prefix and its declaration no longer strands the prefix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CGyHZAhLAv6PVnV9vsqbxd
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 theorem workspace generation robust to the shape of the source declaration, so a problem module can use the constructs that Total variation estimate for hyperbolic systems does without the generated workspace coming out wrong.
Accept direct
:= sorrybodies and bodies with trivia between:=andby, and ignore body-like text in comments and strings. The body marker is the candidate whose body is asorryrunning to the end of the declaration, so a statement that opens a tactic block of its own (substInv_X_sub_X_sq_eq_catalancontains a top-levelhaveI … := by …) is not mistaken for the body.Preserve scoped
notation,syntaxandmacrocommands, and keep the precise inter-declaration context that trusted helpers need:ChallengeDeps.leandeletes only a declaration's own.ileanrange rather than everything up to the next declaration, so an interveningvariableorlocal notationsurvives. Removals still extend back overset_option … inand similar prefixes, which sit outside the range they scope onto.Pass outer
variableparameters through the generatedSolutiondelegation. Which of them Lean retained is read off the elaborated declaration: a hole's body is asorry, so its value carries exactly one lambda per signature binder, and counting those separates the signature from binders belonging to the statement. The result is reconciled with the source signature and the re-emittedvariablecommands before use, and generation fails rather than emit a delegation that under-applies.includeandomitare carried through as well, since they decide which of those binders the declaration takes.Validation:
lake exe test_generate(49 passed);lake exe lean-eval generatereproducesmain's tree apart from blank lines in 20ChallengeDeps.leanfiles, all of which typecheck; and thehyperbolic_viscosityworkspace from #499 generates and builds.🤖 Prepared with Claude Code