diff --git a/EvalTools/ExtractTheorem.lean b/EvalTools/ExtractTheorem.lean index b289f18f..891ccfbe 100644 --- a/EvalTools/ExtractTheorem.lean +++ b/EvalTools/ExtractTheorem.lean @@ -14,6 +14,13 @@ structure ExtractedTheorem where declarationName : String module : String sourceRange : SourceRange + /-- Names of the explicit parameters bound by the declaration's *signature*, + 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 @@ -25,6 +32,43 @@ structure ExtractedTheorem where kind : String deriving ToJson +/-- 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 `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 +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. 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 @@ -180,6 +224,7 @@ def extractTheorem (moduleNameText declNameText : String) : IO ExtractedTheorem declarationName := toString resolvedDeclName module := moduleNameText sourceRange := sourceRange + explicitParameters := signatureExplicitParameters constantInfo sameModuleDependencies := deps.map toString kind := kind } diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index d7c2bc1a..a5b85248 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,17 @@ 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 + -- `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 #[] @@ -140,7 +152,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 } @@ -605,21 +617,153 @@ 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 + +/-- 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, 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. -/ +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 + 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 + 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 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) + 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 match sorryMarker with + | 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. -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 body := Source.findTheoremBodyMarker src headerEnd | throw <| IO.userError s!"Could not recover theorem statement text for '{problemId}' from {sourcePath}" - if byPos < 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 byPos).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. -/ @@ -961,12 +1105,38 @@ 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 + +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 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 +1152,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 +1207,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 +1233,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 @@ -1078,6 +1254,80 @@ 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. -/ +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) + +/-! ## 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 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 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 -/ /-- The byte range `[start, stop)` of a single source declaration in `sourceText`, @@ -1128,6 +1378,83 @@ 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"] + +/-- 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 +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 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 + 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 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 + -- 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. @@ -1158,11 +1485,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 - 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. + 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 := #[] @@ -1537,7 +1874,20 @@ 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 sourceArgs := explicitBinderApplicationArgs statement + let explicitArgs ← match extracteds.find? (fun e => e.declarationName == fullName) with + | some extracted => + let variableNames := + variableBlockExplicitNames (extractContextVariables sourceText (some extracted) #[]) + let signatureParams? := + if hasBareSorryBody declText then extracted.explicitParameters else none + match delegationArgs? signatureParams? 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 @@ -1617,10 +1967,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 +1981,25 @@ 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 contextLocalSyntaxBlock := + extractContextLocalSyntaxDeclarations sourceText (some extracted) let contextVariablesBlock := extractContextVariables sourceText (some extracted) theoremBinderNames + let contextIncludeBlock := + extractContextIncludes sourceText (some extracted) + let signatureParams? := + if hasBareSorryBody declText then extracted.explicitParameters else none + let some solutionArgs := delegationArgs? signatureParams? + (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 let includeNamespaces := hasChallengeDeps || !localImports.isEmpty let contextOpenBlock ← extractContextOpens entry.id sourcePath sourceText (some extracted) includeNamespaces @@ -1655,13 +2018,18 @@ 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 ++ + (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ + contextVariablesBlock ++ contextIncludeBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n sorry\n" let solutionFile := - solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextVariablesBlock ++ + solutionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextLocalSyntaxBlock ++ + contextVariablesBlock ++ contextIncludeBlock ++ s!"theorem {theoremName} {theoremStatement} := by\n exact {solutionExact}\n" let submissionFile := - submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ contextVariablesBlock ++ + submissionImports ++ contextOpenBlock ++ contextUniverseBlock ++ + (if hasChallengeDeps then contextLocalSyntaxBlock else contextSyntaxBlock) ++ + 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 9e1b61cc..4c59f3b2 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -24,6 +24,222 @@ 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 "extractStatementText ignores default binder values" passes fails do + let declaration := + "theorem target (h : True := by trivial) : True := by\n" ++ + " 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" + 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" ++ + "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) + + -- 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 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 + 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"]) + + -- 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? 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. + check "delegationArgs? refuses an unplaceable parameter" passes fails do + pure <| assertEq "args" + (delegationArgs? (some #["x", "hn"]) #["n"] #["hn"]) none + + + -- 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