From e1a871e86c71895466303cc1d05259118f7eb617 Mon Sep 17 00:00:00 2001 From: Mikhail Mayorov Date: Fri, 11 Sep 2026 15:36:52 +0400 Subject: [PATCH 1/5] Make the project search path robust to nested packages and LEAN_PATH getAllLakePaths stopped at the first directory containing .lake, so a git dependency that ships several packages side by side (e.g. packages/Hammer/HammerCore) contributed only its top-level build directory and imports from the sibling packages failed to resolve. Recurse into such sub-packages as well. Also honour LEAN_PATH when it is set: 'lake env' derives it from the manifest, which is authoritative for layouts the directory walk cannot infer. parseFile now sets the search path itself (and enables initializer execution) before elaborating, so the library entry point works without the caller having to replicate what bins/ExtractSorry does. Co-Authored-By: Claude Fable 5.1 --- LeanUtils/ExtractSorry.lean | 3 +++ LeanUtils/Utils.lean | 20 ++++++++++++++++++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/LeanUtils/ExtractSorry.lean b/LeanUtils/ExtractSorry.lean index 9760732..e574b11 100644 --- a/LeanUtils/ExtractSorry.lean +++ b/LeanUtils/ExtractSorry.lean @@ -38,6 +38,9 @@ def extractSorries (T : InfoTree) : IO (List <| SorryData Format) := /-- `parseFile myLeanFile` extracts the sorries contained in the Lean file `myLeanFile`. -/ def parseFile (path : System.FilePath) : IO (List ParsedSorry) := do + unsafe enableInitializersExecution + let projectSearchPath ← getProjectSearchPath path + searchPathRef.set projectSearchPath -- Throw an error if the oleans of the file can't be found... path.checkOLeans let (fileMap, trees) ← extractInfoTrees path diff --git a/LeanUtils/Utils.lean b/LeanUtils/Utils.lean index 8aa01d1..3363e29 100644 --- a/LeanUtils/Utils.lean +++ b/LeanUtils/Utils.lean @@ -131,7 +131,17 @@ partial def getAllLakePaths (path : System.FilePath) : IO (Array System.FilePath unless ← path.pathExists do return #[] let dirEntries := (← path.readDir).map IO.FS.DirEntry.path if dirEntries.contains (path / ".lake") then - return (← getAllLakePaths <| path / ".lake/packages").push (path / ".lake/build/lib/lean") + -- A built package. Recurse into its own dependencies, and ALSO into any + -- sub-packages sitting directly inside it: one git dependency can ship + -- several packages side by side (e.g. `packages/Hammer/HammerCore`), which + -- lake puts on LEAN_PATH but which this short-circuit would otherwise skip. + let nested ← getAllLakePaths <| path / ".lake/packages" + let subPkgs ← dirEntries.filterM fun entry => do + if entry == path / ".lake" then return false + if !(← entry.isDir) then return false + (entry / ".lake").pathExists + let fromSubPkgs ← subPkgs.mapM getAllLakePaths + return (nested ++ fromSubPkgs.flatten).push (path / ".lake/build/lib/lean") else let dirEntries ← dirEntries.filterM fun path ↦ path.isDir return (← dirEntries.mapM getAllLakePaths).flatten @@ -144,7 +154,13 @@ def getProjectSearchPath (path : System.FilePath) : IO (System.SearchPath) := do let rootDir ← getProjectRootDirPath path let paths ← getAllLakePaths rootDir let originalSearchPath ← getBuiltinSearchPath (← findSysroot) - return originalSearchPath.append paths.toList + -- Honour LEAN_PATH when it is set: `lake env` derives it from the manifest, + -- which is authoritative for layouts a directory walk cannot infer. + let envPaths : List System.FilePath ← do + match ← IO.getEnv "LEAN_PATH" with + | some raw => pure (System.SearchPath.parse raw) + | none => pure [] + return originalSearchPath.append (paths.toList ++ envPaths) def System.FilePath.checkOLeans (path : System.FilePath) : IO Unit := do discard <| Lean.findOLean (← moduleNameOfFileName path none) From c947cc9a23f57baeae8feb71ebdd39f568b4d58e Mon Sep 17 00:00:00 2001 From: Mikhail Mayorov Date: Fri, 11 Sep 2026 15:39:16 +0400 Subject: [PATCH 2/5] ExtractSorry: report the token's byte range and kind; wire the golden tests into Lake Each ParsedSorry now carries start_byte/end_byte and kind ("tactic" or "term"). Tools that rewrite the source need exactly this: a byte range is what a splice replaces, and the kind decides whether the replacement needs a leading 'by'. On input the three fields are optional (Option, so the derived FromJson accepts a record that lacks them), which keeps records with only line/column positions -- the shape the SorryDB database stores -- valid input for KernelCheck and the goal extractor; ParsedSorry.acceptsKind is the helper consumers use to filter by kind when one is given. A sorry tactic also elaborates to a sorry term at the same position, and the two records used to coincide and be deduplicated. With kind they differ, so dedupByToken merges them explicitly and keeps the tactic record. The golden tests were not runnable from a fresh checkout: LeanUtilsTest was not a Lake target, so its fixture was never built and findOLean could not resolve the fixture's module name. Declare it (and 'bins', so tests can import the executables' root modules), make it the test driver, and regenerate the expected output. Co-Authored-By: Claude Fable 5.1 --- LeanUtils/ExtractSorry.lean | 22 +++++++++++++-- LeanUtils/Utils.lean | 44 +++++++++++++++++++++-------- LeanUtilsTest/TestExtractSorry.lean | 32 ++++++++++++++++++--- lakefile.toml | 13 +++++++++ 4 files changed, 94 insertions(+), 17 deletions(-) diff --git a/LeanUtils/ExtractSorry.lean b/LeanUtils/ExtractSorry.lean index e574b11..96ab4ea 100644 --- a/LeanUtils/ExtractSorry.lean +++ b/LeanUtils/ExtractSorry.lean @@ -36,6 +36,25 @@ where def extractSorries (T : InfoTree) : IO (List <| SorryData Format) := traverseInfoTree ppGoalIfNoMVar T +/-- One record per source token. + +A `sorry` *tactic* elaborates to a `sorry` *term*, so the info trees carry two +nodes for the same token with the same goal. They differ only in `kind`, which +would otherwise defeat the plain deduplication; merge them and keep the +`"tactic"` record, since that is the position the token occupies in the source +(a replacement there needs no leading `by`). -/ +def dedupByToken (sorries : List ParsedSorry) : List ParsedSorry := + sorries.foldl (init := []) fun acc ps => + let sameToken (q : ParsedSorry) := + q.startPos == ps.startPos && q.endPos == ps.endPos && + q.parentDecl == ps.parentDecl && q.goal == ps.goal + match acc.find? sameToken with + | none => acc ++ [ps] + | some q => + if q.kind != some "tactic" && ps.kind == some "tactic" then + acc.map fun r => if sameToken r then ps else r + else acc + /-- `parseFile myLeanFile` extracts the sorries contained in the Lean file `myLeanFile`. -/ def parseFile (path : System.FilePath) : IO (List ParsedSorry) := do unsafe enableInitializersExecution @@ -48,5 +67,4 @@ def parseFile (path : System.FilePath) : IO (List ParsedSorry) := do -- `extractSorries` on infotrees that arise from theorems/lemmas/definitions/... let sorryLists ← trees.mapM extractSorries let sorryLists : List ParsedSorry := sorryLists.flatten'.map (SorryData.toParsedSorry fileMap) - let sorryLists := sorryLists.dedup' - return sorryLists + return dedupByToken sorryLists diff --git a/LeanUtils/Utils.lean b/LeanUtils/Utils.lean index 3363e29..6eef4ff 100644 --- a/LeanUtils/Utils.lean +++ b/LeanUtils/Utils.lean @@ -42,26 +42,45 @@ def visitSorryNode {Out} (ctx : ContextInfo) (node : Info) else return none | _ => return none +/-- One `sorry` found in a file. + +`startByte`/`endByte` and `kind` are emitted by `ExtractSorry` and consumed by +tools that rewrite the source (a byte range is what a splice needs; `kind` +says whether the token is the `sorry` *tactic* or the `sorry` *term*, which +decides whether a replacement needs a leading `by`). They are optional on +input so that a record with only line/column positions -- the shape stored in +the SorryDB database -- still deserializes. -/ structure ParsedSorry where goal : String startPos : Position endPos : Position parentDecl : Name hash : UInt64 + startByte : Option Nat := none + endByte : Option Nat := none + /-- `"tactic"` or `"term"`; `none` accepts either. -/ + kind : Option String := none deriving DecidableEq, FromJson +/-- `true` unless `kind` is set and differs from `k`. -/ +def ParsedSorry.acceptsKind (ps : ParsedSorry) (k : String) : Bool := + ps.kind.all (· == k) + instance : ToJson ParsedSorry where - toJson ps := Json.mkObj [ - ("goal", Json.str ps.goal), - ("location", Json.mkObj [ - ("start_line", Json.num ps.startPos.line), - ("start_column", Json.num ps.startPos.column), - ("end_line", Json.num ps.endPos.line), - ("end_column", Json.num ps.endPos.column) - ]), - ("parentDecl", Json.str ps.parentDecl.toString), - ("hash", Json.num ps.hash.toNat) - ] + toJson ps := + let location := [ + ("start_line", Json.num ps.startPos.line), + ("start_column", Json.num ps.startPos.column), + ("end_line", Json.num ps.endPos.line), + ("end_column", Json.num ps.endPos.column) + ] ++ (ps.startByte.map fun b => ("start_byte", Json.num b)).toList + ++ (ps.endByte.map fun b => ("end_byte", Json.num b)).toList + Json.mkObj <| [ + ("goal", Json.str ps.goal), + ("location", Json.mkObj location), + ("parentDecl", Json.str ps.parentDecl.toString), + ("hash", Json.num ps.hash.toNat) + ] ++ (ps.kind.map fun k => ("kind", Json.str k)).toList def SorryData.toParsedSorry {Out} [ToString Out] (fileMap : FileMap) : SorryData Out → ParsedSorry := @@ -72,6 +91,9 @@ def SorryData.toParsedSorry {Out} [ToString Out] (fileMap : FileMap) : endPos := fileMap.toPosition stx.getTailPos?.get! parentDecl hash := Hashable.hash <| ToString.toString out + startByte := some stx.getPos?.get!.byteIdx + endByte := some stx.getTailPos?.get!.byteIdx + kind := some (if isSorryTactic stx then "tactic" else "term") } instance : ToString ParsedSorry where diff --git a/LeanUtilsTest/TestExtractSorry.lean b/LeanUtilsTest/TestExtractSorry.lean index 73a247f..5658433 100644 --- a/LeanUtilsTest/TestExtractSorry.lean +++ b/LeanUtilsTest/TestExtractSorry.lean @@ -3,22 +3,46 @@ import bins.ExtractSorry /-- info: [{"parentDecl": "test", "location": - {"start_line": 5, "start_column": 4, "end_line": 5, "end_column": 9}, + {"start_line": 5, + "start_column": 4, + "start_byte": 78, + "end_line": 5, + "end_column": 9, + "end_byte": 83}, + "kind": "tactic", "hash": 1590982770643673912, "goal": "⊢ True"}, {"parentDecl": "test", "location": - {"start_line": 6, "start_column": 2, "end_line": 6, "end_column": 7}, + {"start_line": 6, + "start_column": 2, + "start_byte": 86, + "end_line": 6, + "end_column": 7, + "end_byte": 91}, + "kind": "tactic", "hash": 3234805056349482567, "goal": "someLemma : True\n⊢ 1 + 1 = 2"}, {"parentDecl": "test'", "location": - {"start_line": 10, "start_column": 2, "end_line": 10, "end_column": 7}, + {"start_line": 10, + "start_column": 2, + "start_byte": 125, + "end_line": 10, + "end_column": 7, + "end_byte": 130}, + "kind": "term", "hash": 11128604812966687648, "goal": "⊢ 1 + 1 = 2"}, {"parentDecl": "test'''", "location": - {"start_line": 26, "start_column": 4, "end_line": 26, "end_column": 9}, + {"start_line": 26, + "start_column": 4, + "start_byte": 446, + "end_line": 26, + "end_column": 9, + "end_byte": 451}, + "kind": "tactic", "hash": 13350658948405900884, "goal": "⊢ 1 + 2 = 3"}] -/ diff --git a/lakefile.toml b/lakefile.toml index f0ffa21..d66aed2 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,10 +1,16 @@ name = "LeanUtils" version = "0.1.0" defaultTargets = ["KernelCheck", "ExtractSorry"] +testDriver = "LeanUtilsTest" [[lean_lib]] name = "LeanUtils" +# The executables' root modules, as a library so that tests can import them +# (`import bins.ExtractSorry`) and Lake knows how to build them on demand. +[[lean_lib]] +name = "bins" + [[lean_exe]] name = "KernelCheck" root = "bins.KernelCheck" @@ -12,3 +18,10 @@ root = "bins.KernelCheck" [[lean_exe]] name = "ExtractSorry" root = "bins.ExtractSorry" +supportInterpreter = true + +# `#guard_msgs` golden tests plus their fixture files. Building the fixtures is +# what makes `findOLean` resolve their module names when a test re-elaborates them. +[[lean_lib]] +name = "LeanUtilsTest" +globs = ["LeanUtilsTest.+"] From b2aca4967de921f414d0025b77034199e74f33ec Mon Sep 17 00:00:00 2001 From: Mikhail Mayorov Date: Fri, 11 Sep 2026 15:41:20 +0400 Subject: [PATCH 3/5] Share the sorry-locating code between KernelCheck and new tools; fix KernelCheck's verdict on kernel errors Move findTargetEnv out of bins/KernelCheck.lean into LeanUtils/TargetEnv.lean so that other executables can recover the elaboration state at a sorry (the ContextInfo, the local context, the goal type, and the positions of the enclosing commands). Two behaviours change on the way: * A token that closes several goals (constructor <;> sorry, all_goals sorry) used to abort with "Found more than one goal". The recorded goal text now selects the intended goal, compared with whitespace collapsed because different tools wrap goals at different widths; only a genuinely ambiguous token is refused, with the candidates listed. * The record's kind, when given, restricts the match to term or tactic nodes (ParsedSorry.acceptsKind); without it both are accepted as before. KernelCheck looks the parent declaration's TheoremVal up in the environment (it is only needed for the level parameters) and runs elaboration in the sorry's own local context rather than an empty one. Also: when addDecl throws, kernelCheck reported success = true alongside the kernel's error message. Report success = false. A golden test covers the three outcomes (accepted, rejected by name, rejected by the kernel). Co-Authored-By: Claude Fable 5.1 --- LeanUtils/TargetEnv.lean | 184 +++++++++++++++++++++++++++++ LeanUtilsTest/TestKernelCheck.lean | 37 ++++++ bins/KernelCheck.lean | 104 +++------------- 3 files changed, 238 insertions(+), 87 deletions(-) create mode 100644 LeanUtils/TargetEnv.lean create mode 100644 LeanUtilsTest/TestKernelCheck.lean diff --git a/LeanUtils/TargetEnv.lean b/LeanUtils/TargetEnv.lean new file mode 100644 index 0000000..6224044 --- /dev/null +++ b/LeanUtils/TargetEnv.lean @@ -0,0 +1,184 @@ +import LeanUtils.ExtractSorry +import Lean.Meta.Basic + +/-! +# Locating one `sorry` in a file's info trees + +Given a `ParsedSorry` (position, parent declaration, goal text) this module +re-elaborates the file and recovers the elaboration state at that token: the +`ContextInfo`, the local context, and the goal type. `KernelCheck` uses it to +check a candidate proof term against that goal, and `ExtractGoal` uses it to +restate the goal as a standalone theorem. + +Two situations need care: +* a `sorry` tactic also elaborates to a `sorry` term, so one token yields two + nodes; they carry the same type and either will do; +* one token can close several goals (`constructor <;> sorry`, `all_goals sorry`). + The recorded goal text then selects the intended one, compared with whitespace + collapsed because different tools wrap goals at different widths. +-/ + +open Lean Meta Elab Term Expr Meta Tactic + +/-- The elaboration state at one `sorry`. -/ +structure TargetEnvData where + ctx : ContextInfo + lctx : LocalContext + type : Expr + /-- Start positions of the enclosing commands, outermost first: the + declaration's own command and any `… in` wrappers around it. -/ + commandPositions : List Position + +private structure MatchedTarget where + ctx : ContextInfo + type? : Option Expr + goal? : Option MVarId + lctx : LocalContext + commandPositions : List Position := [] + +/-- Collapse all whitespace, so goals that differ only in line wrapping compare equal. + +The dataset's goal text was rendered by SorryDB's REPL at a different line width than +`ExtractSorry` uses here; the content is identical, the line breaks are not. -/ +def goalConclusion (s : String) : String := + -- everything after the LAST turnstile; resets the accumulator at each one + s.foldl (fun acc c => if c == '⊢' then "" else acc.push c) "" + +def normalizeGoalText (s : String) : String := + -- character fold rather than `String.split`: the latter returns `List String` on + -- some toolchains and `Std.Iter String.Slice` on others, which breaks the build + -- for whichever Lean versions the fleet does not happen to be tested against. + (s.foldl (fun acc c => + if c.isWhitespace then + if acc.endsWith " " then acc else acc.push ' ' + else acc.push c) "").trim + +def findTargetEnv (tree : InfoTree) (targetSorry : ParsedSorry) : IO (List TargetEnvData) := do + let matched ← tree.visitM (m := IO) (postNode := fun ctx info _ children => do + let targets : List MatchedTarget := (children.flatMap' Option.toList).flatten' + match info with + | .ofTermInfo ti => + if !targetSorry.acceptsKind "term" || !isSorryTerm ti.stx then + return targets + let some pos := ti.stx.getPos? | return targets + if targetSorry.startPos != ctx.fileMap.toPosition pos then + return targets + let some type := ti.expectedType? | return targets + return targets ++ [{ + ctx + type? := some type + goal? := none + lctx := ti.lctx + }] + | .ofTacticInfo ti => + if !targetSorry.acceptsKind "tactic" || !isSorryTactic ti.stx then + return targets + let some pos := ti.stx.getPos? | return targets + if targetSorry.startPos != ctx.fileMap.toPosition pos then + return targets + let goal ← match ti.goalsBefore with + | [goal] => pure goal + | goals => do + -- A single `sorry` token can close several goals (`constructor <;> sorry`). + -- SorryDB records one entry per goal, all sharing this source position, so + -- the entry's printed goal is what distinguishes them. Select the matching + -- one instead of refusing; still refuse if it is ambiguous. + let mut matching : List MVarId := [] + for candidate in goals do + if let some mdecl := ti.mctxBefore.decls.find? candidate then + let rendered ← ctx.runMetaM mdecl.lctx do + return toString (← ppGoal candidate) + if normalizeGoalText rendered == normalizeGoalText targetSorry.goal then + matching := matching ++ [candidate] + match matching with + | [goal] => pure goal + | _ => + -- report how the selection went, so a rendering mismatch (0 matched) + -- can be told apart from a genuinely ambiguous token (>1 matched) + let rendered ← goals.mapM fun candidate => do + match ti.mctxBefore.decls.find? candidate with + | some mdecl => ctx.runMetaM mdecl.lctx do return toString (← ppGoal candidate) + | none => pure "" + throw (IO.userError s!"Found more than one goal ({goals.length} goals, \ + {matching.length} matched target); target={(normalizeGoalText targetSorry.goal).take 300}; \ + candidates={(rendered.map fun r => (normalizeGoalText r).take 300)}") + let some mdecl := ti.mctxBefore.decls.find? goal + | throw (IO.userError "Could not recover the target goal's local context") + return targets ++ [{ + ctx + type? := none + goal? := some goal + lctx := mdecl.lctx + }] + | .ofCommandInfo ci => + let some pos := ci.stx.getPos? | return targets + let commandPos := ctx.fileMap.toPosition pos + return targets.map fun target => + { target with commandPositions := commandPos :: target.commandPositions } + | _ => return targets) + + let matched := matched.get! + let targetDatas ← matched.mapM fun target => do + target.ctx.runMetaM target.lctx do + let type ← match target.type?, target.goal? with + | some type, none => pure type + | none, some goal => goal.getType + | _, _ => throwError "Bad case" + return [{ + ctx := target.ctx + lctx := target.lctx + type + commandPositions := + if target.commandPositions.isEmpty then [targetSorry.startPos] + else target.commandPositions + }] + + return targetDatas.flatten'.filter fun data => + data.ctx.parentDecl? == some targetSorry.parentDecl + + +def findSorryTargetFromFile (path rawSorry : String) : IO (Except String (FileMap × TargetEnvData)) := do + unsafe enableInitializersExecution + let path : System.FilePath := { toString := path } + let path ← IO.FS.realPath path + let projectSearchPath ← getProjectSearchPath path + searchPathRef.set projectSearchPath + let a := Json.parse rawSorry + let json ← match a with + | .ok json => pure json + | .error e => return .error s!"Failed to parse input as valid JSON {e}" + + let parsedSorry : ParsedSorry ← match (Lean.FromJson.fromJson? json) with + | .ok parsedSorry => pure parsedSorry + | .error e => return .error s!"Failed to deserialize ParsedSorry: {e}" + + let (fileMap, trees) ← extractInfoTrees path + + let targetEnvs ← trees.mapM (fun t => findTargetEnv t parsedSorry) + + let targetEnvs := targetEnvs.flatten' + -- We might have both term-mode and tactic-mode info trees for the same source-level 'sorry' + -- (since the 'sorry' tactic will end up emitting a 'sorry' term) + -- We just pick the first one - as long as they all have the same type (which we check), + -- shouldn't matter + let some singleData := targetEnvs[0]? | return .error s!"Did not find any targetEnv" + if targetEnvs.all (fun d => d.type == singleData.type) then + return .ok (fileMap, singleData) + -- One source `sorry` can legitimately close SEVERAL goals (`all_goals sorry`, + -- `<;> sorry`), so the infotrees genuinely carry different types. That is not an + -- ambiguity to give up on: the recorded goal says which one this task is. Match on + -- the conclusion -- sibling goals share a local context and differ only in the target. + let wantConcl := normalizeGoalText (goalConclusion parsedSorry.goal) + let mut matching : List TargetEnvData := [] + let mut rendered : List String := [] + for d in targetEnvs do + let txt ← d.ctx.runMetaM d.lctx do + return toString (← ppExpr (← instantiateMVars d.type)) + rendered := rendered ++ [normalizeGoalText txt] + if normalizeGoalText txt == wantConcl then + matching := matching ++ [d] + match matching with + | d :: _ => return .ok (fileMap, d) + | [] => + return .error s!"Found different types for infotrees corresponding to same sorry; \ + target={wantConcl.take 200}; candidates={rendered.map (·.take 200)}" diff --git a/LeanUtilsTest/TestKernelCheck.lean b/LeanUtilsTest/TestKernelCheck.lean new file mode 100644 index 0000000..de83228 --- /dev/null +++ b/LeanUtilsTest/TestKernelCheck.lean @@ -0,0 +1,37 @@ +import bins.KernelCheck + +/-! `KernelCheck ` checks a candidate term +against the goal of one `sorry`. The record only needs positions, parent +declaration, goal and hash (a decimal string: JSON numbers cannot carry a full +`UInt64`); `kind`/byte offsets are optional (see `ParsedSorry`). -/ + +def trueSorry : String := + "{\"goal\": \"⊢ True\", \"startPos\": {\"line\": 5, \"column\": 4}, \"endPos\": {\"line\": 5, \"column\": 9}, \"parentDecl\": \"test\", \"hash\": \"1590982770643673912\"}" + +/-- +info: {"success": true, "error": null} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithSorries.lean", trueSorry, "trivial"] + +-- A term that still relies on `sorryAx` is rejected by name, before the kernel. +/-- +info: {"success": false, "error": "Contains banned constant names: [sorryAx]"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithSorries.lean", trueSorry, "sorry"] + +-- A term of the wrong type is rejected by the kernel. +/-- +info: {"success": false, + "error": + "(kernel) declaration type mismatch, '_uniq.1' has type\n Nat\nbut it is expected to have type\n True"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithSorries.lean", trueSorry, "(0 : Nat)"] diff --git a/bins/KernelCheck.lean b/bins/KernelCheck.lean index 2b4117b..7a7d7c9 100644 --- a/bins/KernelCheck.lean +++ b/bins/KernelCheck.lean @@ -1,4 +1,5 @@ import LeanUtils.ExtractSorry +import LeanUtils.TargetEnv import Lean.Meta.Basic open Lean Meta Elab Term Expr Meta Tactic @@ -48,58 +49,6 @@ inductive KernelCheckResult where deriving Repr -structure TargetEnvData where - ctx: ContextInfo - theoremVal: TheoremVal - type: Expr - - - -def findTargetEnv (tree: InfoTree) (targetSorry: ParsedSorry): IO (List TargetEnvData) := do - -- TODO - explain why an empty LocalContext is okay. Maybe - local context occurs within TermElabM - we're at top-level decl, so no local context - let a ← (do (tree.visitM (m := IO) (postNode := fun ctx i _ as => do - let head := (as.flatMap' Option.toList).flatten' - match i with - -- TODO - deduplicate this - | .ofTermInfo ti => - if targetSorry.startPos == ctx.fileMap.toPosition ti.stx.getPos?.get! && isSorryTerm ti.stx then do - if let some type := ti.expectedType? then - return head ++ ([(ctx, some (type), none)]) - else - return head ++ [(ctx, none, none)] - else - return head - | .ofTacticInfo ti => - -- TODO - do we need the 'mctxBefore' stuff from 'visitSorryNode'? - if targetSorry.startPos == ctx.fileMap.toPosition ti.stx.getPos?.get! && isSorryTactic ti.stx then do - let goal ← if let [goal] := ti.goalsBefore then pure goal else (throw (IO.userError "Found more than one goal")) - return head ++ ([(ctx, none, some goal)]) - else - return head - | _ => return head - - ))) - - let matchedCtxs := a.get! - let targetDatas ← (matchedCtxs.mapM (fun (ctx, type, goal) => do - ctx.runMetaM {} do - if let some oldDecl := ctx.env.find? targetSorry.parentDecl then - match oldDecl with - | .thmInfo info => - match (type, goal) with - | (some type, none) => return [({ctx := ctx, theoremVal := info, type := type} : TargetEnvData)] - | (none, some goal) => - let goalType ← goal.getType - return [({ctx := ctx, theoremVal := info, type := goalType} : TargetEnvData)] - | _ => throwError "Bad case" - | _ => throwError "Bad decl type" - else - throwError ("Missing parentDecl in environment") - )) - let allTargets := targetDatas.flatten'.filter (fun data => data.ctx.parentDecl? == (some targetSorry.parentDecl)) - return allTargets - - structure KernelCheckOutput where success: Bool error: Option String @@ -110,7 +59,7 @@ check that `expr` has type `type` -/ -- TODO - change the error type to make it harder to accidentally return success -- remove the 'panics' -def kernelCheck (sorryFilePath: System.FilePath) (targetData: TargetEnvData) (expr : SerializedExpr) (type: Expr) (fileMap: FileMap) (bannedNames : List Name) : IO (KernelCheckOutput) := do +def kernelCheck (sorryFilePath: System.FilePath) (targetData: TargetEnvData) (theoremVal : TheoremVal) (expr : SerializedExpr) (type: Expr) (fileMap: FileMap) (bannedNames : List Name) : IO (KernelCheckOutput) := do let expr := deserializeExpr expr let (res, _) ← Core.CoreM.toIO (ctx := {fileName := sorryFilePath.fileName.get!, fileMap := fileMap}) (s := { env := targetData.ctx.env }) do let bannedNames := (expr.collectNames bannedNames).dedup' @@ -121,54 +70,35 @@ def kernelCheck (sorryFilePath: System.FilePath) (targetData: TargetEnvData) (ex } else try - addDecl (Declaration.thmDecl {targetData.theoremVal with value := expr, type := type, name := ← mkFreshId}) + addDecl (Declaration.thmDecl {theoremVal with value := expr, type := type, name := ← mkFreshId}) return { success := true, error := none } catch e => + -- addDecl threw: the kernel rejected the declaration. return { - success := true, + success := false, error := ← e.toMessageData.toString } return res def parseAndCheck (args : List String): IO KernelCheckOutput := do if let [path, rawSorry, rawExpr] := args then - unsafe enableInitializersExecution - let path : System.FilePath := { toString := path } - let path ← IO.FS.realPath path - let projectSearchPath ← getProjectSearchPath path - searchPathRef.set projectSearchPath - let a := Json.parse rawSorry - let json ← match a with - | .ok json => pure json - | .error e => return { - success := false, - error := some s!"Failed to parse input as valid JSON {e}" - } - - let parsedSorry: ParsedSorry ← match (Lean.FromJson.fromJson? json) with - | .ok parsedSorry => pure parsedSorry - | .error e => return { - success := false - error := some s!"Failed to deserialize ParsedSorry: {e}" - } - - let (fileMap, trees) ← extractInfoTrees path + -- The parent declaration's TheoremVal supplies the level parameters for the + -- declaration the candidate is checked as. + let parentDecl ← match Json.parse rawSorry >>= fromJson? (α := ParsedSorry) with + | .ok (ps : ParsedSorry) => pure ps.parentDecl + | .error e => return { success := false, error := some s!"Failed to deserialize ParsedSorry: {e}" } - let targetEnvs ← trees.mapM (fun t => findTargetEnv t parsedSorry) + let (fileMap, singleData) ← match ← findSorryTargetFromFile path rawSorry with + | .ok x => pure x + | .error e => return { success := false, error := some e } - let targetEnvs := targetEnvs.flatten' - -- We might have both term-mode and tactic-mode info trees for the same source-level 'sorry' - -- (since the 'sorry' tactic will end up emitting a 'sorry' term) - -- We just pick the first one - as long as they all have the same type (which we check), - -- shouldn't matter - let some singleData := targetEnvs[0]? | throw (IO.userError s!"Did not find any targetEnv") - if !targetEnvs.all (fun d => d.type == singleData.type) then - throw (IO.userError "Found different types for infotrees corresponding to same sorry") + let some (.thmInfo theoremVal) := singleData.ctx.env.find? parentDecl + | return { success := false, error := some s!"Parent declaration {parentDecl} is not a theorem in the environment" } - singleData.ctx.runMetaM {} do + singleData.ctx.runMetaM singleData.lctx do let mut elabedExpr := none try let a ← TermElabM.run (elabStringAsExpr rawExpr singleData.type) @@ -179,7 +109,7 @@ def parseAndCheck (args : List String): IO KernelCheckOutput := do error := some s!"Elaboration error: {(← e.toMessageData.format).pretty}" } - kernelCheck path singleData (serializeExpr elabedExpr.get!) singleData.type fileMap [`sorryAx] + kernelCheck path singleData theoremVal (serializeExpr elabedExpr.get!) singleData.type fileMap [`sorryAx] else return { success := false, From 0b90cc18df68b2133a442fed263f59b87f97a9d9 Mon Sep 17 00:00:00 2001 From: Mikhail Mayorov Date: Fri, 11 Sep 2026 15:45:31 +0400 Subject: [PATCH 4/5] Add ExtractGoal: restate the goal at a sorry as a standalone theorem ExtractGoal [flags] re-elaborates the file, recovers the goal and local context at the given sorry (via LeanUtils.TargetEnv), reverts the context into binders and prints * the source prefix up to the enclosing command (where the helper belongs, followed by any '... in' wrappers around the declaration), * 'theorem mytheorem : := sorry', and * the application 'mytheorem ' that closes the original goal, separated by marker lines. Replacing the sorry with 'exact ' and inserting the helper before the enclosing command gives a file whose only new sorry is the helper's, so the restatement is validated by compiling that file. Universe parameters are renamed so they cannot collide with section universes at the insertion point. The default rendering is compact. A set of flags each changes one pretty-printer or context-handling decision for goals whose compact rendering does not re-elaborate: pp.analyze on the application, sanitizing the context (let-bound proofs become hypotheses, sorry-tainted and unused locals are cleared), rendering the signature from the type expression so that the pp.* flags apply to it, pp.proofs on the statement, and hoisting closed Prop-typed subterms into binders (only Props, so the statement stays equivalent by proof irrelevance). Three situations are refused rather than rendered wrongly: a statement still containing an omitted term, a goal whose type depends on an earlier sorry, and a multi-goal token whose recorded goal matches none of the candidates. All failures are reported as {"error": ...}. Golden tests cover a tactic sorry with a hypothesis, a term sorry, and the multi-goal selection and refusal. The README documents the record format, the payload, the flags and the refusals. Builds and passes the tests on Lean 4.17.0 (the pin), 4.18.0 and 4.27.0-rc1. Co-Authored-By: Claude Fable 5.1 --- LeanUtilsTest/LeanFileWithMultiGoalSorry.lean | 5 + LeanUtilsTest/TestExtractGoal.lean | 52 +++ README.md | 132 +++++- bins/ExtractGoal.lean | 441 ++++++++++++++++++ lakefile.toml | 7 +- 5 files changed, 635 insertions(+), 2 deletions(-) create mode 100644 LeanUtilsTest/LeanFileWithMultiGoalSorry.lean create mode 100644 LeanUtilsTest/TestExtractGoal.lean create mode 100644 bins/ExtractGoal.lean diff --git a/LeanUtilsTest/LeanFileWithMultiGoalSorry.lean b/LeanUtilsTest/LeanFileWithMultiGoalSorry.lean new file mode 100644 index 0000000..da33f3d --- /dev/null +++ b/LeanUtilsTest/LeanFileWithMultiGoalSorry.lean @@ -0,0 +1,5 @@ +import Lean + +-- One `sorry` token closes two goals; SorryDB records one entry per goal. +theorem both : (1 : Nat) = 1 ∧ (2 : Nat) = 2 := by + constructor <;> sorry diff --git a/LeanUtilsTest/TestExtractGoal.lean b/LeanUtilsTest/TestExtractGoal.lean new file mode 100644 index 0000000..50a93ee --- /dev/null +++ b/LeanUtilsTest/TestExtractGoal.lean @@ -0,0 +1,52 @@ +import bins.ExtractGoal + +/-! `ExtractGoal [flags]` restates the goal at one `sorry` +as a standalone theorem, and prints the term that closes the original goal with +it. Only positions, parent declaration, goal and hash are required in the record +(hash as a decimal string). The payload has three parts, separated by markers: +the source prefix up to the enclosing command, the helper theorem, and the +application. -/ + +-- A tactic `sorry` with one hypothesis in scope. +/-- +info: {"ok": + "import Lean\n\n\n-- sorrydb-helper-start\ntheorem mytheorem (someLemma : True) : 1 + 1 = 2 := sorry\n-- sorrydb-application: mytheorem someLemma"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithSorries.lean", + "{\"goal\": \"someLemma : True\\n⊢ 1 + 1 = 2\", \"startPos\": {\"line\": 6, \"column\": 2}, \"endPos\": {\"line\": 6, \"column\": 7}, \"parentDecl\": \"test\", \"hash\": \"3234805056349482567\"}"] + +-- A term-mode `sorry`: the prefix now contains the whole preceding declaration. +/-- +info: {"ok": + "import Lean\n\ntheorem test : 1 + 1 = 2 := by\n have someLemma : True := by\n sorry\n sorry\n\n\n\n-- sorrydb-helper-start\ntheorem mytheorem : 1 + 1 = 2 := sorry\n-- sorrydb-application: mytheorem"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithSorries.lean", + "{\"goal\": \"⊢ 1 + 1 = 2\", \"startPos\": {\"line\": 10, \"column\": 2}, \"endPos\": {\"line\": 10, \"column\": 7}, \"parentDecl\": \"test'\", \"hash\": \"11128604812966687648\"}"] + +-- One token, two goals: the recorded goal text selects which one is meant. +/-- +info: {"ok": + "import Lean\n\n-- One `sorry` token closes two goals; SorryDB records one entry per goal.\n\n-- sorrydb-helper-start\ntheorem mytheorem : 2 = 2 := sorry\n-- sorrydb-application: mytheorem"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithMultiGoalSorry.lean", + "{\"goal\": \"⊢ 2 = 2\", \"startPos\": {\"line\": 5, \"column\": 18}, \"endPos\": {\"line\": 5, \"column\": 23}, \"parentDecl\": \"both\", \"hash\": \"0\", \"kind\": \"tactic\"}"] + +-- ... and a goal text matching neither is refused, listing the candidates. +/-- +info: {"error": + "Found different types for infotrees corresponding to same sorry; target=3 = 3; candidates=[1 = 1, 2 = 2]"} +--- +info: 0 +-/ +#guard_msgs in +#eval main ["LeanUtilsTest/LeanFileWithMultiGoalSorry.lean", + "{\"goal\": \"⊢ 3 = 3\", \"startPos\": {\"line\": 5, \"column\": 18}, \"endPos\": {\"line\": 5, \"column\": 23}, \"parentDecl\": \"both\", \"hash\": \"0\", \"kind\": \"tactic\"}"] diff --git a/README.md b/README.md index fb20642..645ae8a 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,132 @@ # LeanUtils -Lean scripts for indexing sorries and verifying proofs +Lean scripts for indexing sorries and verifying proofs. + +Three executables, all dependency-free and driven from the command line with +JSON in and JSON out: + +| binary | purpose | +|---|---| +| `ExtractSorry ` | list every `sorry` in a file with its goal and position | +| `KernelCheck ` | check a candidate proof term against the goal of one `sorry` | +| `ExtractGoal [flags]` | restate the goal of one `sorry` as a standalone theorem | + +```bash +lake build +lake test # #guard_msgs golden tests in LeanUtilsTest/ +``` + +Each binary re-elaborates the given file, so the project it belongs to must +already be built (`lake build` in that project) and the binary must run with a +Lean toolchain matching the project's `lean-toolchain`. Run it from the +project's root, or under `lake env`, so that `LEAN_PATH` is available; the +search path is otherwise reconstructed by walking the project's `.lake` +directories. + +## The sorry record + +`ExtractSorry` prints one record per `sorry` token: + +```json +{"parentDecl": "test", + "location": {"start_line": 6, "start_column": 2, "start_byte": 86, + "end_line": 6, "end_column": 7, "end_byte": 91}, + "kind": "tactic", + "hash": 3234805056349482567, + "goal": "someLemma : True\n⊢ 1 + 1 = 2"} +``` + +`start_byte`/`end_byte` are the token's byte range, which is what a tool that +rewrites the source needs to splice at. `kind` is `"tactic"` or `"term"`: a +replacement in tactic position needs no leading `by`, one in term position does. +A `sorry` tactic also elaborates to a `sorry` term at the same position; the two +are merged into the tactic record. A token that closes several goals +(`constructor <;> sorry`) yields one record per goal, distinguished by `goal`. + +`KernelCheck` and `ExtractGoal` take a record back as their second argument, in +the shape the `ParsedSorry` structure deserializes: + +```json +{"goal": "someLemma : True\n⊢ 1 + 1 = 2", + "startPos": {"line": 6, "column": 2}, "endPos": {"line": 6, "column": 7}, + "parentDecl": "test", "hash": "3234805056349482567", + "kind": "tactic", "startByte": 86, "endByte": 91} +``` + +`hash` is a decimal string here (a JSON number cannot carry a full `UInt64`). +`kind`, `startByte` and `endByte` are optional; without `kind` both term and +tactic nodes are accepted. `goal` is only consulted when one token closes +several goals, to select the intended one. + +## ExtractGoal + +Turns the goal at a `sorry` into a theorem that can be stated on its own, plus +the term that closes the original goal with it. The local context at the sorry +is reverted into binders, so the theorem is exactly the goal with its context +quantified; the proof is left as `sorry` for whoever wants to prove it. + +``` +$ ExtractGoal LeanUtilsTest/LeanFileWithSorries.lean '{"goal": "...", "startPos": {"line": 6, "column": 2}, ...}' +{"ok": + "import Lean\n\n + -- sorrydb-helper-start\n + theorem mytheorem (someLemma : True) : 1 + 1 = 2 := sorry\n + -- sorrydb-application: mytheorem someLemma"} +``` + +The payload has three parts separated by the two marker lines: the file's +source up to the start of the enclosing command (the helper belongs before +it, together with any `… in` wrappers, which are reproduced after the +marker), the helper theorem, and the application term. Replacing the original +`sorry` by `exact ` (or `by exact …` in term position) and +inserting the helper before the enclosing command yields a file whose only new +`sorry` is the helper's; the caller compiles that file to validate the +restatement. Universe parameters are renamed `sorrydb_u_1, …` so they cannot +collide with section universes at the insertion point. + +The contract has three refusals, each reported as `{"error": "..."}`: + +* `compact theorem signature contains omitted terms (⋯)` — a proof inside a + data value was elided by the pretty printer and the statement would not + re-elaborate; see `--show-proofs` and `--abstract-proofs`. +* `its type depends on an earlier sorry` — the goal mentions a `sorryAx` + from another sorry; no restatement can name that term. +* `Found more than one goal` / `Found different types for infotrees` — the + token closes several goals and the record's `goal` matches none of them. + +### Rendering flags + +The default rendering is the compact one (`pp.proofs` off, notation on). Each +flag changes one pretty-printer or context-handling decision; callers typically +try the default first and add flags only when the restatement fails to +elaborate. + +| flag | effect | +|---|---| +| `--analyze` | render the application with `pp.analyze`: named arguments (`(d := d)`) for implicits the call site cannot infer | +| `--sanitize-context` | turn `let`-bound proofs into hypotheses; clear locals whose type or value mentions `sorryAx`, unused `let`s, and unused inaccessible locals | +| `--assumption-holes` | an argument whose value is an inaccessible local renders as `?_`; replace it by `(by assumption)` | +| `--expr-signature` | render the statement from the type expression (`name : ∀ …`) instead of `MessageData.signature`, so the flags below can act on it | +| `--no-fun-binder-types` | `pp.funBinderTypes := false` | +| `--no-coercion-types` | `pp.coercions.types := false` (drop `⇑f : A → B` ascriptions) | +| `--no-field-notation` | `pp.fieldNotation := false` (`X.ρ` can re-resolve to the wrong constant through an `abbrev`) | +| `--coe-explicit` | print `DFunLike.coe (F := …)` explicitly | +| `--numeric-types` | `pp.numericTypes := true` (`(2 : ℝ)`) | +| `--show-proofs` | `pp.proofs := true` on the statement: proofs nested in data print instead of `⋯` (lossless by proof irrelevance) | +| `--abstract-proofs` | hoist closed `Prop`-typed subterms of the goal into binders `sorrydb_prf_i`, `_` at the call site; only `Prop`s, so the statement stays equivalent | + +## KernelCheck + +Elaborates the term against the goal in the sorry's own local context, rejects +terms that mention a banned constant (`sorryAx`) by name, and otherwise asks +the kernel to accept the declaration: + +``` +$ KernelCheck LeanUtilsTest/LeanFileWithSorries.lean '{"goal": "⊢ True", ..., "parentDecl": "test", "hash": "1590982770643673912"}' trivial +{"success": true, "error": null} +``` + +## Toolchains + +`lean-toolchain` pins the version the tests run with. The sources are kept +free of version-specific API where possible (see `LeanUtils/Backports.lean`) +and have been built against Lean 4.17 through the 4.27 release candidates. diff --git a/bins/ExtractGoal.lean b/bins/ExtractGoal.lean new file mode 100644 index 0000000..7388446 --- /dev/null +++ b/bins/ExtractGoal.lean @@ -0,0 +1,441 @@ +import Lean +import LeanUtils.TargetEnv + +open Lean Elab Meta Expr MVarId + +def Pp.compactOptions (numericTypes : Bool := false) : Options → Options := + (pp.proofs.set · false |> + (pp.deepTerms.set · true |> + (pp.numericTypes.set · numericTypes |> + (pp.maxSteps.set · 1000000 |> + (pp.match.set · true |> + (pp.motives.all.set · false |> + (pp.coercions.types.set · true |> + (pp.unicode.fun.set · true |> + (pp.funBinderTypes.set · true |> + (pp.explicit.set · false |> + (pp.universes.set · false))))))))))) + +def Pp.extractionOptions (numericTypes : Bool) (opts : Options) : Options := + Pp.compactOptions numericTypes opts + +/-- Rendering flags for the helper's *statement*. + +Each corresponds to a delaborator habit that does not round-trip: +* `noFunBinderTypes` — forced `fun (a : T) ↦ …` ascriptions can name types with no + matching instance (an appended `OracleSpec` prints as a bare arrow). +* `noCoercionTypes` — `pp.coercions.types` ascribes `⇑f`'s *unbundled* arrow, losing + every implicit that only the bundled hom type pins. +* `noFieldNotation` — `X.ρ` re-resolves to the wrong constant when the type is a + reducible alias whose namespace defines a same-named field. +* `coeExplicit` — print `DFunLike.coe (F := )` explicitly; needs `pp.analyze` + *and* `pp.coercions := false` together, neither works alone. +* `showProofs` — re-enable `pp.proofs`, which `Pp.compactOptions` turns off for every + rung. A `Prop`-typed proof nested inside a *data* value (`⟨σ, ⁻o⟩ : OSequence`) + is then elided as `⋯` in the statement and no rung can recover it, even though the + term is already spelled out in scope. Printing it is lossless: by definitional + proof irrelevance any proof of that `Prop` is interchangeable, so the restated + signature elaborates to the same type. Kept off by default because proofs are + usually large and irrelevant; this is a retry rung, not a new baseline. +-/ +structure SigFlags where + noFunBinderTypes : Bool := false + noCoercionTypes : Bool := false + noFieldNotation : Bool := false + coeExplicit : Bool := false + analyze : Bool := false + showProofs : Bool := false + deriving Inhabited + +def Pp.signatureOptions (numericTypes : Bool) (f : SigFlags) (opts : Options) : Options := + let opts := Pp.compactOptions numericTypes opts + let opts := if f.noFunBinderTypes then pp.funBinderTypes.set opts false else opts + let opts := if f.noCoercionTypes then pp.coercions.types.set opts false else opts + let opts := if f.noFieldNotation then opts.setBool `pp.fieldNotation false else opts + let opts := if f.analyze then opts.setBool `pp.analyze true else opts + let opts := if f.showProofs then pp.proofs.set opts true else opts + if f.coeExplicit then + opts.setBool `pp.coercions false + |>.setBool `pp.analyze true + |>.setBool `pp.analyze.checkInstances true + else opts + +/-- Find a maximal *closed* proof subterm that is not already an fvar. + +`Meta.isProof` guarantees the subterm's type is a `Prop`, which is exactly the +guard we need: abstracting a `Prop` is lossless in both directions by definitional +proof irrelevance, whereas abstracting a data subterm would yield a strictly +stronger and possibly false statement. Subterms with loose bvars are skipped -- +they cannot be hoisted into an outer binder -- and fvars are skipped because they +already print by name rather than as `⋯`. +-/ +partial def collectProofSubterms (e : Expr) : MetaM (Array Expr) := do + if !e.hasLooseBVars && !e.isFVar then + if ← Meta.isProof e then + return #[e] + match e with + | .app f a => return (← collectProofSubterms f) ++ (← collectProofSubterms a) + | .lam _ t b _ => return (← collectProofSubterms t) ++ (← collectProofSubterms b) + | .forallE _ t b _ => return (← collectProofSubterms t) ++ (← collectProofSubterms b) + | .letE _ t v b _ => + return (← collectProofSubterms t) ++ (← collectProofSubterms v) + ++ (← collectProofSubterms b) + | .mdata _ b => collectProofSubterms b + | .proj _ _ b => collectProofSubterms b + | _ => return #[] + +/-- All maximal closed proof subterms, the ones containing a `sorry` first. + +Ordering matters: a subterm that mentions `sorryAx` is what actually blocks +extraction, and hoisting it is the whole point. An unrelated instance proof found +earlier in the traversal must not stop us from reaching it -- the previous version +searched for a single subterm and gave up if that one turned out unusable. -/ +def proofSubtermCandidates (e : Expr) : MetaM (Array Expr) := do + let all ← collectProofSubterms e + return (all.filter (·.hasSorry)) ++ (all.filter (fun t => !t.hasSorry)) + +partial def getFreshConstName (base : Name) : MetaM Name := do + let env ← getEnv + let consts := env.constants + let rec loop (i : Nat) := + let cand := + if i = 0 then base else base.appendIndexAfter i + if consts.contains cand then + loop (i + 1) + else + cand + return loop 0 + +def keepUsedSignatureLevelParams (name : Name) (levels : List Name) + (signature : String) : String := + match signature.splitOn "}" with + | first :: rest => + if first.startsWith (name.toString ++ ".{") then + let body := String.intercalate "}" rest + let used := levels.filter fun level => + (body.splitOn level.toString).length > 1 + let renderedName := + if used.isEmpty then + name.toString + else + name.toString ++ ".{" ++ + String.intercalate ", " (used.map (·.toString)) ++ "}" + renderedName ++ body + else + signature + | [] => signature + +/-- +Obtain the inaccessible fvars from the given local context. An fvar is +inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a +later fvar with the same user name. +-/ +def Lean.LocalContext.inaccessibleFVars (lctx : LocalContext) : + Array LocalDecl := + let (result, _) := + lctx.foldr (β := Array LocalDecl × Std.HashSet Name) + (init := (Array.mkEmpty lctx.numIndices, {})) + fun ldecl (result, seen) => + let result := + if ldecl.isImplementationDetail || ldecl.userName.hasMacroScopes || + seen.contains ldecl.userName then + result.push ldecl + else + result + (result, seen.insert ldecl.userName) + result.reverse + + +/-- +Rename all inaccessible fvars. An fvar is inaccessible if (a) its user name is +inaccessible or (b) it is shadowed by a later fvar with the same user name. This +function gives all inaccessible fvars a unique, accessible user name. It returns +the new goal and the fvars that were renamed. +-/ +def Lean.MVarId.renameInaccessibleFVars (mvarId : MVarId) : + MetaM (MVarId × Array FVarId) := do + let mdecl ← mvarId.getDecl + let mut lctx := mdecl.lctx + let inaccessibleFVars := lctx.inaccessibleFVars + if inaccessibleFVars.isEmpty then + return (mvarId, #[]) + let mut renamedFVars := Array.mkEmpty lctx.decls.size + for ldecl in inaccessibleFVars do + let newName := lctx.getUnusedName ldecl.userName + lctx := lctx.setUserName ldecl.fvarId newName + renamedFVars := renamedFVars.push ldecl.fvarId + let newMVar ← mkFreshExprMVarAt lctx mdecl.localInstances mdecl.type + mvarId.assign newMVar + return (newMVar.mvarId!, renamedFVars) + +/-- Convert local proof definitions into ordinary hypotheses. This is safe for +proofs because their particular values are irrelevant, while generalizing a +data-valued `let` could make the extracted theorem strictly stronger. -/ +def Lean.MVarId.abstractLocalProofValues (mvarId : MVarId) : + MetaM (MVarId × Array FVarId) := do + let mdecl ← mvarId.getDecl + let candidates := + mdecl.lctx.foldl (init := #[]) fun result ldecl => + if ldecl.isLet then result.push ldecl else result + let mut lctx := mdecl.lctx + let mut abstracted := #[] + for ldecl in candidates do + if ← isProp ldecl.type then + lctx := lctx.modifyLocalDecl ldecl.fvarId fun + | .ldecl index fvarId userName type _ _ kind => + .cdecl index fvarId userName type .default kind + | decl => decl + abstracted := abstracted.push ldecl.fvarId + if abstracted.isEmpty then + return (mvarId, abstracted) + let newMVar ← mkFreshExprMVarAt lctx mdecl.localInstances mdecl.type + mvarId.assign newMVar + return (newMVar.mvarId!, abstracted) + +/-- Preserve all locals except blockers that Lean can prove are unused. Local +proof definitions become hypotheses. Unused local definitions are removed. +Used data-valued definitions retain their values; if such a value contains a +sorry, it is removed only when `tryClearMany'` proves it unused, and otherwise +extraction is rejected by the final sorry check. +The returned arrays contain removed locals and abstracted proof definitions. -/ +def Lean.MVarId.sanitizeForExtraction (mvarId : MVarId) : + MetaM (MVarId × Array FVarId × Array FVarId) := do + let (mvarId, abstractedProofs) ← mvarId.abstractLocalProofValues + let contaminated := (← mvarId.getDecl).lctx.foldl (init := #[]) fun result ldecl => + let valueHasSorry := ldecl.value?.any (fun value => value.hasSorry) + if ldecl.type.hasSorry || valueHasSorry then + result.push ldecl.fvarId + else + result + let (mvarId, clearedContaminated) ← mvarId.tryClearMany' contaminated + let localDefinitions := (← mvarId.getDecl).lctx.foldl (init := #[]) fun result ldecl => + if ldecl.isLet then result.push ldecl.fvarId else result + let (mvarId, clearedDefinitions) ← mvarId.tryClearMany' localDefinitions + let inaccessible := (← mvarId.getDecl).lctx.inaccessibleFVars.map (·.fvarId) + let (mvarId, clearedInaccessible) ← mvarId.tryClearMany' inaccessible + return (mvarId, clearedContaminated ++ clearedDefinitions ++ clearedInaccessible, + abstractedProofs) + +/-- Format a goal into a type signature for a declaration named `name`. + +Example output: `myTheorem (a b : Nat) : a + b = b + a`. + +The return values are: +* A formatted piece of `MessageData`, like `m!"myTheorem (a b : Nat) : a + b = b + a"`. +-/ +def mkThmHeader (name : Name) (g : MVarId) (numericTypes : Bool := false) + (sanitizeContext : Bool := false) (analyze : Bool := false) + (sigFlags : SigFlags := {}) (exprSignature : Bool := false) + (abstractProofs : Bool := false) : + TermElabM (MessageData × MessageData × List Name) := + withoutModifyingEnv <| withoutModifyingState do + let originalLctx := (← g.getDecl).lctx + let (g, removedFVarIds, abstractedProofFVarIds) ← + if sanitizeContext then g.sanitizeForExtraction else pure (g, #[], #[]) + let (g, inaccessibleFVarIds) ← g.renameInaccessibleFVars + + -- Hoist proof subterms of the goal into real locals *before* the context is + -- reverted -- afterwards every context variable is a bound variable, so the + -- subterms we want are no longer closed and cannot be abstracted. + -- `generalize` introduces each as a local, which the existing revert then turns + -- into a binder; marking them inaccessible makes the call site pass a hole, and + -- unification restores the original proof term. + let (g, generalizedFVarIds, generalizedTypes) ← do + if !abstractProofs then + pure (g, #[], #[]) + else + let mut g := g + let mut introduced : Array FVarId := #[] + -- record each type here: the generalized fvar lives only in the + -- intermediate goal's context, so `fvarId.getType` cannot find it later + let mut types : Array Expr := #[] + for _ in [0:8] do + let next? ← g.withContext do + let ty ← instantiateMVars (← g.getType) + -- take the first *usable* candidate rather than giving up on the first + -- unusable one; sorry-bearing subterms are tried first + for sub in ← proofSubtermCandidates ty do + let subTy ← instantiateMVars (← inferType sub) + unless subTy.hasSorry || subTy.hasLooseBVars || subTy.hasExprMVar do + return some sub + return none + match next? with + | none => break + | some sub => + let name := Name.mkSimple s!"sorrydb_prf_{introduced.size + 1}" + let subTy ← g.withContext do instantiateMVars (← inferType sub) + let (ids, g') ← g.generalize #[{ expr := sub, xName? := some name }] + g := g' + introduced := introduced ++ ids + types := types ++ ids.map (fun _ => subTy) + pure (g, introduced, types) + let inaccessibleFVarIds := inaccessibleFVarIds ++ generalizedFVarIds + + let (fvarIds, defaultApplicationFVarIds) := + (← g.getDecl).lctx.foldl (init := (#[], #[])) fun (ids, applicationIds) decl => + if decl.isAuxDecl then + (ids, applicationIds) + else + let ids := ids.push decl.fvarId + let applicationIds := + if decl.isLet then applicationIds else applicationIds.push decl.fvarId + (ids, applicationIds) + let applicationFVarIds := + if sanitizeContext then + originalLctx.foldl (init := #[]) fun ids decl => + if decl.isAuxDecl || removedFVarIds.contains decl.fvarId then ids + else if decl.isLet && !abstractedProofFVarIds.contains decl.fvarId then ids + else ids.push decl.fvarId + else + defaultApplicationFVarIds + let (_, g) ← g.revert (clearAuxDeclsInsteadOfRevert := false) fvarIds + let fvars ← + if sanitizeContext then + applicationFVarIds.mapM fun fvarId => pure (mkFVar fvarId) + else + applicationFVarIds.mapM fun fvarId => do + if inaccessibleFVarIds.contains fvarId then + let ty ← match generalizedFVarIds.findIdx? (· == fvarId) with + | some i => pure generalizedTypes[i]! + | none => fvarId.getType + mkFreshExprSyntheticOpaqueMVar ty + else + pure (mkFVar fvarId) + let ty ← instantiateMVars (← g.getType) + if ty.hasExprMVar then + -- TODO: turn metavariables into new hypotheses? + throwError "Extracted goal has metavariables: {ty}" + let ty ← Term.levelMVarToParam ty + if ty.hasSorry then + throwError "Unsupported extracted goal: its type depends on an earlier sorry" + let originalLevels := (collectLevelParams {} ty).params.toList + -- Pretty-printer-generated names such as `u_1` may already be in scope + -- through a section variable, or may be genuinely new. Give every helper + -- declaration its own predictable level names so both cases elaborate the + -- same way when the rendered theorem is inserted back into the source. + let levels := originalLevels.mapIdx fun index _ => + Name.mkSimple s!"sorrydb_u_{index + 1}" + let ty := ty.instantiateLevelParams originalLevels (levels.map mkLevelParam) + addAndCompile <| Declaration.axiomDecl + { name := name + levelParams := levels + isUnsafe := false + type := ty } + -- `MessageData.signature` routes through `ppSignature`, which delaborates the + -- bare `.const` -- so `topDownAnalyze` has no application to look at and + -- `pp.analyze` is structurally a no-op there. Rendering the quantified type + -- directly makes the statement a real, re-renderable artifact that the retry + -- ladder can act on. Kept behind a flag so the default path is byte-identical. + let signature ← withOptions + (Pp.signatureOptions numericTypes sigFlags) do + if exprSignature then + let levelSuffix := + if levels.isEmpty then "" + else ".{" ++ String.intercalate ", " (levels.map (·.toString)) ++ "}" + addMessageContext m!"{name.toString ++ levelSuffix} : {ty}" + else + addMessageContext <| MessageData.signature name + let application := mkAppN (← mkConstWithFreshMVarLevels name) fvars + discard <| inferType application + let application ← instantiateMVars application + -- `pp.analyze` re-renders the application with the *minimum* annotations + -- needed for it to elaborate back to the same term: named arguments like + -- `(d := d)` for implicits the call site cannot infer, and nothing at all + -- where inference already works. Without it the implicit arguments are + -- passed in the term but omitted from the rendering, so re-elaboration + -- fails with `don't know how to synthesize implicit argument`. + let application ← withOptions + (fun opts => + (pp.explicit.set (pp.universes.set (pp.proofs.set opts true) false) false) + |>.setBool `pp.mvars false |>.setBool `pp.analyze analyze) do + addMessageContext <| MessageData.ofExpr application + return (signature, application, levels) + +/-- +Render the application, optionally turning unfilled holes into `by assumption`. + +`mkThmHeader` passes a fresh metavariable for any argument whose value is an +*inaccessible* local, since such a local cannot be named at the call site. That +renders as `?_`, which does not elaborate. For a binder the conclusion never +mentions, any inhabitant of the right type will do, so `by assumption` is enough; +for one the conclusion does mention, a wrong choice changes the statement and the +candidate fails to compile, so the compile stage is the safety net. +-/ +def renderApplication (application : MessageData) (assumptionHoles : Bool) + (abstractProofs : Bool) : CoreM String := do + let rendered ← application.toString + if assumptionHoles then + return rendered.replace "?_" "(by assumption)" + else if abstractProofs then + -- holes standing for abstracted proof binders: `_` lets unification put the + -- original proof term back, which is what makes the round trip exact + return rendered.replace "?_" "_" + else + return rendered + +def getTheoremPosition (ci : ConstantVal) : MetaM (Option Position) := do + return (← findDeclarationRanges? ci.name).map (·.range.pos) + +def extractGoal (args : List String): IO (Except String String) := do + let readRawSorry : IO String := do + let stdin ← IO.getStdin + return (← stdin.getLine).trim + let (path, rawSorry, numericTypes, sanitizeContext, analyze, assumptionHoles, + sigFlags, exprSignature, abstractProofs) ← match args with + | path :: rest => do + let flags := rest.filter (fun arg => arg.startsWith "--") + let positional := rest.filter (fun arg => !arg.startsWith "--") + let rawSorry ← match positional with + | [] => readRawSorry + | [raw] => pure raw + | _ => throw (IO.userError "Expected at most one JSON argument") + let sigFlags : SigFlags := { + noFunBinderTypes := flags.contains "--no-fun-binder-types" + noCoercionTypes := flags.contains "--no-coercion-types" + noFieldNotation := flags.contains "--no-field-notation" + coeExplicit := flags.contains "--coe-explicit" + analyze := flags.contains "--analyze" + showProofs := flags.contains "--show-proofs" } + pure (path, rawSorry, + flags.contains "--numeric-types", + flags.contains "--sanitize-context", + flags.contains "--analyze", + flags.contains "--assumption-holes", + sigFlags, + flags.contains "--expr-signature", + flags.contains "--abstract-proofs") + | [] => throw (IO.userError "Requires a path, optional JSON input, and optional --numeric-types, --sanitize-context, --analyze or --assumption-holes") + + let (fileMap, singleData) ← match ← findSorryTargetFromFile path rawSorry with + | .ok x => pure x + | .error e => throw (IO.userError e) + + singleData.ctx.runMetaM singleData.lctx do + MonadWithOptions.withOptions (Pp.extractionOptions numericTypes) do + let g ← mkFreshExprMVar singleData.type + let name ← getFreshConstName `mytheorem + let (header, application, levels) ← + Lean.Elab.Term.TermElabM.run' (mkThmHeader name g.mvarId! numericTypes sanitizeContext analyze sigFlags exprSignature abstractProofs) + let header := keepUsedSignatureLevelParams name levels (← header.toString) + if header.contains '⋯' then + throwError "Unsupported extracted goal: compact theorem signature contains omitted terms (⋯)" + let commandPositions := singleData.commandPositions.map fileMap.ofPosition + let commandPos := commandPositions.head! + let wrapperPrefix := + (commandPositions.zip (commandPositions.drop 1)).foldl + (fun text positions => + text ++ (String.fromUTF8! <| fileMap.source.toUTF8.extract positions.1.byteIdx positions.2.byteIdx)) "" + let «prefix» := String.fromUTF8! <| fileMap.source.toUTF8.extract 0 commandPos.byteIdx + return .ok («prefix» ++ "\n-- sorrydb-helper-start\n" ++ wrapperPrefix ++ + "theorem " ++ header ++ " := sorry" ++ + "\n-- sorrydb-application: " ++ (← renderApplication application assumptionHoles abstractProofs)) + +def main (args : List String) : IO UInt32 := do + -- Every failure, including refusals raised inside MetaM, is reported as + -- `{"error": ...}` so callers can rely on one output shape. + let res ← try extractGoal args catch e => pure (.error (toString e)) + let res := match res with + | .ok a => Json.mkObj [("ok", ToJson.toJson a)] + | .error e => Json.mkObj [("error", ToJson.toJson e)] + IO.println (toJson res) + return 0 diff --git a/lakefile.toml b/lakefile.toml index d66aed2..f66299c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,6 @@ name = "LeanUtils" version = "0.1.0" -defaultTargets = ["KernelCheck", "ExtractSorry"] +defaultTargets = ["KernelCheck", "ExtractSorry", "ExtractGoal"] testDriver = "LeanUtilsTest" [[lean_lib]] @@ -20,6 +20,11 @@ name = "ExtractSorry" root = "bins.ExtractSorry" supportInterpreter = true +[[lean_exe]] +name = "ExtractGoal" +root = "bins.ExtractGoal" +supportInterpreter = true + # `#guard_msgs` golden tests plus their fixture files. Building the fixtures is # what makes `findOLean` resolve their module names when a test re-elaborates them. [[lean_lib]] From 75f661e3d9dce18345b38fe3ad684f91212e8ac9 Mon Sep 17 00:00:00 2001 From: Mikhail Mayorov Date: Fri, 11 Sep 2026 15:52:48 +0400 Subject: [PATCH 5/5] README: document the flag combinations that have worked and their order Co-Authored-By: Claude Fable 5.1 --- README.md | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/README.md b/README.md index 645ae8a..a0c8726 100644 --- a/README.md +++ b/README.md @@ -114,6 +114,47 @@ elaborate. | `--show-proofs` | `pp.proofs := true` on the statement: proofs nested in data print instead of `⋯` (lossless by proof irrelevance) | | `--abstract-proofs` | hoist closed `Prop`-typed subterms of the goal into binders `sorrydb_prf_i`, `_` at the call site; only `Prop`s, so the statement stays equivalent | +### Flag combinations that have worked + +The flags are independent, but not every combination is meaningful, and the +useful ones form an escalation ladder: start compact, and add flags only when +the previous rendering failed to elaborate at the insertion point. This is the +order used to convert the SorryDB evaluation split (about 590 sorries across +~100 projects); the last column says how often each rung was the first one to +succeed there. + +| rung | flags | fixes | share | +|---|---|---|---| +| 1 | *(none)* | — | ~94% | +| 2 | `--sanitize-context` | context polluted by `let`s, `sorryAx`-tainted or inaccessible locals | ~5% | +| 3 | `--analyze` | call site fails with *don't know how to synthesize implicit argument* | <1% | +| 4 | `--analyze --assumption-holes` | the call has `?_` holes for inaccessible locals | <1% | +| 5 | `--analyze --expr-signature --no-fun-binder-types --no-field-notation` | statement fails to elaborate: forced `fun (a : T) ↦` ascriptions, `X.f` resolving to the wrong constant | <1% | +| 6 | rung 5 `+ --no-coercion-types` | `⇑f : A → B` ascriptions losing the bundled hom's implicits | rare | +| 7 | `--analyze --expr-signature --coe-explicit` | typeclass problem stuck on a coercion | rare | +| 8 | rung 5 `+ --numeric-types` | numerals defaulting to the wrong type (`-1` becoming `ℤ`) | rare | +| 9 | rung 5 `+ --show-proofs` | *omitted terms (⋯)*: a proof nested in a data value | rare | +| 10 | `--analyze --abstract-proofs`, optionally with the rung-5 flags or `--show-proofs` | *omitted terms* or *depends on an earlier sorry* where the offending subterm is a closed `Prop` | rare | + +Notes: + +* Rungs 5–10 need `--expr-signature`: the default signature printer works on + the bare constant, so `pp.*` flags and `pp.analyze` have nothing to act on + there. `--coe-explicit` switches `pp.analyze` on by itself. +* `--assumption-holes` and `--abstract-proofs` only matter when the call + contains `?_`; the first substitutes `(by assumption)`, the second `_`, + which unification fills with the original proof. +* Later rungs often render the same text as an earlier one (e.g. `--analyze` + changes nothing when no implicit needs naming). Comparing renderings before + compiling avoids paying for a duplicate. +* Rung 9 is the one that recovers most *omitted terms* refusals; fully + explicit printing (`pp.all`) recovers no more than it does and produces + statements 2–35× larger, so it is not offered as a flag. +* When one token closes several goals, the application closes only the goal + the record names. The caller has to keep the siblings as sorries, e.g. by + splicing `first | exact | sorry`; that is a splice decision, + not a rendering flag. + ## KernelCheck Elaborates the term against the goal in the sorry's own local context, rejects