diff --git a/LeanUtils/ExtractSorry.lean b/LeanUtils/ExtractSorry.lean
index 9760732..96ab4ea 100644
--- a/LeanUtils/ExtractSorry.lean
+++ b/LeanUtils/ExtractSorry.lean
@@ -36,8 +36,30 @@ 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
+  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
@@ -45,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/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 "<no mvar decl>"
+              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/LeanUtils/Utils.lean b/LeanUtils/Utils.lean
index 8aa01d1..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
@@ -131,7 +153,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 +176,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)
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 <file> <ParsedSorry json> [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/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/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 <file> <ParsedSorry json> <proof term>` 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/README.md b/README.md
index fb20642..a0c8726 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,173 @@
 # 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 <file>` | list every `sorry` in a file with its goal and position |
+| `KernelCheck <file> <sorry> <term>` | check a candidate proof term against the goal of one `sorry` |
+| `ExtractGoal <file> <sorry> [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 <application>` (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 |
+
+### 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 <application> | 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
+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 := <bundled>)` 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/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,
diff --git a/lakefile.toml b/lakefile.toml
index f0ffa21..f66299c 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,10 +1,16 @@
 name = "LeanUtils"
 version = "0.1.0"
-defaultTargets = ["KernelCheck", "ExtractSorry"]
+defaultTargets = ["KernelCheck", "ExtractSorry", "ExtractGoal"]
+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,15 @@ root = "bins.KernelCheck"
 [[lean_exe]]
 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]]
+name = "LeanUtilsTest"
+globs = ["LeanUtilsTest.+"]