From d94298632c622e79fd4ddc4709f2773346b4b339 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 6 Aug 2026 03:33:40 +0000 Subject: [PATCH 1/4] fix: make theorem workspace generation robust to source context --- EvalTools/Generate.lean | 157 ++++++++++++++++++-- tests/lean/EvalToolsTests/GenerateTest.lean | 55 +++++++ 2 files changed, 196 insertions(+), 16 deletions(-) diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index d7c2bc1a..069d19d9 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -605,21 +605,86 @@ def Source.findTheoremHeader (s : Source) (start : Nat) (name : String) : Option i := i + 1 return none +/-- Skip whitespace and Lean comments from `start`. Block comments are nested. -/ +def Source.skipTrivia (s : Source) (start : Nat) : Nat := Id.run do + let mut i := start + while i < s.size do + if s[i]!.isWhitespace then + i := i + 1 + else if Source.startsWithAt s i "--".toList then + while i < s.size && s[i]! != '\n' do + i := i + 1 + else if Source.startsWithAt s i "/-".toList then + i := blockCommentEnd s i + else + break + return i + +/-- Skip a double-quoted string, including escaped characters. `start` must +point at the opening quote. -/ +private def Source.stringLiteralEnd (s : Source) (start : Nat) : Nat := Id.run do + let mut i := start + 1 + while i < s.size do + if s[i]! == '\\' then + i := min (i + 2) s.size + else if s[i]! == '"' then + return i + 1 + else + i := i + 1 + return s.size + +/-- Locate the body marker of an eval-problem theorem without assuming the +literal spelling `:= by`. Candidates inside comments and strings are ignored; +arbitrary trivia may follow `:=`; and both the usual `by ... sorry` body and a +direct `sorry` body are accepted. + +A direct `sorry` candidate is only accepted when it is the complete remaining +body. For `by` bodies we retain the previous last-candidate behavior, while +making its whitespace and comment handling lexical rather than literal. -/ +def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.run do + let mut i := start + let mut byMarker : Option Nat := none + let mut directSorryMarker : Option Nat := none + while i < s.size do + if Source.startsWithAt s i "--".toList then + while i < s.size && s[i]! != '\n' do + i := i + 1 + else if Source.startsWithAt s i "/-".toList then + i := blockCommentEnd s i + else if s[i]! == '"' then + i := Source.stringLiteralEnd s i + else if Source.startsWithAt s i ":=".toList then + let bodyStart := Source.skipTrivia s (i + 2) + if Source.startsWithAt s bodyStart "sorry".toList + && Source.atWordEnd s (bodyStart + "sorry".length) + && Source.skipTrivia s (bodyStart + "sorry".length) == s.size then + directSorryMarker := some i + else if Source.startsWithAt s bodyStart "by".toList + && Source.atWordEnd s (bodyStart + "by".length) then + byMarker := some i + i := i + 2 + else + i := i + 1 + return match directSorryMarker with + | some marker => some marker + | none => byMarker + /-- Extract the theorem statement text from a sliced declaration body. -Mirrors `extract_statement_text`. -/ +The body marker is found lexically so direct `:= sorry` holes and flexible +whitespace/comment formatting are supported. -/ def extractStatementText (problemId : String) (sourcePath : System.FilePath) (declarationText theoremName : String) : IO String := do let src := Source.ofString declarationText let some headerEnd := Source.findTheoremHeader src 0 theoremName | throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - let some byPos := Source.rfind src src.size ":= by".toList + let some bodyPos := Source.findTheoremBodyMarker src headerEnd | throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - if byPos < headerEnd then + if bodyPos < headerEnd then throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - return (Source.slice src headerEnd byPos).trimAscii.toString + return (Source.slice src headerEnd bodyPos).trimAscii.toString /-- Parse leading binders off a theorem-statement string. Returns pairs of `(opener, body)` for each leading `(...)`, `{...}`, or `[...]` group. -/ @@ -961,12 +1026,28 @@ private def variableShadowedByTheorem (varText : String) if !theoremBinderNames.contains name then return false return true +/-- Syntax declarations are source context, not mathematical helpers, but +extracted statements and kept declarations may depend on their notation. -/ +private def isSyntaxContextDeclaration (declarationText : String) : Bool := Id.run do + let text := declarationText.trimAsciiStart.toString + let prefixes := #[ + "notation", "local notation", "scoped notation", + "infix", "infixl", "infixr", "prefix", "postfix", + "local infix", "local infixl", "local infixr", "local prefix", "local postfix", + "scoped infix", "scoped infixl", "scoped infixr", "scoped prefix", "scoped postfix", + "syntax", "local syntax", "scoped syntax", "macro", "macro_rules" + ] + for kw in prefixes do + if startsWithKeyword text kw then return true + return false + /-- Top-level command keywords that begin a fresh declaration/command. A whitespace-indented line opening with one of these is never a continuation of a preceding `variable`/`universe` block (Lean permits indented top-level commands), so the block scanner must stop before absorbing it. -/ private def startsWithCommandKeyword (stripped : String) : Bool := Id.run do if stripped.startsWith "@[" then return true + if isSyntaxContextDeclaration stripped then return true let kws := #["def", "theorem", "lemma", "instance", "abbrev", "opaque", "axiom", "class", "structure", "inductive", "namespace", "section", "end", "variable", "universe", "open", "example", "noncomputable", "private", @@ -982,8 +1063,9 @@ goes out of scope at the matching `end`. Multi-line blocks absorb following whitespace-indented continuation lines. Each collected block is filtered through `keep`; only blocks for which `keep` returns true are emitted. Returns the kept blocks joined by newlines with a trailing blank line, or `""` if none. -/ -def extractScopedCommandBlocks (source : String) (extracted? : Option ExtractedTheorem) - (keyword : String) (keep : String → Bool) : String := Id.run do +private def extractScopedCommandBlocksWhere (source : String) + (extracted? : Option ExtractedTheorem) (isMatch : String → Bool) + (keep : String → Bool) : String := Id.run do let lines := source.splitOn "\n" let targetLine? : Option Nat := extracted?.map fun e => e.startLine let mut layers : Array (Array String) := #[#[]] @@ -1036,7 +1118,7 @@ def extractScopedCommandBlocks (source : String) (extracted? : Option ExtractedT frameDepth := frameDepth - 1 layers := layers.pop idx := idx + 1 - else if startsWithKeyword stripped keyword then + else if isMatch stripped then let mut block := line idx := idx + 1 while idx < lines.length do @@ -1062,6 +1144,11 @@ def extractScopedCommandBlocks (source : String) (extracted? : Option ExtractedT if flat.isEmpty then return "" return "\n".intercalate flat.toList ++ "\n\n" +def extractScopedCommandBlocks (source : String) (extracted? : Option ExtractedTheorem) + (keyword : String) (keep : String → Bool) : String := + extractScopedCommandBlocksWhere source extracted? + (fun stripped => startsWithKeyword stripped keyword) keep + def extractContextVariables (source : String) (extracted? : Option ExtractedTheorem) (theoremBinderNames : Array String) : String := -- One layer per `section`/`namespace` we are still inside, matching Lean's @@ -1070,6 +1157,27 @@ def extractContextVariables (source : String) (extracted? : Option ExtractedTheo extractScopedCommandBlocks source extracted? "variable" (fun block => !variableShadowedByTheorem block theoremBinderNames) +/-- Explicit arguments introduced by the emitted `variable` context. These +parameters precede the theorem's own binders in the generated declaration and +must also be supplied when `Solution` delegates to `Submission`. -/ +def contextVariableApplicationArgs (contextVariables : String) : Array String := Id.run do + let mut args : Array String := #[] + let mut current := "" + for line in contextVariables.splitOn "\n" do + let stripped := line.trimAsciiStart.toString + if startsWithKeyword stripped "variable" then + if !current.isEmpty then + args := args ++ explicitBinderApplicationArgs current + current := (stripped.drop "variable".length).toString + else if !current.isEmpty && isLineStartingWithWhitespace line then + current := current ++ "\n" ++ line + else if !current.isEmpty then + args := args ++ explicitBinderApplicationArgs current + current := "" + if !current.isEmpty then + args := args ++ explicitBinderApplicationArgs current + return args + /-- Collect top-level `universe` commands in scope at the theorem. A source module may declare `universe u v` and refer to `u`/`v` in a theorem whose reconstructed `Challenge.lean` slice (`theorem … := by sorry`) would otherwise @@ -1078,6 +1186,13 @@ in-scope `universe` commands restores them. -/ def extractContextUniverses (source : String) (extracted? : Option ExtractedTheorem) : String := extractScopedCommandBlocks source extracted? "universe" (fun _ => true) +/-- Collect notation, syntax, and macro commands still in scope at the target +declaration. Generated statements retain their source notation, so these +commands must accompany them just like scoped variables and universes do. -/ +def extractContextSyntaxDeclarations (source : String) + (extracted? : Option ExtractedTheorem) : String := + extractScopedCommandBlocksWhere source extracted? isSyntaxContextDeclaration (fun _ => true) + /-! ## Render ChallengeDeps.lean -/ /-- The byte range `[start, stop)` of a single source declaration in `sourceText`, @@ -1128,7 +1243,6 @@ def applyEdits (sourceText : String) (edits : Array (Nat × Nat × String)) : St result := Source.slice src 0 start ++ replacement ++ Source.slice src stop src.size return result - /-- Shared core of single- and multi-hole `ChallengeDeps.lean` rendering. * `keepDeclarations` are the names whose source text we want to *retain* @@ -1160,9 +1274,14 @@ def renderChallengeDepsCore (root : System.FilePath) (entry : EvalProblemMetadat let mut removeRangesRaw : Array (Nat × Nat) := #[] for span in spans do if keepDeclarations.contains span.name then continue + let declarationText := Source.slice sourceSrc span.start span.declEnd + if isSyntaxContextDeclaration declarationText then continue match protectedRanges[span.name]? with | some (s, e) => removeRangesRaw := removeRangesRaw.push (s, e) - | none => removeRangesRaw := removeRangesRaw.push (span.start, span.stop) + -- Delete only the declaration's precise `.ilean` range. Extending to the + -- next declaration also deletes intervening scoped context commands such + -- as `variable` and `local notation`, which kept helpers may require. + | none => removeRangesRaw := removeRangesRaw.push (span.start, span.declEnd) let removeRanges := removeRangesRaw.qsort (fun a b => a.1 < b.1 || (a.1 == b.1 && a.2 < b.2)) let mut pieces : Array String := #[] @@ -1617,10 +1736,6 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb let endOff ← src.offsetForLineColumn extracted.endLine extracted.endColumn let declText := Source.slice src startOff endOff let theoremStatement ← extractStatementText entry.id sourcePath declText theoremName - let solutionArgs := explicitBinderApplicationArgs theoremStatement - let solutionExact := - if solutionArgs.isEmpty then s!"Submission.{theoremName}" - else s!"Submission.{theoremName} " ++ " ".intercalate solutionArgs.toList let localImports ← repoLocalImportModules root entry.moduleName let challengeDeps? ← renderChallengeDeps root entry extracted localImports let hasChallengeDeps := challengeDeps?.isSome @@ -1635,8 +1750,15 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb let theoremBinderNames := binderIntroducedNames theoremStatement let contextUniverseBlock := extractContextUniverses sourceText (some extracted) + let contextSyntaxBlock := + extractContextSyntaxDeclarations sourceText (some extracted) let contextVariablesBlock := extractContextVariables sourceText (some extracted) theoremBinderNames + let solutionArgs := contextVariableApplicationArgs contextVariablesBlock ++ + explicitBinderApplicationArgs theoremStatement + let solutionExact := + if solutionArgs.isEmpty then s!"Submission.{theoremName}" + else s!"Submission.{theoremName} " ++ " ".intercalate solutionArgs.toList let includeNamespaces := hasChallengeDeps || !localImports.isEmpty let contextOpenBlock ← extractContextOpens entry.id sourcePath sourceText (some extracted) includeNamespaces @@ -1655,13 +1777,16 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb let readmeLines := renderReadmeLines entry #[extracted] (multiHole := false) let readme := "\n".intercalate readmeLines.toList ++ "\n" let challengeFile := - challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ contextVariablesBlock ++ + challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + contextVariablesBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n" let solutionFile := - solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextVariablesBlock ++ + solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + contextVariablesBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n exact {solutionExact}\n" let submissionFile := - submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextVariablesBlock ++ + submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + contextVariablesBlock ++ "namespace Submission\n\n" ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n\n" ++ "end Submission\n" diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 9e1b61cc..8f0a66ed 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -24,6 +24,61 @@ def main : IO UInt32 := do let passes ← IO.mkRef 0 let fails ← IO.mkRef 0 + check "extractStatementText accepts a direct sorry body" passes fails do + let declaration := + "theorem target (n : Nat) :\n" ++ + " ∃ m, n ≤ m :=\n" ++ + " sorry" + let actual ← extractStatementText "direct-sorry" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual "(n : Nat) :\n ∃ m, n ≤ m" + + check "extractStatementText accepts trivia before by" passes fails do + let declaration := + "theorem target : True := /- proof starts here -/\n" ++ + " by\n" ++ + " sorry" + let actual ← extractStatementText "trivia-before-by" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual ": True" + + check "extractStatementText ignores body-like text in the statement" passes fails do + let declaration := + "theorem target :\n" ++ + " let marker := \"fake := by and := sorry\"\n" ++ + " marker.length = 24 :=\n" ++ + " sorry" + let actual ← extractStatementText "body-like-text" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual + ":\n let marker := \"fake := by and := sorry\"\n marker.length = 24" + + check "extractContextSyntaxDeclarations respects scope" passes fails do + let source := + "section\n" ++ + "local notation \"closed\" => Nat\n" ++ + "end\n" ++ + "namespace Demo\n" ++ + "local notation:arg \"ℝ^\" n:arg => EuclideanSpace ℝ (Fin n)\n" ++ + "theorem target : True := by sorry\n" ++ + "end Demo\n" + let extracted : ExtractedTheorem := { + declarationName := "Demo.target" + module := "Demo" + startLine := 6, startColumn := 0 + endLine := 6, endColumn := 32 + sameModuleDependencies := #[] + kind := "theorem" + } + let context := extractContextSyntaxDeclarations source (some extracted) + pure <| assertEq "active notation kept" ((context.find? "local notation:arg").isSome) true + |>.or (assertEq "closed notation dropped" ((context.find? "closed").isSome) false) + + check "contextVariableApplicationArgs keeps only explicit binders" passes fails do + let context := + "variable {α : Type*} (n : Nat)\n" ++ + " (f : α → α)\n" ++ + "variable [DecidableEq α] (x y : α)\n\n" + pure <| assertEq "arguments" + (contextVariableApplicationArgs context) #["n", "f", "x", "y"] + -- Regression for https://github.com/leanprover/lean-eval/pull/467: -- Mathlib-style copyright headers precede imports. The generator must drop -- both the header and imports before copying trusted helpers into From 6936c3bcaedb5aefa41ac0e4475bda3df3834553 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 6 Aug 2026 04:53:01 +0000 Subject: [PATCH 2/4] fix: derive delegation arguments from elaborated declarations --- EvalTools/ExtractTheorem.lean | 11 ++ EvalTools/Generate.lean | 116 +++++++++++++------- tests/lean/EvalToolsTests/GenerateTest.lean | 21 ++-- 3 files changed, 102 insertions(+), 46 deletions(-) diff --git a/EvalTools/ExtractTheorem.lean b/EvalTools/ExtractTheorem.lean index b289f18f..7add5f75 100644 --- a/EvalTools/ExtractTheorem.lean +++ b/EvalTools/ExtractTheorem.lean @@ -14,6 +14,10 @@ structure ExtractedTheorem where declarationName : String module : String sourceRange : SourceRange + /-- Names of the explicit parameters in the elaborated declaration type, in + application order. This includes source-level `variable` parameters exactly + when Lean actually retained them in the declaration. -/ + explicitParameters : Array String /-- Names of declarations from the same module that appear (transitively) in the type or value of this theorem. Computed from the elaborated terms, so this captures uses introduced by typeclass synthesis (which the `.ilean` references metadata @@ -25,6 +29,12 @@ structure ExtractedTheorem where kind : String deriving ToJson +def explicitParameterNames : Expr → Array String + | .forallE name _ body binderInfo => + let rest := explicitParameterNames body + if binderInfo == .default && !name.isAnonymous then #[name.toString] ++ rest else rest + | _ => #[] + def parseName (text : String) : Name := text.splitOn "." |>.foldl Name.str .anonymous @@ -180,6 +190,7 @@ def extractTheorem (moduleNameText declNameText : String) : IO ExtractedTheorem declarationName := toString resolvedDeclName module := moduleNameText sourceRange := sourceRange + explicitParameters := explicitParameterNames constantInfo.type sameModuleDependencies := deps.map toString kind := kind } diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index 069d19d9..7a1a63df 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -115,6 +115,7 @@ structure ExtractedTheorem where startColumn : Nat endLine : Nat endColumn : Nat + explicitParameters : Option (Array String) := none sameModuleDependencies : Array String kind : String deriving Inhabited @@ -129,6 +130,14 @@ private def parseExtractedTheorem (payload : String) : Except String ExtractedTh let startColumn ← range.getObjValAs? Nat "startColumn" let endLine ← range.getObjValAs? Nat "endLine" let endColumn ← range.getObjValAs? Nat "endColumn" + let explicitParameters ← match json.getObjVal? "explicitParameters" with + | .error _ => pure none + | .ok paramsJson => do + let paramsJson ← paramsJson.getArr? + let mut params : Array String := #[] + for paramJson in paramsJson do + params := params.push (← paramJson.getStr?) + pure (some params) let depNames : Array String ← match json.getObjVal? "sameModuleDependencies" with | .error _ => pure #[] @@ -140,7 +149,7 @@ private def parseExtractedTheorem (payload : String) : Except String ExtractedTh acc := acc.push s pure acc return { - declarationName, module, startLine, startColumn, endLine, endColumn + declarationName, module, startLine, startColumn, endLine, endColumn, explicitParameters sameModuleDependencies := depNames kind } @@ -633,18 +642,36 @@ private def Source.stringLiteralEnd (s : Source) (start : Nat) : Nat := Id.run d i := i + 1 return s.size +/-- If `start` begins a character literal, return its end. Apostrophes used in +identifiers are rejected by requiring a closing quote in the literal shape. -/ +private def Source.charLiteralEnd? (s : Source) (start : Nat) : Option Nat := + if start + 2 < s.size && s[start + 2]! == '\'' then some (start + 3) + else if start + 3 < s.size && s[start + 1]! == '\\' && s[start + 3]! == '\'' then + some (start + 4) + else none + +/-- Skip a French-quoted identifier such as `«a := by»`. -/ +private def Source.quotedIdentifierEnd (s : Source) (start : Nat) : Nat := Id.run do + let mut i := start + 1 + while i < s.size do + if s[i]! == '»' then return i + 1 + i := i + 1 + return s.size + /-- Locate the body marker of an eval-problem theorem without assuming the literal spelling `:= by`. Candidates inside comments and strings are ignored; arbitrary trivia may follow `:=`; and both the usual `by ... sorry` body and a direct `sorry` body are accepted. A direct `sorry` candidate is only accepted when it is the complete remaining -body. For `by` bodies we retain the previous last-candidate behavior, while -making its whitespace and comment handling lexical rather than literal. -/ +body. Only top-level markers are considered, so default binder values and +nested proof assignments cannot be mistaken for the declaration body. -/ def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.run do let mut i := start - let mut byMarker : Option Nat := none - let mut directSorryMarker : Option Nat := none + let mut roundDepth := 0 + let mut squareDepth := 0 + let mut braceDepth := 0 + let mut angleDepth := 0 while i < s.size do if Source.startsWithAt s i "--".toList then while i < s.size && s[i]! != '\n' do @@ -653,21 +680,34 @@ def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.r i := blockCommentEnd s i else if s[i]! == '"' then i := Source.stringLiteralEnd s i - else if Source.startsWithAt s i ":=".toList then + else if s[i]! == '\'' then + match Source.charLiteralEnd? s i with + | some literalEnd => i := literalEnd + | none => i := i + 1 + else if s[i]! == '«' then + i := Source.quotedIdentifierEnd s i + else if s[i]! == '(' then roundDepth := roundDepth + 1; i := i + 1 + else if s[i]! == ')' then roundDepth := roundDepth - 1; i := i + 1 + else if s[i]! == '[' then squareDepth := squareDepth + 1; i := i + 1 + else if s[i]! == ']' then squareDepth := squareDepth - 1; i := i + 1 + else if s[i]! == '{' then braceDepth := braceDepth + 1; i := i + 1 + else if s[i]! == '}' then braceDepth := braceDepth - 1; i := i + 1 + else if s[i]! == '⟨' then angleDepth := angleDepth + 1; i := i + 1 + else if s[i]! == '⟩' then angleDepth := angleDepth - 1; i := i + 1 + else if roundDepth == 0 && squareDepth == 0 && braceDepth == 0 && angleDepth == 0 + && Source.startsWithAt s i ":=".toList then let bodyStart := Source.skipTrivia s (i + 2) if Source.startsWithAt s bodyStart "sorry".toList && Source.atWordEnd s (bodyStart + "sorry".length) && Source.skipTrivia s (bodyStart + "sorry".length) == s.size then - directSorryMarker := some i + return some i else if Source.startsWithAt s bodyStart "by".toList && Source.atWordEnd s (bodyStart + "by".length) then - byMarker := some i + return some i i := i + 2 else i := i + 1 - return match directSorryMarker with - | some marker => some marker - | none => byMarker + return none /-- Extract the theorem statement text from a sliced declaration body. The body marker is found lexically so direct `:= sorry` holes and flexible @@ -1041,6 +1081,16 @@ private def isSyntaxContextDeclaration (declarationText : String) : Bool := Id.r if startsWithKeyword text kw then return true return false +private def isLocalSyntaxContextDeclaration (declarationText : String) : Bool := Id.run do + let text := declarationText.trimAsciiStart.toString + let prefixes := #[ + "local notation", "local infix", "local infixl", "local infixr", + "local prefix", "local postfix", "local syntax" + ] + for kw in prefixes do + if startsWithKeyword text kw then return true + return false + /-- Top-level command keywords that begin a fresh declaration/command. A whitespace-indented line opening with one of these is never a continuation of a preceding `variable`/`universe` block (Lean permits indented top-level @@ -1157,27 +1207,6 @@ def extractContextVariables (source : String) (extracted? : Option ExtractedTheo extractScopedCommandBlocks source extracted? "variable" (fun block => !variableShadowedByTheorem block theoremBinderNames) -/-- Explicit arguments introduced by the emitted `variable` context. These -parameters precede the theorem's own binders in the generated declaration and -must also be supplied when `Solution` delegates to `Submission`. -/ -def contextVariableApplicationArgs (contextVariables : String) : Array String := Id.run do - let mut args : Array String := #[] - let mut current := "" - for line in contextVariables.splitOn "\n" do - let stripped := line.trimAsciiStart.toString - if startsWithKeyword stripped "variable" then - if !current.isEmpty then - args := args ++ explicitBinderApplicationArgs current - current := (stripped.drop "variable".length).toString - else if !current.isEmpty && isLineStartingWithWhitespace line then - current := current ++ "\n" ++ line - else if !current.isEmpty then - args := args ++ explicitBinderApplicationArgs current - current := "" - if !current.isEmpty then - args := args ++ explicitBinderApplicationArgs current - return args - /-- Collect top-level `universe` commands in scope at the theorem. A source module may declare `universe u v` and refer to `u`/`v` in a theorem whose reconstructed `Challenge.lean` slice (`theorem … := by sorry`) would otherwise @@ -1193,6 +1222,10 @@ def extractContextSyntaxDeclarations (source : String) (extracted? : Option ExtractedTheorem) : String := extractScopedCommandBlocksWhere source extracted? isSyntaxContextDeclaration (fun _ => true) +def extractContextLocalSyntaxDeclarations (source : String) + (extracted? : Option ExtractedTheorem) : String := + extractScopedCommandBlocksWhere source extracted? isLocalSyntaxContextDeclaration (fun _ => true) + /-! ## Render ChallengeDeps.lean -/ /-- The byte range `[start, stop)` of a single source declaration in `sourceText`, @@ -1656,7 +1689,10 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl let some lastEq := Source.rfind betweenSrc betweenSrc.size ":=".toList | throw <| IO.userError s!"Source decl for hole '{fullName}' has no `:=` body marker." let statement := Source.slice betweenSrc 0 lastEq - let explicitArgs := explicitBinderApplicationArgs statement + let explicitArgs := match extracteds.find? (fun e => e.declarationName == fullName) with + | some extracted => extracted.explicitParameters.getD + (explicitBinderApplicationArgs statement) + | none => explicitBinderApplicationArgs statement let applied := if explicitArgs.isEmpty then s!"Submission.{fullName}" else s!"Submission.{fullName} " ++ " ".intercalate explicitArgs.toList @@ -1752,10 +1788,12 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb extractContextUniverses sourceText (some extracted) let contextSyntaxBlock := extractContextSyntaxDeclarations sourceText (some extracted) + let contextLocalSyntaxBlock := + extractContextLocalSyntaxDeclarations sourceText (some extracted) let contextVariablesBlock := extractContextVariables sourceText (some extracted) theoremBinderNames - let solutionArgs := contextVariableApplicationArgs contextVariablesBlock ++ - explicitBinderApplicationArgs theoremStatement + let solutionArgs := extracted.explicitParameters.getD + (explicitBinderApplicationArgs theoremStatement) let solutionExact := if solutionArgs.isEmpty then s!"Submission.{theoremName}" else s!"Submission.{theoremName} " ++ " ".intercalate solutionArgs.toList @@ -1777,15 +1815,17 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb let readmeLines := renderReadmeLines entry #[extracted] (multiHole := false) let readme := "\n".intercalate readmeLines.toList ++ "\n" let challengeFile := - challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ + (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ contextVariablesBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n" let solutionFile := - solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextLocalSyntaxBlock ++ contextVariablesBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n exact {solutionExact}\n" let submissionFile := - submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextSyntaxBlock ++ + submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ + (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ contextVariablesBlock ++ "namespace Submission\n\n" ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n\n" ++ diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 8f0a66ed..9c59c6bd 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -50,6 +50,19 @@ def main : IO UInt32 := do pure <| assertEq "statement" actual ":\n let marker := \"fake := by and := sorry\"\n marker.length = 24" + check "extractStatementText ignores nested proof assignments" passes fails do + let declaration := + "theorem target (h : True := by trivial) : True := by\n" ++ + " have nested : True := sorry" + let actual ← extractStatementText "nested-assignment" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual "(h : True := by trivial) : True" + + check "extractStatementText handles quote characters" passes fails do + let declaration := + "theorem target : ('\"' : Char) = '\"' := by sorry" + let actual ← extractStatementText "char-literal" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual ": ('\"' : Char) = '\"'" + check "extractContextSyntaxDeclarations respects scope" passes fails do let source := "section\n" ++ @@ -71,14 +84,6 @@ def main : IO UInt32 := do pure <| assertEq "active notation kept" ((context.find? "local notation:arg").isSome) true |>.or (assertEq "closed notation dropped" ((context.find? "closed").isSome) false) - check "contextVariableApplicationArgs keeps only explicit binders" passes fails do - let context := - "variable {α : Type*} (n : Nat)\n" ++ - " (f : α → α)\n" ++ - "variable [DecidableEq α] (x y : α)\n\n" - pure <| assertEq "arguments" - (contextVariableApplicationArgs context) #["n", "f", "x", "y"] - -- Regression for https://github.com/leanprover/lean-eval/pull/467: -- Mathlib-style copyright headers precede imports. The generator must drop -- both the header and imports before copying trusted helpers into From 635ecc338683bce1bc63a26207a9a0d147a8d4b2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 9 Aug 2026 11:17:47 +0000 Subject: [PATCH 3/4] fix: derive delegation arguments from the declaration's signature only MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) Claude-Session: https://claude.ai/code/session_01CGyHZAhLAv6PVnV9vsqbxd --- EvalTools/ExtractTheorem.lean | 48 +++- EvalTools/Generate.lean | 229 +++++++++++++++++--- tests/lean/EvalToolsTests/GenerateTest.lean | 139 +++++++++++- 3 files changed, 374 insertions(+), 42 deletions(-) diff --git a/EvalTools/ExtractTheorem.lean b/EvalTools/ExtractTheorem.lean index 7add5f75..70d3b901 100644 --- a/EvalTools/ExtractTheorem.lean +++ b/EvalTools/ExtractTheorem.lean @@ -14,9 +14,11 @@ structure ExtractedTheorem where declarationName : String module : String sourceRange : SourceRange - /-- Names of the explicit parameters in the elaborated declaration type, in - application order. This includes source-level `variable` parameters exactly - when Lean actually retained them in the declaration. -/ + /-- Names of the explicit parameters bound by the declaration's *signature*, + in application order. This includes source-level `variable` parameters + exactly when Lean actually retained them in the declaration, and excludes + binders that belong to the statement itself (a leading `∀` in the + conclusion), which the generated delegation must not apply. -/ explicitParameters : Array String /-- Names of declarations from the same module that appear (transitively) in the type or value of this theorem. Computed from the elaborated terms, so this captures @@ -29,11 +31,39 @@ structure ExtractedTheorem where kind : String deriving ToJson -def explicitParameterNames : Expr → Array String - | .forallE name _ body binderInfo => - let rest := explicitParameterNames body - if binderInfo == .default && !name.isAnonymous then #[name.toString] ++ rest else rest - | _ => #[] +/-- The number of leading `fun` binders of `value`, if what they wrap is a bare +`sorry`; `none` for any other body. -/ +def sorryBodyArity : Expr → Option Nat + | .lam _ _ body _ => (sorryBodyArity body).map (· + 1) + | e => if e.isSorry then some 0 else none + +/-- Names of the explicit parameters bound by the declaration's signature, in +application order, or `#[]` when they cannot be determined. + +An eval-problem hole has a bare `sorry` body, so its elaborated value is one +`fun` binder per signature binder — the declaration's own binders together with +the `variable` binders Lean retained — wrapped around `sorryAx`. Counting those +lambdas separates the signature from the statement: a conclusion that starts +with `∀` contributes `forallE` binders to the type but no lambda to the value, +and applying those in the generated delegation would be wrong. + +The `sorry` body is what makes the count meaningful, so it is checked rather +than assumed: a tactic proof can introduce conclusion binders of its own, and +its lambdas say nothing about the signature. -/ +def signatureExplicitParameters (info : ConstantInfo) : Array String := Id.run do + let some arity := info.value? (allowOpaque := true) >>= sorryBodyArity | return #[] + let mut remaining := arity + let mut type := info.type + let mut names : Array String := #[] + while remaining > 0 do + match type with + | .forallE name _ body binderInfo => + if binderInfo == .default && !name.isAnonymous then + names := names.push name.toString + type := body + remaining := remaining - 1 + | _ => remaining := 0 + return names def parseName (text : String) : Name := text.splitOn "." |>.foldl Name.str .anonymous @@ -190,7 +220,7 @@ def extractTheorem (moduleNameText declNameText : String) : IO ExtractedTheorem declarationName := toString resolvedDeclName module := moduleNameText sourceRange := sourceRange - explicitParameters := explicitParameterNames constantInfo.type + explicitParameters := signatureExplicitParameters constantInfo sameModuleDependencies := deps.map toString kind := kind } diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index 7a1a63df..8c2c36dc 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -659,19 +659,30 @@ private def Source.quotedIdentifierEnd (s : Source) (start : Nat) : Nat := Id.ru return s.size /-- Locate the body marker of an eval-problem theorem without assuming the -literal spelling `:= by`. Candidates inside comments and strings are ignored; -arbitrary trivia may follow `:=`; and both the usual `by ... sorry` body and a -direct `sorry` body are accepted. - -A direct `sorry` candidate is only accepted when it is the complete remaining -body. Only top-level markers are considered, so default binder values and -nested proof assignments cannot be mistaken for the declaration body. -/ +literal spelling `:= by`. Candidates inside comments, strings, and brackets are +ignored, so a default binder value such as `(h : P := by tac)` cannot be +mistaken for the declaration body; arbitrary trivia may follow `:=`; and both +the usual `by sorry` body and a direct `sorry` body are accepted. + +An eval-problem hole's body is a `sorry`, so a candidate whose body is exactly +`sorry` (behind `by` or not) and runs to the end of the declaration wins over +every other candidate: a *statement* may itself contain a top-level +`haveI … := by …`, and that tactic block is not the body. + +Failing that — the `ci_regenerate_main_check` canary really is proved by +`trivial` — a candidate opening a tactic block is used, but only if it is the +only one. With a body that is not a `sorry` there is nothing left to tell an +assignment in the statement apart from an assignment in the proof, so `none` is +returned and the caller reports that it could not recover the statement. -/ def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.run do let mut i := start let mut roundDepth := 0 let mut squareDepth := 0 let mut braceDepth := 0 let mut angleDepth := 0 + let mut sorryMarker : Option Nat := none + let mut tacticMarker : Option Nat := none + let mut tacticMarkers := 0 while i < s.size do if Source.startsWithAt s i "--".toList then while i < s.size && s[i]! != '\n' do @@ -697,17 +708,23 @@ def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.r else if roundDepth == 0 && squareDepth == 0 && braceDepth == 0 && angleDepth == 0 && Source.startsWithAt s i ":=".toList then let bodyStart := Source.skipTrivia s (i + 2) - if Source.startsWithAt s bodyStart "sorry".toList - && Source.atWordEnd s (bodyStart + "sorry".length) - && Source.skipTrivia s (bodyStart + "sorry".length) == s.size then - return some i - else if Source.startsWithAt s bodyStart "by".toList - && Source.atWordEnd s (bodyStart + "by".length) then - return some i + let tacticBody := Source.startsWithAt s bodyStart "by".toList + && Source.atWordEnd s (bodyStart + "by".length) + let termStart := + if tacticBody then Source.skipTrivia s (bodyStart + "by".length) else bodyStart + if Source.startsWithAt s termStart "sorry".toList + && Source.atWordEnd s (termStart + "sorry".length) + && Source.skipTrivia s (termStart + "sorry".length) == s.size then + sorryMarker := some i + else if tacticBody then + tacticMarker := some i + tacticMarkers := tacticMarkers + 1 i := i + 2 else i := i + 1 - return none + return match sorryMarker with + | some marker => some marker + | none => if tacticMarkers == 1 then tacticMarker else none /-- Extract the theorem statement text from a sliced declaration body. The body marker is found lexically so direct `:= sorry` holes and flexible @@ -1215,6 +1232,16 @@ in-scope `universe` commands restores them. -/ def extractContextUniverses (source : String) (extracted? : Option ExtractedTheorem) : String := extractScopedCommandBlocks source extracted? "universe" (fun _ => true) +/-- Collect the `include` and `omit` commands in scope at the theorem. These +decide which of the surrounding `variable` binders the declaration actually +takes, so re-emitting the `variable` commands without them would give the +generated declaration a different signature from the source one — and the +delegation arguments derived from the source declaration would not fit. -/ +def extractContextIncludes (source : String) (extracted? : Option ExtractedTheorem) : String := + extractScopedCommandBlocksWhere source extracted? + (fun stripped => startsWithKeyword stripped "include" || startsWithKeyword stripped "omit") + (fun _ => true) + /-- Collect notation, syntax, and macro commands still in scope at the target declaration. Generated statements retain their source notation, so these commands must accompany them just like scoped variables and universes do. -/ @@ -1226,6 +1253,58 @@ def extractContextLocalSyntaxDeclarations (source : String) (extracted? : Option ExtractedTheorem) : String := extractScopedCommandBlocksWhere source extracted? isLocalSyntaxContextDeclaration (fun _ => true) +/-! ## Delegation arguments -/ + +/-- Explicit (parenthesised) binder names introduced by the `variable` commands +in `block`, the text produced by `extractContextVariables`. These are the outer +parameters the generated files re-declare ahead of the restated signature, so +they are the only names a delegation may legitimately apply beyond the +declaration's own binders. -/ +def variableBlockExplicitNames (block : String) : Array String := Id.run do + let mut names : Array String := #[] + let mut current : Option String := none + for line in block.splitOn "\n" do + let stripped := line.trimAsciiStart.toString + if startsWithKeyword stripped "variable" then + if let some command := current then + names := names ++ explicitBinderApplicationArgs command + current := some (stripped.drop "variable".length).toString + else if let some command := current then + current := some (command ++ "\n" ++ line) + if let some command := current then + names := names ++ explicitBinderApplicationArgs command + return names + +/-- The arguments the generated delegation must apply to `Submission.`. + +`sourceArgs` are the explicit binders parsed out of the declaration's own +source signature. A module may introduce further explicit parameters through +outer `variable` commands; Lean retains those in the elaborated declaration and +the generated files re-declare them, so they precede `sourceArgs` in +application order. `signatureParams?` is the extractor's report of the full +list. + +The extractor's list is only trusted when it agrees with what the source +shows: it must end with `sourceArgs`, and every name ahead of them must be +introduced by one of the re-emitted `variable` commands. + +When the two views disagree, `sourceArgs` alone is the right answer only if it +cannot be missing anything — that is, if the extractor reports no more explicit +parameters than the source signature accounts for. A longer report means there +are parameters we cannot place (an inaccessible binder name, say), and +delegating without them would under-apply; `none` is returned so the caller can +fail rather than emit a workspace that does not compile. -/ +def delegationArgs? (signatureParams? : Option (Array String)) + (variableNames sourceArgs : Array String) : Option (Array String) := Id.run do + let some params := signatureParams? | return some sourceArgs + if params.size ≥ sourceArgs.size then + let outerCount := params.size - sourceArgs.size + if params.extract outerCount params.size == sourceArgs + && (params.extract 0 outerCount).all (fun p => variableNames.contains p) then + return some params + if params.size > sourceArgs.size then return none + return some sourceArgs + /-! ## Render ChallengeDeps.lean -/ /-- The byte range `[start, stop)` of a single source declaration in `sourceText`, @@ -1276,6 +1355,77 @@ def applyEdits (sourceText : String) (edits : Array (Nat × Nat × String)) : St result := Source.slice src 0 start ++ replacement ++ Source.slice src stop src.size return result +/-- The tokens of `line` with comments removed. -/ +private def commandTokens (line : String) : Array String := + splitWhitespace (stripLineComment (stripSingleLineBlockComments line)) + +/-- Commands that can be written as ` … in ` to scope +themselves onto a single following declaration. -/ +private def scopingCommandKeywords : Array String := + #["set_option", "open", "attribute", "include", "omit", "local", "scoped"] + +/-- Move a removal range's start back over the command prefixes that scope onto +the declaration being removed — `set_option … in`, `open … in`, and friends. A +`.ilean` declaration range begins at the declaration proper, so such a prefix +is not covered by it and would otherwise be stranded with no command to apply +to. + +A prefix is recognised by its last token being `in`, and is then followed back +to the line opening the command, so prefixes spread over several lines are +consumed whole. Blank and comment-only lines are crossed, but are only dropped +if a prefix is found beyond them. `lowerBound` is the end of the previous +declaration; the search never crosses it, so text belonging to a declaration we +are keeping can never be consumed. -/ +def extendOverScopingPrefixes (source : Source) (lowerBound start : Nat) : Nat := Id.run do + -- Start of the line that position `i` sits on, clamped to `lowerBound`. + let lineStartAt : Nat → Nat := fun i => Id.run do + let mut lineStart := i + while lineStart > lowerBound && source[lineStart - 1]! != '\n' do + lineStart := lineStart - 1 + return lineStart + let lineEndAt : Nat → Nat := fun i => Id.run do + let mut lineEnd := i + while lineEnd < source.size && source[lineEnd]! != '\n' do + lineEnd := lineEnd + 1 + return lineEnd + let lastTokenIsIn : String → Bool := fun text => (commandTokens text).back? == some "in" + -- Walk back from the line holding a prefix's `in` to the line opening that + -- command, so a prefix spread over several lines is consumed whole. Stays + -- put if no opening line is found rather than guessing. + let commandStartAt : Nat → Nat := fun inLineStart => Id.run do + let mut lineStart := inLineStart + while true do + let opensCommand := scopingCommandKeywords.any fun keyword => + (commandTokens (Source.slice source lineStart (lineEndAt lineStart)))[0]? == some keyword + if opensCommand then return lineStart + if lineStart ≤ lowerBound then return inLineStart + lineStart := lineStartAt (lineStart - 1) + return inLineStart + let mut result := start + let mut cursor := start + while cursor > lowerBound do + let lineStart := lineStartAt cursor + if lastTokenIsIn (Source.slice source lineStart cursor) then + -- The prefix shares the declaration's line: `set_option … in theorem …`. + result := commandStartAt lineStart + cursor := result + else if lineStart ≤ lowerBound then + return result + else + let previousStart := lineStartAt (lineStart - 1) + let previous := Source.slice source previousStart (lineStart - 1) + let stripped := previous.trimAscii.toString + if stripped.isEmpty || stripped.startsWith "--" then + -- Trivia is crossed in the hope of a prefix beyond it, and only + -- dropped if one is found. + cursor := previousStart + else if lastTokenIsIn previous then + result := commandStartAt previousStart + cursor := result + else + return result + return result + /-- Shared core of single- and multi-hole `ChallengeDeps.lean` rendering. * `keepDeclarations` are the names whose source text we want to *retain* @@ -1305,16 +1455,21 @@ def renderChallengeDepsCore (root : System.FilePath) (entry : EvalProblemMetadat let bodyStart := importPreludeLength sourceSrc let spans ← loadDeclSpans root entry sourceSrc let mut removeRangesRaw : Array (Nat × Nat) := #[] + -- End of the last declaration we have walked past, so that a removal never + -- reaches back into the text of the declaration before it. + let mut previousEnd := bodyStart for span in spans do - if keepDeclarations.contains span.name then continue - let declarationText := Source.slice sourceSrc span.start span.declEnd - if isSyntaxContextDeclaration declarationText then continue - match protectedRanges[span.name]? with - | some (s, e) => removeRangesRaw := removeRangesRaw.push (s, e) -- Delete only the declaration's precise `.ilean` range. Extending to the -- next declaration also deletes intervening scoped context commands such -- as `variable` and `local notation`, which kept helpers may require. - | none => removeRangesRaw := removeRangesRaw.push (span.start, span.declEnd) + let (start, stop) := match protectedRanges[span.name]? with + | some (s, e) => (s, e) + | none => (span.start, span.declEnd) + let declarationText := Source.slice sourceSrc span.start span.declEnd + if !keepDeclarations.contains span.name && !isSyntaxContextDeclaration declarationText then + removeRangesRaw := removeRangesRaw.push + (extendOverScopingPrefixes sourceSrc previousEnd start, stop) + previousEnd := max previousEnd (max span.declEnd stop) let removeRanges := removeRangesRaw.qsort (fun a b => a.1 < b.1 || (a.1 == b.1 && a.2 < b.2)) let mut pieces : Array String := #[] @@ -1689,10 +1844,18 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl let some lastEq := Source.rfind betweenSrc betweenSrc.size ":=".toList | throw <| IO.userError s!"Source decl for hole '{fullName}' has no `:=` body marker." let statement := Source.slice betweenSrc 0 lastEq - let explicitArgs := match extracteds.find? (fun e => e.declarationName == fullName) with - | some extracted => extracted.explicitParameters.getD - (explicitBinderApplicationArgs statement) - | none => explicitBinderApplicationArgs statement + let sourceArgs := explicitBinderApplicationArgs statement + let explicitArgs ← match extracteds.find? (fun e => e.declarationName == fullName) with + | some extracted => + let variableNames := + variableBlockExplicitNames (extractContextVariables sourceText (some extracted) #[]) + match delegationArgs? extracted.explicitParameters variableNames sourceArgs with + | some args => pure args + | none => + throw <| IO.userError + s!"Could not match the elaborated parameters of hole '{fullName}' against its \ + source signature; the generated delegation would under-apply it." + | none => pure sourceArgs let applied := if explicitArgs.isEmpty then s!"Submission.{fullName}" else s!"Submission.{fullName} " ++ " ".intercalate explicitArgs.toList @@ -1792,8 +1955,14 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb extractContextLocalSyntaxDeclarations sourceText (some extracted) let contextVariablesBlock := extractContextVariables sourceText (some extracted) theoremBinderNames - let solutionArgs := extracted.explicitParameters.getD - (explicitBinderApplicationArgs theoremStatement) + let contextIncludeBlock := + extractContextIncludes sourceText (some extracted) + let some solutionArgs := delegationArgs? extracted.explicitParameters + (variableBlockExplicitNames contextVariablesBlock) + (explicitBinderApplicationArgs theoremStatement) + | throw <| IO.userError + s!"Could not match the elaborated parameters of '{extracted.declarationName}' against \ + its source signature; the generated delegation would under-apply it." let solutionExact := if solutionArgs.isEmpty then s!"Submission.{theoremName}" else s!"Submission.{theoremName} " ++ " ".intercalate solutionArgs.toList @@ -1817,16 +1986,16 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb let challengeFile := challengeImport ++ contextOpenBlock ++ contextUniverseBlock ++ (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ - contextVariablesBlock ++ + contextVariablesBlock ++ contextIncludeBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n" let solutionFile := solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextLocalSyntaxBlock ++ - contextVariablesBlock ++ + contextVariablesBlock ++ contextIncludeBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n exact {solutionExact}\n" let submissionFile := submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ - contextVariablesBlock ++ + contextVariablesBlock ++ contextIncludeBlock ++ "namespace Submission\n\n" ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n\n" ++ "end Submission\n" diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 9c59c6bd..b4d445df 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -50,13 +50,46 @@ def main : IO UInt32 := do pure <| assertEq "statement" actual ":\n let marker := \"fake := by and := sorry\"\n marker.length = 24" - check "extractStatementText ignores nested proof assignments" passes fails do + check "extractStatementText ignores default binder values" passes fails do let declaration := "theorem target (h : True := by trivial) : True := by\n" ++ - " have nested : True := sorry" - let actual ← extractStatementText "nested-assignment" "Demo.lean" declaration "target" + " sorry" + let actual ← extractStatementText "default-binder-value" "Demo.lean" declaration "target" pure <| assertEq "statement" actual "(h : True := by trivial) : True" + -- Regression for `substInv_X_sub_X_sq_eq_catalan`: the statement itself + -- opens a tactic block, which is not the declaration body. The body is the + -- `sorry` that runs to the end of the declaration. + check "extractStatementText ignores a tactic block inside the statement" passes fails do + let declaration := + "theorem target (n : ℕ) :\n" ++ + " haveI : Nonempty (Fin (n + 1)) := by\n" ++ + " exact ⟨0⟩\n" ++ + " n = n := by\n" ++ + " sorry" + let actual ← extractStatementText "statement-tactic-block" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual + ("(n : ℕ) :\n haveI : Nonempty (Fin (n + 1)) := by\n" ++ + " exact ⟨0⟩\n n = n") + + -- Not every hole is proved by `sorry`: the repository's CI canary really is + -- `:= by trivial`, so an unambiguous tactic body must still be recognised. + check "extractStatementText accepts a non-sorry tactic body" passes fails do + let declaration := "theorem target : True := by trivial" + let actual ← extractStatementText "tactic-body" "Demo.lean" declaration "target" + pure <| assertEq "statement" actual ": True" + + -- With no `sorry` to anchor on, an assignment in the proof is + -- indistinguishable from one in the statement, so guessing is not allowed. + check "extractStatementText rejects an ambiguous tactic body" passes fails do + let declaration := + "theorem target : True := by\n" ++ + " have h : True := by trivial\n" ++ + " exact h" + match ← (extractStatementText "ambiguous" "Demo.lean" declaration "target").toBaseIO with + | .ok statement => pure (some s!"expected failure, got {statement.quote}") + | .error _ => pure none + check "extractStatementText handles quote characters" passes fails do let declaration := "theorem target : ('\"' : Char) = '\"' := by sorry" @@ -84,6 +117,106 @@ def main : IO UInt32 := do pure <| assertEq "active notation kept" ((context.find? "local notation:arg").isSome) true |>.or (assertEq "closed notation dropped" ((context.find? "closed").isSome) false) + -- Regression for `honeycomb_connective_constant`: a `set_option … in` that + -- prefixes a removed declaration is not part of its `.ilean` range, and + -- leaving it behind strands an `in` with no command to apply to. + check "extendOverScopingPrefixes consumes a set_option prefix" passes fails do + let text := + "def helper : Nat := 0\n\n" ++ + "set_option maxRecDepth 10000 in\n" ++ + "theorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + let some prefixStart := Source.find source 0 "set_option".toList + | pure (some "no set_option in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) prefixStart + + check "extendOverScopingPrefixes consumes a prefix spread over lines" passes fails do + let text := + "def helper : Nat := 0\n\n" ++ + "set_option\n" ++ + " maxRecDepth 10000 in\n" ++ + "-- why we need it\n" ++ + "theorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + let some prefixStart := Source.find source 0 "set_option".toList + | pure (some "no set_option in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) prefixStart + + check "extendOverScopingPrefixes consumes a same-line prefix" passes fails do + let text := + "def helper : Nat := 0\n\n" ++ + "set_option maxRecDepth 10000 in theorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + let some prefixStart := Source.find source 0 "set_option".toList + | pure (some "no set_option in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) prefixStart + + check "extendOverScopingPrefixes leaves an unprefixed declaration alone" passes fails do + let text := "def helper : Nat := 0\n\ntheorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) target + + -- The previous declaration's text is off limits, so a line that merely ends + -- in `in` inside it can never be consumed. + check "extendOverScopingPrefixes stops at the previous declaration" passes fails do + let text := "theorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source target target) target + + check "variableBlockExplicitNames collects explicit binders only" passes fails do + let block := + "variable (n : ℕ) {α : Type*} [Fintype α]\n" ++ + " (A : Fin n → α)\n" ++ + "variable (K : Set α)\n\n" + pure <| assertEq "names" (variableBlockExplicitNames block) #["n", "A", "K"] + + -- Outer `variable` parameters are binders of the restated signature, so the + -- delegation has to apply them ahead of the declaration's own binders. + check "delegationArgs? passes outer variable parameters" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #["n", "A", "K", "hn", "hK"]) #["n", "A", "K"] #["hn", "hK"]) + (some #["n", "A", "K", "hn", "hK"]) + + -- The elaborated type of `bvp_comparison` continues past the signature into + -- the statement's own `∀ x ∈ Set.Icc 0 1, …`. Applying those binders left + -- `Solution.lean` referring to an unbound `x`, so only signature parameters + -- may be reported, and a report that disagrees with the source is rejected. + check "delegationArgs? keeps the declaration's own binders" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #["u", "hu"]) #[] #["u", "hu"]) (some #["u", "hu"]) + + -- The extractor reports nothing for a hole whose body is not a `sorry`, and + -- then the source signature is all we have — and all we need. + check "delegationArgs? falls back when nothing was reported" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #[]) #["n"] #["hn"]) (some #["hn"]) + + -- A parameter no `variable` command introduces cannot be applied by the + -- generated files, and dropping it would under-apply the delegation. + check "delegationArgs? refuses an unplaceable parameter" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #["x", "hn"]) #["n"] #["hn"]) none + + check "delegationArgs? falls back without extractor data" passes fails do + pure <| assertEq "args" (delegationArgs? none #["n"] #["h"]) (some #["h"]) + + -- An inaccessible binder name means the two views cannot be lined up. There + -- is then no safe answer: dropping the parameters we cannot place would + -- under-apply the delegation, so generation has to fail instead. + check "delegationArgs? refuses to under-apply" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #["n", "x✝"]) #["n"] #["_"]) none + -- Regression for https://github.com/leanprover/lean-eval/pull/467: -- Mathlib-style copyright headers precede imports. The generator must drop -- both the header and imports before copying trusted helpers into From b6da8269a667e6ced6e0854a1463f532b0892c57 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sun, 9 Aug 2026 12:29:47 +0000 Subject: [PATCH 4/4] fix: trust the elaborated parameters only where they mean something MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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) Claude-Session: https://claude.ai/code/session_01CGyHZAhLAv6PVnV9vsqbxd --- EvalTools/ExtractTheorem.lean | 48 ++--- EvalTools/Generate.lean | 188 ++++++++++++-------- tests/lean/EvalToolsTests/GenerateTest.lean | 33 +++- 3 files changed, 165 insertions(+), 104 deletions(-) diff --git a/EvalTools/ExtractTheorem.lean b/EvalTools/ExtractTheorem.lean index 70d3b901..891ccfbe 100644 --- a/EvalTools/ExtractTheorem.lean +++ b/EvalTools/ExtractTheorem.lean @@ -15,11 +15,12 @@ structure ExtractedTheorem where module : String sourceRange : SourceRange /-- Names of the explicit parameters bound by the declaration's *signature*, - in application order. This includes source-level `variable` parameters - exactly when Lean actually retained them in the declaration, and excludes - binders that belong to the statement itself (a leading `∀` in the - conclusion), which the generated delegation must not apply. -/ - explicitParameters : Array String + in application order, or `none` when they could not be determined. This + includes source-level `variable` parameters exactly when Lean actually + retained them in the declaration, and excludes binders that belong to the + statement itself (a leading `∀` in the conclusion), which the generated + delegation must not apply. -/ + explicitParameters : Option (Array String) /-- Names of declarations from the same module that appear (transitively) in the type or value of this theorem. Computed from the elaborated terms, so this captures uses introduced by typeclass synthesis (which the `.ilean` references metadata @@ -38,7 +39,7 @@ def sorryBodyArity : Expr → Option Nat | e => if e.isSorry then some 0 else none /-- Names of the explicit parameters bound by the declaration's signature, in -application order, or `#[]` when they cannot be determined. +application order, or `none` when they cannot be determined. An eval-problem hole has a bare `sorry` body, so its elaborated value is one `fun` binder per signature binder — the declaration's own binders together with @@ -48,22 +49,25 @@ with `∀` contributes `forallE` binders to the type but no lambda to the value, and applying those in the generated delegation would be wrong. The `sorry` body is what makes the count meaningful, so it is checked rather -than assumed: a tactic proof can introduce conclusion binders of its own, and -its lambdas say nothing about the signature. -/ -def signatureExplicitParameters (info : ConstantInfo) : Array String := Id.run do - let some arity := info.value? (allowOpaque := true) >>= sorryBodyArity | return #[] - let mut remaining := arity - let mut type := info.type - let mut names : Array String := #[] - while remaining > 0 do - match type with - | .forallE name _ body binderInfo => - if binderInfo == .default && !name.isAnonymous then - names := names.push name.toString - type := body - remaining := remaining - 1 - | _ => remaining := 0 - return names +than assumed. The check is necessary but not sufficient: `by intro x; sorry` +also elaborates to a lambda over `sorryAx`, and only the source text says +whether the body was a bare `sorry`. The generator decides that, and asks for +this list only when it was. -/ +def signatureExplicitParameters (info : ConstantInfo) : Option (Array String) := do + let arity ← info.value? (allowOpaque := true) >>= sorryBodyArity + return Id.run do + let mut remaining := arity + let mut type := info.type + let mut names : Array String := #[] + while remaining > 0 do + match type with + | .forallE name _ body binderInfo => + if binderInfo == .default && !name.isAnonymous then + names := names.push name.toString + type := body + remaining := remaining - 1 + | _ => remaining := 0 + return names def parseName (text : String) : Name := text.splitOn "." |>.foldl Name.str .anonymous diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index 8c2c36dc..a5b85248 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -132,12 +132,15 @@ private def parseExtractedTheorem (payload : String) : Except String ExtractedTh let endColumn ← range.getObjValAs? Nat "endColumn" let explicitParameters ← match json.getObjVal? "explicitParameters" with | .error _ => pure none - | .ok paramsJson => do - let paramsJson ← paramsJson.getArr? - let mut params : Array String := #[] - for paramJson in paramsJson do - params := params.push (← paramJson.getStr?) - pure (some params) + -- `null` for a declaration whose signature the extractor could not read. + | .ok paramsJson => + match paramsJson.getArr? with + | .error _ => pure none + | .ok paramsJson => do + let mut params : Array String := #[] + for paramJson in paramsJson do + params := params.push (← paramJson.getStr?) + pure (some params) let depNames : Array String ← match json.getObjVal? "sameModuleDependencies" with | .error _ => pure #[] @@ -674,7 +677,14 @@ Failing that — the `ci_regenerate_main_check` canary really is proved by only one. With a body that is not a `sorry` there is nothing left to tell an assignment in the statement apart from an assignment in the proof, so `none` is returned and the caller reports that it could not recover the statement. -/ -def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.run do +structure TheoremBody where + /-- Codepoint index of the `:=` that introduces the declaration's body. -/ + marker : Nat + /-- Whether that body is a bare `sorry`, possibly behind `by`. -/ + isBareSorry : Bool + deriving Inhabited + +def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option TheoremBody := Id.run do let mut i := start let mut roundDepth := 0 let mut squareDepth := 0 @@ -723,8 +733,10 @@ def Source.findTheoremBodyMarker (s : Source) (start : Nat) : Option Nat := Id.r else i := i + 1 return match sorryMarker with - | some marker => some marker - | none => if tacticMarkers == 1 then tacticMarker else none + | some marker => some { marker, isBareSorry := true } + | none => + if tacticMarkers == 1 then tacticMarker.map ({ marker := ·, isBareSorry := false }) + else none /-- Extract the theorem statement text from a sliced declaration body. The body marker is found lexically so direct `:= sorry` holes and flexible @@ -735,13 +747,23 @@ def extractStatementText (problemId : String) (sourcePath : System.FilePath) let some headerEnd := Source.findTheoremHeader src 0 theoremName | throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - let some bodyPos := Source.findTheoremBodyMarker src headerEnd + let some body := Source.findTheoremBodyMarker src headerEnd | throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - if bodyPos < headerEnd then + if body.marker < headerEnd then throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - return (Source.slice src headerEnd bodyPos).trimAscii.toString + return (Source.slice src headerEnd body.marker).trimAscii.toString + +/-- True when the sliced declaration's body is a bare `sorry`, possibly behind +`by`. Only then does the elaborated value carry one lambda per signature +binder, so only then is the extractor's parameter list meaningful: `by intro x; +sorry` elaborates to a lambda over `sorryAx` as well, but its lambda belongs to +the statement. -/ +def hasBareSorryBody (declarationText : String) : Bool := + match Source.findTheoremBodyMarker (Source.ofString declarationText) 0 with + | some body => body.isBareSorry + | none => false /-- Parse leading binders off a theorem-statement string. Returns pairs of `(opener, body)` for each leading `(...)`, `{...}`, or `[...]` group. -/ @@ -1288,22 +1310,23 @@ The extractor's list is only trusted when it agrees with what the source shows: it must end with `sourceArgs`, and every name ahead of them must be introduced by one of the re-emitted `variable` commands. -When the two views disagree, `sourceArgs` alone is the right answer only if it -cannot be missing anything — that is, if the extractor reports no more explicit -parameters than the source signature accounts for. A longer report means there -are parameters we cannot place (an inaccessible binder name, say), and -delegating without them would under-apply; `none` is returned so the caller can -fail rather than emit a workspace that does not compile. -/ +When the two views disagree there is no safe answer, because the disagreement +is itself evidence that one of them is wrong: delegating on either would emit a +workspace that does not compile. `none` is returned so the caller can fail +instead. + +`signatureParams?` is `none` for a declaration the extractor could not read. +The source binders are then all we have, and they are enough only when no outer +`variable` command could have contributed a parameter we cannot see. -/ def delegationArgs? (signatureParams? : Option (Array String)) (variableNames sourceArgs : Array String) : Option (Array String) := Id.run do - let some params := signatureParams? | return some sourceArgs - if params.size ≥ sourceArgs.size then - let outerCount := params.size - sourceArgs.size - if params.extract outerCount params.size == sourceArgs - && (params.extract 0 outerCount).all (fun p => variableNames.contains p) then - return some params - if params.size > sourceArgs.size then return none - return some sourceArgs + let some params := signatureParams? + | return if variableNames.isEmpty then some sourceArgs else none + if params.size < sourceArgs.size then return none + let outerCount := params.size - sourceArgs.size + if params.extract outerCount params.size != sourceArgs then return none + if !(params.extract 0 outerCount).all (fun p => variableNames.contains p) then return none + return some params /-! ## Render ChallengeDeps.lean -/ @@ -1364,6 +1387,37 @@ themselves onto a single following declaration. -/ private def scopingCommandKeywords : Array String := #["set_option", "open", "attribute", "include", "omit", "local", "scoped"] +/-- Split `[lowerBound, limit)` into lines, each paired with the tokens it +contributes outside comments. Comment state is carried forward across lines, so +a line inside a multi-line block comment contributes nothing — which is what +makes it recognisable as trivia when the caller walks back over it. -/ +private def gapLineTokens (source : Source) (lowerBound limit : Nat) : + Array (Nat × Array String) := Id.run do + let mut lines : Array (Nat × Array String) := #[] + let mut lineStart := lowerBound + let mut text : String := "" + let mut depth : Nat := 0 + let mut i := lowerBound + while i < limit do + if depth == 0 && Source.startsWithAt source i "--".toList then + while i < limit && source[i]! != '\n' do + i := i + 1 + else if Source.startsWithAt source i "/-".toList then + depth := depth + 1 + i := i + 2 + else if depth > 0 && Source.startsWithAt source i "-/".toList then + depth := depth - 1 + i := i + 2 + else if source[i]! == '\n' then + lines := lines.push (lineStart, splitWhitespace text) + text := "" + i := i + 1 + lineStart := i + else + if depth == 0 then text := text.push source[i]! + i := i + 1 + return lines.push (lineStart, splitWhitespace text) + /-- Move a removal range's start back over the command prefixes that scope onto the declaration being removed — `set_option … in`, `open … in`, and friends. A `.ilean` declaration range begins at the declaration proper, so such a prefix @@ -1371,59 +1425,35 @@ is not covered by it and would otherwise be stranded with no command to apply to. A prefix is recognised by its last token being `in`, and is then followed back -to the line opening the command, so prefixes spread over several lines are -consumed whole. Blank and comment-only lines are crossed, but are only dropped -if a prefix is found beyond them. `lowerBound` is the end of the previous -declaration; the search never crosses it, so text belonging to a declaration we -are keeping can never be consumed. -/ +to the line opening the command, so one spread over several lines is consumed +whole, as is one sharing the declaration's own line. Blank and comment-only +lines are crossed, but are only dropped if a prefix is found beyond them. +`lowerBound` is the end of the previous declaration; the search never crosses +it, so text belonging to a declaration we are keeping can never be consumed. -/ def extendOverScopingPrefixes (source : Source) (lowerBound start : Nat) : Nat := Id.run do - -- Start of the line that position `i` sits on, clamped to `lowerBound`. - let lineStartAt : Nat → Nat := fun i => Id.run do - let mut lineStart := i - while lineStart > lowerBound && source[lineStart - 1]! != '\n' do - lineStart := lineStart - 1 - return lineStart - let lineEndAt : Nat → Nat := fun i => Id.run do - let mut lineEnd := i - while lineEnd < source.size && source[lineEnd]! != '\n' do - lineEnd := lineEnd + 1 - return lineEnd - let lastTokenIsIn : String → Bool := fun text => (commandTokens text).back? == some "in" - -- Walk back from the line holding a prefix's `in` to the line opening that - -- command, so a prefix spread over several lines is consumed whole. Stays - -- put if no opening line is found rather than guessing. - let commandStartAt : Nat → Nat := fun inLineStart => Id.run do - let mut lineStart := inLineStart - while true do - let opensCommand := scopingCommandKeywords.any fun keyword => - (commandTokens (Source.slice source lineStart (lineEndAt lineStart)))[0]? == some keyword - if opensCommand then return lineStart - if lineStart ≤ lowerBound then return inLineStart - lineStart := lineStartAt (lineStart - 1) - return inLineStart + let lines := gapLineTokens source lowerBound start + let opensCommand : Nat → Bool := fun idx => + match (lines[idx]!.2)[0]? with + | some token => scopingCommandKeywords.contains token + | none => false let mut result := start - let mut cursor := start - while cursor > lowerBound do - let lineStart := lineStartAt cursor - if lastTokenIsIn (Source.slice source lineStart cursor) then - -- The prefix shares the declaration's line: `set_option … in theorem …`. - result := commandStartAt lineStart - cursor := result - else if lineStart ≤ lowerBound then + let mut idx := lines.size + while idx > 0 do + let (lineStart, tokens) := lines[idx - 1]! + if tokens.isEmpty then + -- Trivia is crossed in the hope of a prefix beyond it, and only dropped + -- if one is found. + idx := idx - 1 + else if tokens.back? != some "in" then return result else - let previousStart := lineStartAt (lineStart - 1) - let previous := Source.slice source previousStart (lineStart - 1) - let stripped := previous.trimAscii.toString - if stripped.isEmpty || stripped.startsWith "--" then - -- Trivia is crossed in the hope of a prefix beyond it, and only - -- dropped if one is found. - cursor := previousStart - else if lastTokenIsIn previous then - result := commandStartAt previousStart - cursor := result - else - return result + -- Follow the prefix back to the line that opens the command. Stay put + -- rather than guess if there is no such line within the gap. + let mut commandIdx := idx - 1 + while commandIdx > 0 && !opensCommand commandIdx do + commandIdx := commandIdx - 1 + result := if opensCommand commandIdx then lines[commandIdx]!.1 else lineStart + idx := commandIdx return result /-- Shared core of single- and multi-hole `ChallengeDeps.lean` rendering. @@ -1849,7 +1879,9 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl | some extracted => let variableNames := variableBlockExplicitNames (extractContextVariables sourceText (some extracted) #[]) - match delegationArgs? extracted.explicitParameters variableNames sourceArgs with + let signatureParams? := + if hasBareSorryBody declText then extracted.explicitParameters else none + match delegationArgs? signatureParams? variableNames sourceArgs with | some args => pure args | none => throw <| IO.userError @@ -1957,7 +1989,9 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb extractContextVariables sourceText (some extracted) theoremBinderNames let contextIncludeBlock := extractContextIncludes sourceText (some extracted) - let some solutionArgs := delegationArgs? extracted.explicitParameters + let signatureParams? := + if hasBareSorryBody declText then extracted.explicitParameters else none + let some solutionArgs := delegationArgs? signatureParams? (variableBlockExplicitNames contextVariablesBlock) (explicitBinderApplicationArgs theoremStatement) | throw <| IO.userError diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index b4d445df..4c59f3b2 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -157,6 +157,20 @@ def main : IO UInt32 := do | pure (some "no set_option in fixture") pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) prefixStart + check "extendOverScopingPrefixes crosses a block comment" passes fails do + let text := + "def helper : Nat := 0\n\n" ++ + "set_option maxRecDepth 10000 in\n" ++ + "/- reason\n" ++ + " spelled out -/\n" ++ + "theorem target : True := by sorry\n" + let source := Source.ofString text + let some target := Source.find source 0 "theorem".toList + | pure (some "no theorem in fixture") + let some prefixStart := Source.find source 0 "set_option".toList + | pure (some "no set_option in fixture") + pure <| assertEq "start" (extendOverScopingPrefixes source 0 target) prefixStart + check "extendOverScopingPrefixes leaves an unprefixed declaration alone" passes fails do let text := "def helper : Nat := 0\n\ntheorem target : True := by sorry\n" let source := Source.ofString text @@ -195,11 +209,22 @@ def main : IO UInt32 := do pure <| assertEq "args" (delegationArgs? (some #["u", "hu"]) #[] #["u", "hu"]) (some #["u", "hu"]) - -- The extractor reports nothing for a hole whose body is not a `sorry`, and - -- then the source signature is all we have — and all we need. + -- A hole whose body is not a `sorry` gets no report, and then the source + -- signature is all we have. That is enough when no `variable` is in scope. check "delegationArgs? falls back when nothing was reported" passes fails do pure <| assertEq "args" - (delegationArgs? (some #[]) #["n"] #["hn"]) (some #["hn"]) + (delegationArgs? none #[] #["hn"]) (some #["hn"]) + + -- But with a `variable` in scope it is not: Lean may have retained one, and + -- the source signature does not say. Guessing would under-apply. + check "delegationArgs? refuses to guess past a variable" passes fails do + pure <| assertEq "args" + (delegationArgs? none #["n"] #["hn"]) none + + -- An empty report is not the same as no report: it says, reliably, that the + -- declaration takes no explicit parameters. + check "delegationArgs? trusts an empty report" passes fails do + pure <| assertEq "args" (delegationArgs? (some #[]) #["n"] #[]) (some #[]) -- A parameter no `variable` command introduces cannot be applied by the -- generated files, and dropping it would under-apply the delegation. @@ -207,8 +232,6 @@ def main : IO UInt32 := do pure <| assertEq "args" (delegationArgs? (some #["x", "hn"]) #["n"] #["hn"]) none - check "delegationArgs? falls back without extractor data" passes fails do - pure <| assertEq "args" (delegationArgs? none #["n"] #["h"]) (some #["h"]) -- An inaccessible binder name means the two views cannot be lined up. There -- is then no safe answer: dropping the parameters we cannot place would