From 860344f9c504d3c86d679ea9ef43e306e26a964e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Sep 2024 13:44:46 -0700
Subject: [PATCH 01/13] refactor: Factor out `FrontendM` driver

---
 Pantograph/Compile/Elab.lean     |  2 +-
 Pantograph/Compile/Frontend.lean | 16 +++++++++++-----
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Compile/Elab.lean
index 79833f3..2ded0f1 100644
--- a/Pantograph/Compile/Elab.lean
+++ b/Pantograph/Compile/Elab.lean
@@ -1,4 +1,4 @@
-
+/- Adapted from https://github.com/semorrison/lean-training-data -/
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Compile/Frontend.lean
index 3dbad85..640f5fa 100644
--- a/Pantograph/Compile/Frontend.lean
+++ b/Pantograph/Compile/Frontend.lean
@@ -29,6 +29,9 @@ end Lean.PersistentArray
 
 namespace Pantograph.Compile
 
+
+abbrev FrontendM := Elab.Frontend.FrontendM
+
 structure CompilationStep where
   fileName : String
   fileMap : FileMap
@@ -44,7 +47,7 @@ structure CompilationStep where
 Process one command, returning a `CompilationStep` and
 `done : Bool`, indicating whether this was the last command.
 -/
-def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
+def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
@@ -57,30 +60,33 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
   return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
-partial def processFile : Elab.Frontend.FrontendM (List CompilationStep) := do
+partial def collectCompilationSteps : FrontendM (List CompilationStep) := do
   let (cmd, done) ← processOneCommand
   if done then
     return [cmd]
   else
-    return cmd :: (← processFile)
+    return cmd :: (← collectCompilationSteps)
 
 
 def findSourcePath (module : Name) : IO System.FilePath := do
   return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
 
-def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do
+def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do
   let file ← IO.FS.readFile (← findSourcePath module)
   let inputCtx := Parser.mkInputContext file module.toString
 
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, messages) ← Elab.processHeader header opts messages inputCtx
   let commandState := Elab.Command.mkState env messages opts
-  processFile.run { inputCtx }
+  m.run { inputCtx }
     |>.run' {
     commandState := { commandState with infoState.enabled := true },
     parserState,
     cmdPos := parserState.pos
   }
 
+def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) :=
+  runFrontendMInFile module opts collectCompilationSteps
+
 
 end Pantograph.Compile

From 8e3241c02ab65660169cdcb436883e27bd81e2b6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Sep 2024 15:02:43 -0700
Subject: [PATCH 02/13] refactor: Move all frontend functions to `Frontend`

---
 Main.lean                                     |  2 +-
 Pantograph.lean                               |  2 +-
 Pantograph/Compile.lean                       | 25 ----------------
 Pantograph/Compile/Parse.lean                 | 14 ---------
 Pantograph/Condensed.lean                     |  1 -
 Pantograph/Frontend.lean                      |  4 +++
 .../Frontend.lean => Frontend/Basic.lean}     | 30 +++++++++++++------
 Pantograph/{Compile => Frontend}/Elab.lean    | 20 +++++++++++--
 Pantograph/Goal.lean                          | 18 -----------
 Pantograph/Library.lean                       | 20 +++++++++++--
 Pantograph/Protocol.lean                      |  5 ++--
 Pantograph/Serial.lean                        |  7 +++++
 Repl.lean                                     | 23 +++++++-------
 Test/Integration.lean                         |  4 +--
 14 files changed, 86 insertions(+), 89 deletions(-)
 delete mode 100644 Pantograph/Compile.lean
 delete mode 100644 Pantograph/Compile/Parse.lean
 create mode 100644 Pantograph/Frontend.lean
 rename Pantograph/{Compile/Frontend.lean => Frontend/Basic.lean} (78%)
 rename Pantograph/{Compile => Frontend}/Elab.lean (86%)

diff --git a/Main.lean b/Main.lean
index eb5240d..2959a64 100644
--- a/Main.lean
+++ b/Main.lean
@@ -7,7 +7,7 @@ import Pantograph
 import Repl
 
 -- Main IO functions
-open Pantograph
+open Pantograph.Repl
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Protocol.Command := do
diff --git a/Pantograph.lean b/Pantograph.lean
index 09327e8..292efb9 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -1,6 +1,6 @@
-import Pantograph.Compile
 import Pantograph.Condensed
 import Pantograph.Environment
+import Pantograph.Frontend
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
diff --git a/Pantograph/Compile.lean b/Pantograph/Compile.lean
deleted file mode 100644
index 83b463f..0000000
--- a/Pantograph/Compile.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-/- Adapted from lean-training-data by semorrison -/
-import Pantograph.Protocol
-import Pantograph.Compile.Frontend
-import Pantograph.Compile.Elab
-import Pantograph.Compile.Parse
-
-open Lean
-
-namespace Pantograph.Compile
-
-def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let infoTrees := steps.bind (·.trees)
-  let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ
-    | info@(.ofTacticInfo _) => info.isOriginal
-    | _ => false
-  let tactics := tacticInfoTrees.bind collectTactics
-  tactics.mapM λ invocation => do
-    let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
-    let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
-    let tactic ← invocation.ctx.runMetaM {} do
-      let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
-      return t.pretty
-    return { goalBefore, goalAfter, tactic }
-
-end Pantograph.Compile
diff --git a/Pantograph/Compile/Parse.lean b/Pantograph/Compile/Parse.lean
deleted file mode 100644
index 72eb620..0000000
--- a/Pantograph/Compile/Parse.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Compile
-
-def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
-  return Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := s)
-    (fileName := "<stdin>")
-
-end Pantograph.Compile
diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index c47f882..125b69c 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -2,7 +2,6 @@
 import Lean
 import Pantograph.Goal
 import Pantograph.Expr
-import Pantograph.Protocol
 
 open Lean
 
diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean
new file mode 100644
index 0000000..ffeeec5
--- /dev/null
+++ b/Pantograph/Frontend.lean
@@ -0,0 +1,4 @@
+/- Adapted from lean-training-data by semorrison -/
+import Pantograph.Protocol
+import Pantograph.Frontend.Basic
+import Pantograph.Frontend.Elab
diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Frontend/Basic.lean
similarity index 78%
rename from Pantograph/Compile/Frontend.lean
rename to Pantograph/Frontend/Basic.lean
index 640f5fa..55f8e93 100644
--- a/Pantograph/Compile/Frontend.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -27,8 +27,7 @@ protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :
 end Lean.PersistentArray
 
 
-namespace Pantograph.Compile
-
+namespace Pantograph.Frontend
 
 abbrev FrontendM := Elab.Frontend.FrontendM
 
@@ -47,6 +46,7 @@ structure CompilationStep where
 Process one command, returning a `CompilationStep` and
 `done : Bool`, indicating whether this was the last command.
 -/
+@[export pantograph_frontend_process_one_command_m]
 def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
@@ -67,26 +67,38 @@ partial def collectCompilationSteps : FrontendM (List CompilationStep) := do
   else
     return cmd :: (← collectCompilationSteps)
 
-
 def findSourcePath (module : Name) : IO System.FilePath := do
   return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
 
-def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do
+@[export pantograph_create_frontend_context_state_from_file_m]
+unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := {})
+  : IO (Elab.Frontend.Context × Elab.Frontend.State) := do
   let file ← IO.FS.readFile (← findSourcePath module)
   let inputCtx := Parser.mkInputContext file module.toString
 
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, messages) ← Elab.processHeader header opts messages inputCtx
   let commandState := Elab.Command.mkState env messages opts
-  m.run { inputCtx }
-    |>.run' {
+  let context: Elab.Frontend.Context := { inputCtx }
+  let state: Elab.Frontend.State := {
     commandState := { commandState with infoState.enabled := true },
     parserState,
     cmdPos := parserState.pos
   }
+  return (context, state)
 
-def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) :=
-  runFrontendMInFile module opts collectCompilationSteps
+partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
+  let (cmd, done) ← processOneCommand
+  let result ← f cmd
+  if done then
+    return [result]
+  else
+    return result :: (← mapCompilationSteps f)
+
+def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do
+  let (context, state) ← createFrontendContextStateFromFile module opts
+  m.run context |>.run' state
 
 
-end Pantograph.Compile
+
+end Pantograph.Frontend
diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Frontend/Elab.lean
similarity index 86%
rename from Pantograph/Compile/Elab.lean
rename to Pantograph/Frontend/Elab.lean
index 2ded0f1..e29d8f9 100644
--- a/Pantograph/Compile/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -3,7 +3,8 @@ import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
 
-import Pantograph.Compile.Frontend
+import Pantograph.Protocol
+import Pantograph.Frontend.Basic
 
 open Lean
 
@@ -75,7 +76,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
 end Lean.Elab.InfoTree
 
 
-namespace Pantograph.Compile
+namespace Pantograph.Frontend
 
 -- Info tree filtering functions
 
@@ -142,5 +143,18 @@ def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
 def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
   collectTacticNodes t |>.filter fun i => i.info.isSubstantive
 
+@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
+def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
+  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
+    | info@(.ofTacticInfo _) => info.isOriginal
+    | _ => false
+  let tactics := tacticInfoTrees.bind collectTactics
+  tactics.mapM λ invocation => do
+    let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
+    let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
+    let tactic ← invocation.ctx.runMetaM {} do
+      let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      return t.pretty
+    return { goalBefore, goalAfter, tactic }
 
-end Pantograph.Compile
+end Pantograph.Frontend
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index f248923..b4a6fc7 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -3,9 +3,7 @@ Functions for handling metavariables
 
 All the functions starting with `try` resume their inner monadic state.
 -/
-import Pantograph.Protocol
 import Pantograph.Tactic
-import Pantograph.Compile.Parse
 import Lean
 
 
@@ -385,20 +383,4 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-
-protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
-      Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let recursor ← match (← Compile.parseTermM recursor) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
-protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
-      Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let eq ← match (← Compile.parseTermM eq) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-
 end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 2f31042..23a2046 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -159,7 +159,7 @@ def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticRes
   runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
 protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
-  let type ← match (← Compile.parseTermM type) with
+  let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   runTermElabM do
@@ -167,12 +167,28 @@ protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: S
     state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
 protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
-  let expr ← match (← Compile.parseTermM expr) with
+  let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   runTermElabM do
     state.restoreElabM
     state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
+@[export pantograph_goal_try_motivated_apply_m]
+protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match (← parseTermM recursor) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
+@[export pantograph_goal_try_no_confuse_m]
+protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let eq ← match (← parseTermM eq) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goal binderName type
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 223fcfe..74da216 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -286,8 +286,6 @@ structure GoalDiag where
 /-- Executes the Lean compiler on a single file -/
 structure CompileUnit where
   module: String
-  -- If set to true, query the string boundaries of compilation units
-  compilationUnits: Bool := false
   -- If set to true, collect tactic invocations
   invocations: Bool := false
   deriving Lean.FromJson
@@ -297,7 +295,8 @@ structure InvokedTactic where
   tactic: String
   deriving Lean.ToJson
 structure CompileUnitResult where
-  units?: Option $ List (Nat × Nat)
+  -- String boundaries of compilation units
+  units: List (Nat × Nat)
   invocations?: Option $ List InvokedTactic
   deriving Lean.ToJson
 
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 93dfb95..3a9efa4 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -26,6 +26,13 @@ def parseTerm (env: Environment) (s: String): Except String Syntax :=
     (input := s)
     (fileName := "<stdin>")
 
+def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
+  return Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
 /-- Parse a syntax object. May generate additional metavariables! -/
 def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
   try
diff --git a/Repl.lean b/Repl.lean
index ef77d56..cd5bfe7 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -1,7 +1,7 @@
 import Lean.Data.HashMap
 import Pantograph
 
-namespace Pantograph
+namespace Pantograph.Repl
 
 structure Context where
   imports: List String
@@ -204,17 +204,20 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
     let module := args.module.toName
     try
-      let steps ← Compile.processSource module
-      let units? := if args.compilationUnits then
-          .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+      let li ← Frontend.runFrontendMInFile module {} <| Frontend.mapCompilationSteps λ step => do
+        let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+        let tacticInvocations ← if args.invocations then
+            Frontend.collectTacticsFromCompilationStep step
+          else
+            pure []
+        return (unitBoundary, tacticInvocations)
+      let units := li.map λ (unit, _) => unit
+      let invocations? := if args.invocations then
+          .some $ li.bind λ (_, invocations) => invocations
         else
           .none
-      let invocations? ← if args.invocations then
-          pure $ .some (← Compile.collectTacticsFromCompilation steps)
-        else
-          pure .none
-      return .ok { units?, invocations? }
+      return .ok { units, invocations? }
     catch e =>
       return .error $ errorI "compile" (← e.toMessageData.toString)
 
-end Pantograph
+end Pantograph.Repl
diff --git a/Test/Integration.lean b/Test/Integration.lean
index b82962b..e9eec76 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -6,13 +6,13 @@ import Repl
 import Test.Common
 
 namespace Pantograph.Test.Integration
-open Pantograph
+open Pantograph.Repl
 
 def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
     (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
   let payload := Lean.Json.mkObj payload
   let name := name?.getD s!"{cmd} {payload.compress}"
-  let result ← execute { cmd, payload }
+  let result ← Repl.execute { cmd, payload }
   return LSpec.test name (toString result = toString (Lean.toJson expected))
 
 abbrev Test := List (MainM LSpec.TestSeq)

From 08fb53c0209a27fcfce95d738ab896e92b382625 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 10:18:20 -0700
Subject: [PATCH 03/13] test: Frontend process testing

---
 Pantograph/Frontend/Basic.lean | 55 +++++++++++++++++++---------------
 Pantograph/Protocol.lean       | 12 +++++---
 Repl.lean                      | 23 ++++++++++----
 Test/Integration.lean          | 33 ++++++++++++++++++++
 4 files changed, 90 insertions(+), 33 deletions(-)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 55f8e93..79d3ea1 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -60,24 +60,45 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
   return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
-partial def collectCompilationSteps : FrontendM (List CompilationStep) := do
+partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand
   if done then
-    return [cmd]
+    if cmd.src.isEmpty then
+      return []
+    else
+      return [← f cmd]
   else
-    return cmd :: (← collectCompilationSteps)
+    return (← f cmd) :: (← mapCompilationSteps f)
 
+
+@[export pantograph_frontend_find_source_path_m]
 def findSourcePath (module : Name) : IO System.FilePath := do
   return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
 
-@[export pantograph_create_frontend_context_state_from_file_m]
-unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options := {})
-  : IO (Elab.Frontend.Context × Elab.Frontend.State) := do
-  let file ← IO.FS.readFile (← findSourcePath module)
-  let inputCtx := Parser.mkInputContext file module.toString
+/--
+Use with
+```lean
+let m: FrontendM α := ...
+let (context, state) ← createContextStateFromFile ...
+m.run context |>.run' state
+```
+-/
+@[export pantograph_frontend_create_context_state_from_file_m]
+def createContextStateFromFile
+    (file : String) -- Content of the file
+    (fileName : String := "<anonymous>")
+    (env? : Option Lean.Environment := .none) -- If set to true, assume there's no header.
+    (opts : Options := {})
+    : IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do
+  --let file ← IO.FS.readFile (← findSourcePath module)
+  let inputCtx := Parser.mkInputContext file fileName
 
-  let (header, parserState, messages) ← Parser.parseHeader inputCtx
-  let (env, messages) ← Elab.processHeader header opts messages inputCtx
+  let (env, parserState, messages) ← match env? with
+    | .some env => pure (env, {}, .empty)
+    | .none =>
+      let (header, parserState, messages) ← Parser.parseHeader inputCtx
+      let (env, messages) ← Elab.processHeader header opts messages inputCtx
+      pure (env, parserState, messages)
   let commandState := Elab.Command.mkState env messages opts
   let context: Elab.Frontend.Context := { inputCtx }
   let state: Elab.Frontend.State := {
@@ -87,18 +108,4 @@ unsafe def createFrontendContextStateFromFile (module : Name) (opts : Options :=
   }
   return (context, state)
 
-partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
-  let (cmd, done) ← processOneCommand
-  let result ← f cmd
-  if done then
-    return [result]
-  else
-    return result :: (← mapCompilationSteps f)
-
-def runFrontendMInFile { α } (module : Name) (opts : Options := {}) (m : FrontendM α): IO α := unsafe do
-  let (context, state) ← createFrontendContextStateFromFile module opts
-  m.run context |>.run' state
-
-
-
 end Pantograph.Frontend
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 74da216..12a75a2 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -284,20 +284,24 @@ structure GoalDiag where
 
 
 /-- Executes the Lean compiler on a single file -/
-structure CompileUnit where
-  module: String
+structure FrontendProcess where
+  -- One of these two must be supplied: Either supply the file name or the content.
+  fileName?: Option String := .none
+  file?: Option String := .none
   -- If set to true, collect tactic invocations
   invocations: Bool := false
+  -- If set to true, collect `sorry`s
+  sorrys: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
   goalAfter: String
   tactic: String
   deriving Lean.ToJson
-structure CompileUnitResult where
+structure FrontendProcessResult where
   -- String boundaries of compilation units
   units: List (Nat × Nat)
-  invocations?: Option $ List InvokedTactic
+  invocations?: Option (List InvokedTactic) := .none
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α
diff --git a/Repl.lean b/Repl.lean
index cd5bfe7..2f92eb8 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -46,7 +46,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   | "goal.continue" => run goal_continue
   | "goal.delete"   => run goal_delete
   | "goal.print"    => run goal_print
-  | "compile.unit"  => run compile_unit
+  | "frontend.process"  => run frontend_process
   | cmd =>
     let error: Protocol.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
@@ -201,16 +201,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
     let result ← runMetaInMainM <| goalPrint goalState state.options
     return .ok result
-  compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
-    let module := args.module.toName
+  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
     try
-      let li ← Frontend.runFrontendMInFile module {} <| Frontend.mapCompilationSteps λ step => do
+      let (fileName, file) ← match args.fileName?, args.file? with
+        | .some fileName, .none => do
+          let file ← IO.FS.readFile fileName
+          pure (fileName, file)
+        | .none, .some file =>
+          pure ("<anonymous>", file)
+        | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+      let env?: Option Lean.Environment ← if args.fileName?.isSome then
+          pure .none
+        else do
+          let env ← Lean.MonadEnv.getEnv
+          pure <| .some env
+      let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+      let m := Frontend.mapCompilationSteps λ step => do
         let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
         let tacticInvocations ← if args.invocations then
             Frontend.collectTacticsFromCompilationStep step
           else
             pure []
         return (unitBoundary, tacticInvocations)
+      let li ← m.run context |>.run' state
       let units := li.map λ (unit, _) => unit
       let invocations? := if args.invocations then
           .some $ li.bind λ (_, invocations) => invocations
@@ -218,6 +231,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           .none
       return .ok { units, invocations? }
     catch e =>
-      return .error $ errorI "compile" (← e.toMessageData.toString)
+      return .error $ errorI "frontend" (← e.toMessageData.toString)
 
 end Pantograph.Repl
diff --git a/Test/Integration.lean b/Test/Integration.lean
index e9eec76..3681d4e 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -161,6 +161,38 @@ def test_env_add_inspect : Test :=
       Protocol.EnvInspectResult)
   ]
 
+example : ∀ (p: Prop), p → p := by
+  intro p h
+  exact h
+
+def test_frontend_process : Test :=
+  [
+    let file := "example : ∀ (p: Prop), p → p := by\n  intro p h\n  exact h"
+    let goal1 := "p : Prop\nh : p\n⊢ p"
+    step "frontend.process"
+      [
+        ("file", .str file),
+        ("invocations", .bool true),
+        ("sorrys", .bool false),
+      ]
+     ({
+       units := [(0, file.utf8ByteSize)],
+       invocations? := .some [
+         {
+           goalBefore := "⊢ ∀ (p : Prop), p → p",
+           goalAfter := goal1,
+           tactic := "intro p h",
+         },
+         {
+           goalBefore := goal1 ,
+           goalAfter := "",
+           tactic := "exact h",
+         },
+       ]
+    }: Protocol.FrontendProcessResult),
+  ]
+
+
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let context: Context := {
@@ -182,6 +214,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
     ("env.add env.inspect", test_env_add_inspect),
+    ("frontend.process", test_frontend_process),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

From 4f5950ed7878f17de50d9b535b3bd030f1965af8 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 12:26:46 -0700
Subject: [PATCH 04/13] feat: Convert holes to goals

---
 Pantograph/Frontend/Elab.lean | 29 ++++++++++++++++++++--
 Pantograph/Goal.lean          | 11 +++++++++
 Pantograph/Protocol.lean      |  1 +
 Repl.lean                     | 45 +++++++++++++++++++++++------------
 Test/Integration.lean         | 33 ++++++++++++++++++++++++-
 5 files changed, 101 insertions(+), 18 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index e29d8f9..8deac23 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -5,6 +5,7 @@ import Lean.Elab.InfoTree
 
 import Pantograph.Protocol
 import Pantograph.Frontend.Basic
+import Pantograph.Goal
 
 open Lean
 
@@ -132,7 +133,7 @@ partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pre
 
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
-def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
+private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
   let infos := findAllInfo t none fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
@@ -153,8 +154,32 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
     let tactic ← invocation.ctx.runMetaM {} do
-      let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
       return t.pretty
     return { goalBefore, goalAfter, tactic }
 
+private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo :=
+  let infos := findAllInfo t none fun i => match i with
+    | .ofTermInfo { expectedType?, expr, stx, .. } =>
+        expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
+    | _ => false
+  infos.filterMap fun p => match p with
+    | (.ofTermInfo i, _, _) => .some i
+    | _ => none
+
+@[export pantograph_frontend_collect_sorrys_m]
+def collectSorrys (step: CompilationStep) : List Elab.TermInfo :=
+  step.trees.bind collectSorrysInTree
+
+@[export pantograph_frontend_sorrys_to_goal_state]
+def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do
+  assert! !sorrys.isEmpty
+  let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do
+    let type := termInfo.expectedType?.get!
+    let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+    return mvar.mvarId!
+  GoalState.createFromMVars goals (root := { name := .anonymous })
+
+
+
 end Pantograph.Frontend
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index b4a6fc7..79e3004 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -46,6 +46,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
     savedState,
     parentMVar? := .none,
   }
+@[export pantograph_goal_state_create_from_mvars_m]
+protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {}
+  return {
+    root,
+    savedState,
+    parentMVar? := .none,
+  }
 @[export pantograph_goal_state_is_conv]
 protected def GoalState.isConv (state: GoalState): Bool :=
   state.convMVar?.isSome
@@ -143,6 +152,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
 
 @[export pantograph_goal_state_root_expr]
 protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+  if goalState.root.name == .anonymous then
+    .none
   let expr ← goalState.mctx.eAssignment.find? goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   if expr.hasExprMVar then
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 12a75a2..26cae09 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -302,6 +302,7 @@ structure FrontendProcessResult where
   -- String boundaries of compilation units
   units: List (Nat × Nat)
   invocations?: Option (List InvokedTactic) := .none
+  goalStates?: Option (List (Nat × Array Goal)) := .none
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α
diff --git a/Repl.lean b/Repl.lean
index 2f92eb8..1277e73 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -54,6 +54,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
+  newGoalState (goalState: GoalState) : MainM Nat := do
+    let state ← get
+    let stateId := state.nextId
+    set { state with
+      goalStates := state.goalStates.insert stateId goalState,
+      nextId := state.nextId + 1
+    }
+    return stateId
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -95,7 +103,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
     return .ok (← get).options
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
@@ -108,11 +115,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     match expr? with
     | .error error => return .error error
     | .ok goalState =>
-      let stateId := state.nextId
-      set { state with
-        goalStates := state.goalStates.insert stateId goalState,
-        nextId := state.nextId + 1
-      }
+      let stateId ← newGoalState goalState
       return .ok { stateId, root := goalState.root.name.toString }
   goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
     let state ← get
@@ -151,11 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
           pure result
         | false, _ => pure nextGoalState
-      let nextStateId := state.nextId
-      set { state with
-        goalStates := state.goalStates.insert state.nextId nextGoalState,
-        nextId := state.nextId + 1,
-      }
+      let nextStateId ← newGoalState nextGoalState
       let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return .ok {
         nextStateId? := .some nextStateId,
@@ -202,6 +201,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let result ← runMetaInMainM <| goalPrint goalState state.options
     return .ok result
   frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+    let options := (← get).options
     try
       let (fileName, file) ← match args.fileName?, args.file? with
         | .some fileName, .none => do
@@ -222,14 +222,29 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
             Frontend.collectTacticsFromCompilationStep step
           else
             pure []
-        return (unitBoundary, tacticInvocations)
+        let sorrys := if args.sorrys then
+            Frontend.collectSorrys step
+          else
+            []
+        return (unitBoundary, tacticInvocations, sorrys)
       let li ← m.run context |>.run' state
-      let units := li.map λ (unit, _) => unit
+      let units := li.map λ (unit, _, _) => unit
       let invocations? := if args.invocations then
-          .some $ li.bind λ (_, invocations) => invocations
+          .some $ li.bind λ (_, invocations, _) => invocations
         else
           .none
-      return .ok { units, invocations? }
+      let goalStates? ← if args.sorrys then do
+          let stateIds ← li.filterMapM λ (_, _, sorrys) => do
+            if sorrys.isEmpty then
+              return .none
+            let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
+            let stateId ← newGoalState goalState
+            let goals ← goalSerialize goalState options
+            return .some (stateId, goals)
+          pure $ .some stateIds
+        else
+          pure .none
+      return .ok { units, invocations?, goalStates? }
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 3681d4e..4a8e418 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -192,6 +192,36 @@ def test_frontend_process : Test :=
     }: Protocol.FrontendProcessResult),
   ]
 
+example : 1 + 2 = 3 := rfl
+example (p: Prop): p → p := by simp
+
+def test_frontend_process_sorry : Test :=
+  let solved := "example : 1 + 2 = 3 := rfl\n"
+  let withSorry := "example (p: Prop): p → p := sorry"
+  [
+    let file := s!"{solved}{withSorry}"
+    let goal1: Protocol.Goal := {
+      name := "_uniq.1",
+      target := { pp? := .some "p → p" },
+      vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}],
+    }
+    step "frontend.process"
+      [
+        ("file", .str file),
+        ("invocations", .bool false),
+        ("sorrys", .bool true),
+      ]
+     ({
+       units := [
+         (0, solved.utf8ByteSize),
+         (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
+       ],
+       goalStates? := [
+         (0, #[goal1]),
+       ]
+    }: Protocol.FrontendProcessResult),
+  ]
+
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
@@ -214,7 +244,8 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
     ("env.add env.inspect", test_env_add_inspect),
-    ("frontend.process", test_frontend_process),
+    ("frontend.process invocation", test_frontend_process),
+    ("frontend.process sorry", test_frontend_process_sorry),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

From 762a139e7800bc08bc27c2f6a9aa3ba8365fcf44 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 12:30:32 -0700
Subject: [PATCH 05/13] feat: Export frontend functions

---
 Pantograph/Frontend/Basic.lean | 1 +
 Pantograph/Frontend/Elab.lean  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 79d3ea1..933424c 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -8,6 +8,7 @@ namespace Lean.FileMap
 /-- Extract the range of a `Syntax` expressed as lines and columns. -/
 -- Extracted from the private declaration `Lean.Elab.formatStxRange`,
 -- in `Lean.Elab.InfoTree.Main`.
+@[export pantograph_frontend_stx_range]
 protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
   let pos    := stx.getPos?.getD 0
   let endPos := stx.getTailPos?.getD pos
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 8deac23..2ff9a2e 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -88,6 +88,7 @@ structure TacticInvocation where
 namespace TacticInvocation
 
 /-- Return the range of the tactic, as a pair of file positions. -/
+@[export pantograph_frontend_tactic_invocation_range]
 protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
 
 /-- Pretty print a tactic. -/

From 9f0de0957e54dbeaa94d06bbf0f4c5620429f817 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 12:39:32 -0700
Subject: [PATCH 06/13] doc: Update documentation for frontend command

---
 README.md | 74 ++++++++++++++++++++++++++++++-------------------------
 1 file changed, 41 insertions(+), 33 deletions(-)

diff --git a/README.md b/README.md
index 8bda1ef..27af323 100644
--- a/README.md
+++ b/README.md
@@ -9,30 +9,17 @@ examine the symbol list of a Lean project for machine learning.
 
 ## Installation
 
-For Nix based workflow, see below.
+For Nix users, run
+``` sh
+nix build .#{sharedLib,executable}
+```
+to build either the shared library or executable.
 
 Install `elan` and `lake`, and run
 ``` sh
 lake build
 ```
-This builds the executable in `.lake/build/bin/pantograph`.
-
-To use Pantograph in a project environment, setup the `LEAN_PATH` environment
-variable so it contains the library path of lean libraries. The libraries must
-be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
-the environment might be setup like this:
-
-``` sh
-LIB="../lib"
-LIB_MATHLIB="$LIB/mathlib4/lake-packages"
-export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
-
-LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
-```
-The `$LEAN_PATH` executable of any project can be extracted by
-``` sh
-lake env printenv LEAN_PATH
-```
+This builds the executable in `.lake/build/bin/pantograph-repl`.
 
 ## Executable Usage
 
@@ -90,10 +77,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
-  
+
   One particular option for interest for machine learning researchers is the automatic mode.
   `options.set { "automaticMode": true }`. This makes Pantograph act like
-  LeanDojo, with no resumption necessary to manage your goals.
+  gym, with no resumption necessary to manage your goals.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol
@@ -113,6 +100,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   - `{ "goals": <names> }`: Resume the given goals
 * `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
 * `goal.print {"stateId": <id>}"`: Print a goal state
+* `frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations:
+  <bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
+  either the tactic invocations (`"invocations": true`) or the sorrys into goal
+  states (`"sorrys": true`)
 
 ### Errors
 
@@ -129,6 +120,25 @@ Common error forms:
   input of another is broken. For example, attempting to query a symbol not
   existing in the library or indexing into a non-existent proof state.
 
+### Project Environment
+
+To use Pantograph in a project environment, setup the `LEAN_PATH` environment
+variable so it contains the library path of lean libraries. The libraries must
+be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
+the environment might be setup like this:
+
+``` sh
+LIB="../lib"
+LIB_MATHLIB="$LIB/mathlib4/lake-packages"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+
+LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
+```
+The `$LEAN_PATH` executable of any project can be extracted by
+``` sh
+lake env printenv LEAN_PATH
+```
+
 ### Troubleshooting
 
 If lean encounters stack overflow problems when printing catalog, execute this before running lean:
@@ -142,13 +152,22 @@ ulimit -s unlimited
 with `Pantograph` which mirrors the REPL commands above. It is recommended to
 call Pantograph via this FFI since it provides a tremendous speed up.
 
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`.
+
+Inject any project path via the `pantograph_init_search` function.
+
 ## Developing
 
 A Lean development shell is provided in the Nix flake.
 
 ### Testing
 
-The tests are based on `LSpec`. To run tests,
+The tests are based on `LSpec`. To run tests, use either
+``` sh
+nix flake check
+```
+or
 ``` sh
 lake test
 ```
@@ -157,14 +176,3 @@ You can run an individual test by specifying a prefix
 ``` sh
 lake test -- "Tactic/No Confuse"
 ```
-
-## Nix based workflow
-
-The included Nix flake provides build targets for `sharedLib` and `executable`.
-The executable can be used as-is, but linking against the shared library
-requires the presence of `lean-all`.
-
-To run tests:
-``` sh
-nix flake check
-```

From fe8b259e4f09817bf4b2df269d87e836d10155cf Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 17:37:59 -0700
Subject: [PATCH 07/13] feat: Set root when there's just one mvar

---
 Pantograph/Frontend/Elab.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 2ff9a2e..4d6afe4 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -179,7 +179,11 @@ def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do
     let type := termInfo.expectedType?.get!
     let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
     return mvar.mvarId!
-  GoalState.createFromMVars goals (root := { name := .anonymous })
+  let root := match goals with
+    | [] => panic! "This function cannot be called on an empty list"
+    | [g] => g
+    | _ => { name := .anonymous }
+  GoalState.createFromMVars goals root
 
 
 

From bec84f857bd4f80064213fa5646bef4699191290 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Sep 2024 18:43:34 -0700
Subject: [PATCH 08/13] fix: repl build failure

---
 Main.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Main.lean b/Main.lean
index 2959a64..b866711 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,16 +1,15 @@
 import Lean.Data.Json
 import Lean.Environment
 
-import Pantograph.Version
-import Pantograph.Library
 import Pantograph
 import Repl
 
 -- Main IO functions
 open Pantograph.Repl
+open Pantograph.Protocol
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parseCommand (s: String): Except String Protocol.Command := do
+def parseCommand (s: String): Except String Command := do
   let s := s.trim
   match s.get? 0 with
   | .some '{' => -- Parse in Json mode
@@ -30,7 +29,7 @@ partial def loop : MainM Unit := do
   if command.trim.length = 0 then return ()
   match parseCommand command with
   | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>
@@ -46,15 +45,15 @@ unsafe def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   -- Separate imports and options
   if args == ["--version"] then do
-    println! s!"{version}"
+    println! s!"{Pantograph.version}"
     return
 
-  initSearch ""
+  Pantograph.initSearch ""
 
   let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
-    |>.toArray |> createCoreContext
+    |>.toArray |> Pantograph.createCoreContext
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
-  let coreState ← createCoreState imports.toArray
+  let coreState ← Pantograph.createCoreState imports.toArray
   let context: Context := {
     imports
   }

From 18cd1d038819fbb9f8985648aaf3554049822b5e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 2 Oct 2024 22:22:20 -0700
Subject: [PATCH 09/13] fix: Extracting sorrys from sketches

---
 Pantograph/Frontend/Elab.lean | 96 +++++++++++++++++++++++++++++++----
 Test/Frontend.lean            | 55 ++++++++++++++++++++
 Test/Main.lean                |  2 +
 3 files changed, 142 insertions(+), 11 deletions(-)
 create mode 100644 Test/Frontend.lean

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 4d6afe4..ec86df3 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -159,26 +159,100 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
       return t.pretty
     return { goalBefore, goalAfter, tactic }
 
-private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.TermInfo :=
+private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info :=
   let infos := findAllInfo t none fun i => match i with
     | .ofTermInfo { expectedType?, expr, stx, .. } =>
-        expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
+      expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
+    | .ofTacticInfo { stx, .. } =>
+      -- The `sorry` term is distinct from the `sorry` tactic
+      stx.isOfKind `Lean.Parser.Tactic.tacticSorry
     | _ => false
-  infos.filterMap fun p => match p with
-    | (.ofTermInfo i, _, _) => .some i
-    | _ => none
+  infos.map fun (i, _, _) => i
 
+-- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : List Elab.TermInfo :=
+def collectSorrys (step: CompilationStep) : List Elab.Info :=
   step.trees.bind collectSorrysInTree
 
-@[export pantograph_frontend_sorrys_to_goal_state]
-def sorrysToGoalState (sorrys : List Elab.TermInfo) : MetaM GoalState := do
-  assert! !sorrys.isEmpty
-  let goals ← sorrys.mapM λ termInfo => Meta.withLCtx termInfo.lctx #[] do
+
+namespace MetaTranslate
+
+structure Context where
+  sourceMCtx : MetavarContext := {}
+  sourceLCtx : LocalContext := {}
+
+/-
+Monadic state for translating a frozen meta state. The underlying `MetaM`
+operates in the "target" context and state.
+-/
+abbrev MetaTranslateM := ReaderT Context MetaM
+
+def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
+def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
+
+private def translateExpr (expr: Expr) : MetaTranslateM Expr := do
+  let (expr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) expr
+  return expr
+
+def translateLocalDecl (frozenLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
+  let fvarId ← mkFreshFVarId
+  match frozenLocalDecl with
+  | .cdecl index _ userName type bi kind =>
+    return .cdecl index fvarId userName type bi kind
+  | .ldecl index _ userName type value nonDep kind =>
+    return .ldecl index fvarId userName type value nonDep  kind
+
+def translateMVarId (mvarId: MVarId) : MetaTranslateM MVarId := do
+  let shadowDecl := (← getSourceMCtx).findDecl? mvarId |>.get!
+  let target ← translateExpr shadowDecl.type
+  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := shadowDecl.lctx }) do
+    let lctx ← MonadLCtx.getLCtx
+    let lctx ← (← getSourceLCtx).foldlM (λ lctx frozenLocalDecl => do
+        let localDecl ← translateLocalDecl frozenLocalDecl
+        let lctx := lctx.addDecl localDecl
+        pure lctx
+      ) lctx
+    withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
+      Meta.mkFreshExprSyntheticOpaqueMVar target
+  return mvar.mvarId!
+
+def translateTermInfo (termInfo: Elab.TermInfo) : MetaM MVarId := do
+  let trM : MetaTranslateM MVarId := do
     let type := termInfo.expectedType?.get!
-    let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+    let lctx ← getSourceLCtx
+    let mvar ← withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
+      Meta.mkFreshExprSyntheticOpaqueMVar type
     return mvar.mvarId!
+  trM.run { sourceLCtx := termInfo.lctx }
+
+
+def translateTacticInfoBefore (tacticInfo: Elab.TacticInfo) : MetaM (List MVarId) := do
+  let trM : MetaTranslateM (List MVarId) := do
+    tacticInfo.goalsBefore.mapM translateMVarId
+  trM.run { sourceMCtx := tacticInfo.mctxBefore }
+
+
+end MetaTranslate
+
+export MetaTranslate (MetaTranslateM)
+
+/--
+Since we cannot directly merge `MetavarContext`s, we have to get creative. This
+function duplicates frozen mvars in term and tactic info nodes, and add them to
+the current `MetavarContext`.
+-/
+@[export pantograph_frontend_sorrys_to_goal_state]
+def sorrysToGoalState (sorrys : List Elab.Info) : MetaM GoalState := do
+  assert! !sorrys.isEmpty
+  let goals ← sorrys.mapM λ info => Meta.withLCtx info.lctx #[] do
+    match info with
+    | .ofTermInfo termInfo  => do
+      let mvarId ← MetaTranslate.translateTermInfo termInfo
+      return [mvarId]
+    | .ofTacticInfo tacticInfo => do
+      MetaTranslate.translateTacticInfoBefore tacticInfo
+    | _ => panic! "Invalid info"
+  let goals := goals.bind id
   let root := match goals with
     | [] => panic! "This function cannot be called on an empty list"
     | [g] => g
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
new file mode 100644
index 0000000..ac347e6
--- /dev/null
+++ b/Test/Frontend.lean
@@ -0,0 +1,55 @@
+import LSpec
+import Pantograph
+import Repl
+import Test.Common
+
+open Lean Pantograph
+namespace Pantograph.Test.Frontend
+
+def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
+  let filename := "<anonymous>"
+  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
+  let m := Frontend.mapCompilationSteps λ step => do
+    return Frontend.collectSorrys step
+  let li ← m.run context |>.run' state
+  let goalStates ← li.filterMapM λ sorrys => do
+    if sorrys.isEmpty then
+      return .none
+    let goalState ← Frontend.sorrysToGoalState sorrys
+    return .some goalState
+  return goalStates
+
+def test_multiple_sorries_in_proof : TestT MetaM Unit := do
+  let sketch := "
+theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
+   have h_nat_add_succ: ∀ n m : Nat, n = m := sorry
+   sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! "Illegal number of states"
+  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})) = #[
+    {
+      name := "_uniq.1",
+      target := { pp? := "∀ (n m : Nat), n = m" },
+      vars := #[
+      ]
+    },
+    {
+      name := "_uniq.4",
+      target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
+      vars := #[{
+        name := "_uniq.3",
+        userName := "h_nat_add_succ",
+        type? := .some { pp? := "∀ (n m : Nat), n = m" },
+      }],
+    }
+  ])
+
+
+def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
+  let tests := [
+    ("multiple_sorrys_in_proof", test_multiple_sorries_in_proof),
+  ]
+  tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
+
+end Pantograph.Test.Frontend
diff --git a/Test/Main.lean b/Test/Main.lean
index 6da6640..0fde5fa 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -1,5 +1,6 @@
 import LSpec
 import Test.Environment
+import Test.Frontend
 import Test.Integration
 import Test.Library
 import Test.Metavar
@@ -44,6 +45,7 @@ def main (args: List String) := do
 
   let suites: List (String × List (String × IO LSpec.TestSeq)) := [
     ("Environment", Environment.suite),
+    ("Frontend", Frontend.suite env_default),
     ("Integration", Integration.suite env_default),
     ("Library", Library.suite env_default),
     ("Metavar", Metavar.suite env_default),

From 143cd289bbc4ea93f0889cf05737c3b6f90a51df Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 3 Oct 2024 01:29:46 -0700
Subject: [PATCH 10/13] fix: Extraction of sorry's from nested tactics

---
 Pantograph/Frontend/Elab.lean | 135 ++++++++++++++++++++++++----------
 Test/Frontend.lean            |  96 ++++++++++++++++++++++--
 Test/Integration.lean         |   4 +-
 3 files changed, 187 insertions(+), 48 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index ec86df3..2e0c14e 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -124,12 +124,12 @@ protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
 end TacticInvocation
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
     List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
   match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
   | .node i children  =>
-      (if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
+      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
@@ -159,7 +159,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
       return t.pretty
     return { goalBefore, goalAfter, tactic }
 
-private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info :=
+structure InfoWithContext where
+  info: Elab.Info
+  context?: Option Elab.ContextInfo := .none
+
+private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
   let infos := findAllInfo t none fun i => match i with
     | .ofTermInfo { expectedType?, expr, stx, .. } =>
       expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
@@ -167,11 +171,11 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List Elab.Info :=
       -- The `sorry` term is distinct from the `sorry` tactic
       stx.isOfKind `Lean.Parser.Tactic.tacticSorry
     | _ => false
-  infos.map fun (i, _, _) => i
+  infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : List Elab.Info :=
+def collectSorrys (step: CompilationStep) : List InfoWithContext :=
   step.trees.bind collectSorrysInTree
 
 
@@ -181,55 +185,106 @@ structure Context where
   sourceMCtx : MetavarContext := {}
   sourceLCtx : LocalContext := {}
 
+structure State where
+  -- Stores mapping from old to new mvar/fvars
+  mvarMap: HashMap MVarId MVarId := {}
+  fvarMap: HashMap FVarId FVarId := {}
+
 /-
 Monadic state for translating a frozen meta state. The underlying `MetaM`
 operates in the "target" context and state.
 -/
-abbrev MetaTranslateM := ReaderT Context MetaM
+abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
 
 def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
 def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
+def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
+  let state ← get
+  set { state with fvarMap := state.fvarMap.insert src dst }
+def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
+  let state ← get
+  set { state with mvarMap := state.mvarMap.insert src dst }
 
-private def translateExpr (expr: Expr) : MetaTranslateM Expr := do
-  let (expr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) expr
-  return expr
+def resetFVarMap : MetaTranslateM Unit := do
+  let state ← get
+  set { state with fvarMap := {} }
 
-def translateLocalDecl (frozenLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
+private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
+  let (srcExpr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) srcExpr
+  --IO.println s!"Transform src: {srcExpr}"
+  let result ← Core.transform srcExpr λ e => do
+    let state ← get
+    match e with
+    | .fvar fvarId =>
+      let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}"
+      return .done $ .fvar fvarId'
+    | .mvar mvarId => do
+      match state.mvarMap.find? mvarId with
+      | .some mvarId' => do
+        return .done $ .mvar mvarId'
+      | .none => do
+        --let t := (← getSourceMCtx).findDecl? mvarId |>.get!.type
+        --let t' ← translateExpr t
+        let mvar' ← Meta.mkFreshExprMVar .none
+        addTranslatedMVar mvarId mvar'.mvarId!
+        return .done mvar'
+    | _ => return .continue
+  try
+    Meta.check result
+  catch ex =>
+    panic! s!"Check failed: {← ex.toMessageData.toString}"
+  return result
+
+def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
   let fvarId ← mkFreshFVarId
-  match frozenLocalDecl with
-  | .cdecl index _ userName type bi kind =>
-    return .cdecl index fvarId userName type bi kind
-  | .ldecl index _ userName type value nonDep kind =>
-    return .ldecl index fvarId userName type value nonDep  kind
+  addTranslatedFVar srcLocalDecl.fvarId fvarId
+  match srcLocalDecl with
+  | .cdecl index _ userName type bi kind => do
+    --IO.println s!"[CD] {userName} {toString type}"
+    return .cdecl index fvarId userName (← translateExpr type) bi kind
+  | .ldecl index _ userName type value nonDep kind => do
+    --IO.println s!"[LD] {toString type} := {toString value}"
+    return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
 
-def translateMVarId (mvarId: MVarId) : MetaTranslateM MVarId := do
-  let shadowDecl := (← getSourceMCtx).findDecl? mvarId |>.get!
-  let target ← translateExpr shadowDecl.type
-  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := shadowDecl.lctx }) do
-    let lctx ← MonadLCtx.getLCtx
-    let lctx ← (← getSourceLCtx).foldlM (λ lctx frozenLocalDecl => do
-        let localDecl ← translateLocalDecl frozenLocalDecl
-        let lctx := lctx.addDecl localDecl
-        pure lctx
-      ) lctx
-    withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
-      Meta.mkFreshExprSyntheticOpaqueMVar target
+def translateLCtx : MetaTranslateM LocalContext := do
+  resetFVarMap
+  (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
+    let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl
+    pure $ lctx.addDecl localDecl
+  ) (← MonadLCtx.getLCtx)
+
+
+def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
+  let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
+  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
+    let lctx' ← translateLCtx
+    Meta.withLCtx lctx' #[] do
+      let target' ← translateExpr srcDecl.type
+      Meta.mkFreshExprSyntheticOpaqueMVar target'
+  addTranslatedMVar srcMVarId mvar.mvarId!
   return mvar.mvarId!
 
-def translateTermInfo (termInfo: Elab.TermInfo) : MetaM MVarId := do
+def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
+    : MetaM MVarId := do
   let trM : MetaTranslateM MVarId := do
     let type := termInfo.expectedType?.get!
-    let lctx ← getSourceLCtx
-    let mvar ← withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
-      Meta.mkFreshExprSyntheticOpaqueMVar type
+    let lctx' ← translateLCtx
+    let mvar ← Meta.withLCtx lctx' #[] do
+      let type' ← translateExpr type
+      Meta.mkFreshExprSyntheticOpaqueMVar type'
     return mvar.mvarId!
-  trM.run { sourceLCtx := termInfo.lctx }
+  trM.run {
+    sourceMCtx := context?.map (·.mctx) |>.getD {},
+    sourceLCtx := termInfo.lctx } |>.run' {}
 
 
-def translateTacticInfoBefore (tacticInfo: Elab.TacticInfo) : MetaM (List MVarId) := do
+def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
+    : MetaM (List MVarId) := do
   let trM : MetaTranslateM (List MVarId) := do
     tacticInfo.goalsBefore.mapM translateMVarId
-  trM.run { sourceMCtx := tacticInfo.mctxBefore }
+  trM.run {
+    sourceMCtx := tacticInfo.mctxBefore
+  } |>.run' {}
 
 
 end MetaTranslate
@@ -242,15 +297,15 @@ function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state]
-def sorrysToGoalState (sorrys : List Elab.Info) : MetaM GoalState := do
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   assert! !sorrys.isEmpty
-  let goals ← sorrys.mapM λ info => Meta.withLCtx info.lctx #[] do
-    match info with
+  let goals ← sorrys.mapM λ i => do
+    match i.info with
     | .ofTermInfo termInfo  => do
-      let mvarId ← MetaTranslate.translateTermInfo termInfo
+      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
       return [mvarId]
     | .ofTacticInfo tacticInfo => do
-      MetaTranslate.translateTacticInfoBefore tacticInfo
+      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
   let goals := goals.bind id
   let root := match goals with
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index ac347e6..c186503 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -19,7 +19,7 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
     return .some goalState
   return goalStates
 
-def test_multiple_sorries_in_proof : TestT MetaM Unit := do
+def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
   let sketch := "
 theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
    have h_nat_add_succ: ∀ n m : Nat, n = m := sorry
@@ -27,28 +27,112 @@ theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) +
   "
   let goalStates ← (collectSorrysFromSource sketch).run' {}
   let [goalState] := goalStates | panic! "Illegal number of states"
-  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})) = #[
+  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
     {
-      name := "_uniq.1",
       target := { pp? := "∀ (n m : Nat), n = m" },
       vars := #[
       ]
     },
     {
-      name := "_uniq.4",
       target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
       vars := #[{
-        name := "_uniq.3",
         userName := "h_nat_add_succ",
         type? := .some { pp? := "∀ (n m : Nat), n = m" },
       }],
     }
   ])
 
+def test_sorry_in_middle: TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (n m: Nat), n + m = m + n := by
+  intros n m
+  sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}"
+  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "n + m = m + n" },
+      vars := #[{
+           userName := "n",
+           type? := .some { pp? := "Nat" },
+        }, {
+           userName := "m",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    }
+  ])
+
+def test_sorry_in_induction : TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (n m: Nat), n + m = m + n := by
+  intros n m
+  induction n with
+  | zero =>
+    have h1 : 0 + m = m := sorry
+    sorry
+  | succ n ih =>
+    have h2 : n + m = m := sorry
+    sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}"
+  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "0 + m = m" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }]
+    },
+    {
+      target := { pp? := "0 + m = m + 0" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "h1",
+        type? := .some { pp? := "0 + m = m" },
+      }]
+    },
+    {
+      target := { pp? := "n + m = m" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "n",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "ih",
+        type? := .some { pp? := "n + m = m + n" },
+      }]
+    },
+    {
+      target := { pp? := "n + 1 + m = m + (n + 1)" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "n",
+        type? := .some { pp? := "Nat" },
+      }, {
+        userName := "ih",
+        type? := .some { pp? := "n + m = m + n" },
+      },  {
+        userName := "h2",
+        type? := .some { pp? := "n + m = m" },
+      }]
+    }
+  ])
+
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("multiple_sorrys_in_proof", test_multiple_sorries_in_proof),
+    ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
+    ("sorry_in_middle", test_sorry_in_middle),
+    ("sorry_in_induction", test_sorry_in_induction),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 4a8e418..b3d49fe 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -201,9 +201,9 @@ def test_frontend_process_sorry : Test :=
   [
     let file := s!"{solved}{withSorry}"
     let goal1: Protocol.Goal := {
-      name := "_uniq.1",
+      name := "_uniq.6",
       target := { pp? := .some "p → p" },
-      vars := #[{ name := "_uniq.168", userName := "p", type? := .some { pp? := .some "Prop" }}],
+      vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
       [

From 530a1a1a97273314bd7b01c542ce686a366aa0b9 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 3 Oct 2024 11:35:54 -0700
Subject: [PATCH 11/13] fix: Extracting `sorry`s from coupled goals

---
 Pantograph/Expr.lean                   |  87 ++++++++---------
 Pantograph/Frontend.lean               |   2 +-
 Pantograph/Frontend/Elab.lean          | 118 +---------------------
 Pantograph/Frontend/MetaTranslate.lean | 129 +++++++++++++++++++++++++
 Test/Frontend.lean                     |  49 ++++++++--
 5 files changed, 221 insertions(+), 164 deletions(-)
 create mode 100644 Pantograph/Frontend/MetaTranslate.lean

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index f989575..ad064a7 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -60,53 +60,54 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
       -- nested mvars.
       mvarId.setKind .syntheticOpaque
 
-      let lctx ← MonadLCtx.getLCtx
-      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
-        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
-          | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
-          | .none => acc) []
-        panic! s!"Local context variable violation: {violations}"
+      mvarId.withContext do
+        let lctx ← MonadLCtx.getLCtx
+        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+          let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
+            | .none => acc) []
+          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
 
-      if let .some assign ← getExprMVarAssignment? mvarId then
-        --IO.println s!"{padding}├A ?{mvarId.name}"
-        assert! !(← mvarId.isDelayedAssigned)
-        return .visit (mkAppN assign args)
-      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-        --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
-        --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+        if let .some assign ← getExprMVarAssignment? mvarId then
+          --IO.println s!"{padding}├A ?{mvarId.name}"
+          assert! !(← mvarId.isDelayedAssigned)
+          return .visit (mkAppN assign args)
+        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
 
-        if args.size < fvars.size then
-          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
-        --if !args.isEmpty then
-          --IO.println s!"{padding}├── Arguments Begin"
-        let args ← args.mapM self
-        --if !args.isEmpty then
-          --IO.println s!"{padding}├── Arguments End"
-        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
-          --IO.println s!"{padding}├T1"
-          let result := mkAppN f args
+          if args.size < fvars.size then
+            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+          --if !args.isEmpty then
+            --IO.println s!"{padding}├── Arguments Begin"
+          let args ← args.mapM self
+          --if !args.isEmpty then
+            --IO.println s!"{padding}├── Arguments End"
+          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+            --IO.println s!"{padding}├T1"
+            let result := mkAppN f args
+            return .done result
+
+          let pending ← mvarIdPending.withContext do
+            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
+            --IO.println s!"{padding}├Pre: {inner}"
+            pure <| (← inner.abstractM fvars).instantiateRev args
+
+          -- Tail arguments
+          let result := mkAppRange pending fvars.size args.size args
+          --IO.println s!"{padding}├MD {result}"
           return .done result
+        else
+          assert! !(← mvarId.isAssigned)
+          assert! !(← mvarId.isDelayedAssigned)
+          --if !args.isEmpty then
+          --  IO.println s!"{padding}├── Arguments Begin"
+          let args ← args.mapM self
+          --if !args.isEmpty then
+          --  IO.println s!"{padding}├── Arguments End"
 
-        let pending ← mvarIdPending.withContext do
-          let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
-          --IO.println s!"{padding}├Pre: {inner}"
-          pure <| (← inner.abstractM fvars).instantiateRev args
-
-        -- Tail arguments
-        let result := mkAppRange pending fvars.size args.size args
-        --IO.println s!"{padding}├MD {result}"
-        return .done result
-      else
-        assert! !(← mvarId.isAssigned)
-        assert! !(← mvarId.isDelayedAssigned)
-        --if !args.isEmpty then
-        --  IO.println s!"{padding}├── Arguments Begin"
-        let args ← args.mapM self
-        --if !args.isEmpty then
-        --  IO.println s!"{padding}├── Arguments End"
-
-        --IO.println s!"{padding}├M ?{mvarId.name}"
-        return .done (mkAppN f args))
+          --IO.println s!"{padding}├M ?{mvarId.name}"
+          return .done (mkAppN f args))
   --IO.println s!"{padding}└Result {result}"
   return result
   where
diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean
index ffeeec5..fd91823 100644
--- a/Pantograph/Frontend.lean
+++ b/Pantograph/Frontend.lean
@@ -1,4 +1,4 @@
 /- Adapted from lean-training-data by semorrison -/
-import Pantograph.Protocol
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.Elab
+import Pantograph.Frontend.MetaTranslate
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 2e0c14e..2036aea 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -3,9 +3,10 @@ import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
 
-import Pantograph.Protocol
 import Pantograph.Frontend.Basic
+import Pantograph.Frontend.MetaTranslate
 import Pantograph.Goal
+import Pantograph.Protocol
 
 open Lean
 
@@ -179,117 +180,6 @@ def collectSorrys (step: CompilationStep) : List InfoWithContext :=
   step.trees.bind collectSorrysInTree
 
 
-namespace MetaTranslate
-
-structure Context where
-  sourceMCtx : MetavarContext := {}
-  sourceLCtx : LocalContext := {}
-
-structure State where
-  -- Stores mapping from old to new mvar/fvars
-  mvarMap: HashMap MVarId MVarId := {}
-  fvarMap: HashMap FVarId FVarId := {}
-
-/-
-Monadic state for translating a frozen meta state. The underlying `MetaM`
-operates in the "target" context and state.
--/
-abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
-
-def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
-def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
-def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
-  let state ← get
-  set { state with fvarMap := state.fvarMap.insert src dst }
-def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
-  let state ← get
-  set { state with mvarMap := state.mvarMap.insert src dst }
-
-def resetFVarMap : MetaTranslateM Unit := do
-  let state ← get
-  set { state with fvarMap := {} }
-
-private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
-  let (srcExpr, _) := instantiateMVarsCore (mctx := ← getSourceMCtx) srcExpr
-  --IO.println s!"Transform src: {srcExpr}"
-  let result ← Core.transform srcExpr λ e => do
-    let state ← get
-    match e with
-    | .fvar fvarId =>
-      let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}"
-      return .done $ .fvar fvarId'
-    | .mvar mvarId => do
-      match state.mvarMap.find? mvarId with
-      | .some mvarId' => do
-        return .done $ .mvar mvarId'
-      | .none => do
-        --let t := (← getSourceMCtx).findDecl? mvarId |>.get!.type
-        --let t' ← translateExpr t
-        let mvar' ← Meta.mkFreshExprMVar .none
-        addTranslatedMVar mvarId mvar'.mvarId!
-        return .done mvar'
-    | _ => return .continue
-  try
-    Meta.check result
-  catch ex =>
-    panic! s!"Check failed: {← ex.toMessageData.toString}"
-  return result
-
-def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
-  let fvarId ← mkFreshFVarId
-  addTranslatedFVar srcLocalDecl.fvarId fvarId
-  match srcLocalDecl with
-  | .cdecl index _ userName type bi kind => do
-    --IO.println s!"[CD] {userName} {toString type}"
-    return .cdecl index fvarId userName (← translateExpr type) bi kind
-  | .ldecl index _ userName type value nonDep kind => do
-    --IO.println s!"[LD] {toString type} := {toString value}"
-    return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
-
-def translateLCtx : MetaTranslateM LocalContext := do
-  resetFVarMap
-  (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl
-    pure $ lctx.addDecl localDecl
-  ) (← MonadLCtx.getLCtx)
-
-
-def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
-  let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
-  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
-    let lctx' ← translateLCtx
-    Meta.withLCtx lctx' #[] do
-      let target' ← translateExpr srcDecl.type
-      Meta.mkFreshExprSyntheticOpaqueMVar target'
-  addTranslatedMVar srcMVarId mvar.mvarId!
-  return mvar.mvarId!
-
-def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
-    : MetaM MVarId := do
-  let trM : MetaTranslateM MVarId := do
-    let type := termInfo.expectedType?.get!
-    let lctx' ← translateLCtx
-    let mvar ← Meta.withLCtx lctx' #[] do
-      let type' ← translateExpr type
-      Meta.mkFreshExprSyntheticOpaqueMVar type'
-    return mvar.mvarId!
-  trM.run {
-    sourceMCtx := context?.map (·.mctx) |>.getD {},
-    sourceLCtx := termInfo.lctx } |>.run' {}
-
-
-def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
-    : MetaM (List MVarId) := do
-  let trM : MetaTranslateM (List MVarId) := do
-    tacticInfo.goalsBefore.mapM translateMVarId
-  trM.run {
-    sourceMCtx := tacticInfo.mctxBefore
-  } |>.run' {}
-
-
-end MetaTranslate
-
-export MetaTranslate (MetaTranslateM)
 
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
@@ -299,7 +189,7 @@ the current `MetavarContext`.
 @[export pantograph_frontend_sorrys_to_goal_state]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   assert! !sorrys.isEmpty
-  let goals ← sorrys.mapM λ i => do
+  let goalsM := sorrys.mapM λ i => do
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
@@ -307,7 +197,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
     | .ofTacticInfo tacticInfo => do
       MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
-  let goals := goals.bind id
+  let goals := (← goalsM.run {} |>.run' {}).bind id
   let root := match goals with
     | [] => panic! "This function cannot be called on an empty list"
     | [g] => g
diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
new file mode 100644
index 0000000..82f8dfc
--- /dev/null
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -0,0 +1,129 @@
+import Lean.Meta
+
+open Lean
+
+namespace Pantograph.Frontend
+
+namespace MetaTranslate
+
+structure Context where
+  sourceMCtx : MetavarContext := {}
+  sourceLCtx : LocalContext := {}
+
+abbrev FVarMap := HashMap FVarId FVarId
+
+structure State where
+  -- Stores mapping from old to new mvar/fvars
+  mvarMap: HashMap MVarId MVarId := {}
+  fvarMap: HashMap FVarId FVarId := {}
+
+/-
+Monadic state for translating a frozen meta state. The underlying `MetaM`
+operates in the "target" context and state.
+-/
+abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
+
+def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
+def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
+def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := state.fvarMap.insert src dst })
+def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with mvarMap := state.mvarMap.insert src dst })
+
+def saveFVarMap : MetaTranslateM FVarMap := do
+  return (← get).fvarMap
+def restoreFVarMap (map: FVarMap) : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := map })
+def resetFVarMap : MetaTranslateM Unit := do
+  modifyGet λ state => ((), { state with fvarMap := {} })
+
+mutual
+private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
+  let sourceMCtx ← getSourceMCtx
+  let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
+  --IO.println s!"Transform src: {srcExpr}"
+  let result ← Core.transform srcExpr λ e => do
+    let state ← get
+    match e with
+    | .fvar fvarId =>
+      let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}"
+      assert! (← getLCtx).contains fvarId'
+      return .done $ .fvar fvarId'
+    | .mvar mvarId => do
+      assert! !(sourceMCtx.dAssignment.contains mvarId)
+      assert! !(sourceMCtx.eAssignment.contains mvarId)
+      match state.mvarMap.find? mvarId with
+      | .some mvarId' => do
+        return .done $ .mvar mvarId'
+      | .none => do
+        -- Entering another LCtx, must save the current one
+        let fvarMap ← saveFVarMap
+        let mvarId' ← translateMVarId mvarId
+        restoreFVarMap fvarMap
+        return .done $ .mvar mvarId'
+    | _ => return .continue
+  Meta.check result
+  return result
+
+partial def translateLocalInstance (srcInstance: LocalInstance) : MetaTranslateM LocalInstance := do
+  return {
+    className := srcInstance.className,
+    fvar := ← translateExpr srcInstance.fvar
+  }
+partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
+  let fvarId ← mkFreshFVarId
+  addTranslatedFVar srcLocalDecl.fvarId fvarId
+  match srcLocalDecl with
+  | .cdecl index _ userName type bi kind => do
+    --IO.println s!"[CD] {userName} {toString type}"
+    return .cdecl index fvarId userName (← translateExpr type) bi kind
+  | .ldecl index _ userName type value nonDep kind => do
+    --IO.println s!"[LD] {toString type} := {toString value}"
+    return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
+
+partial def translateLCtx : MetaTranslateM LocalContext := do
+  resetFVarMap
+  (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
+    let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl
+    pure $ lctx.addDecl localDecl
+  ) (← MonadLCtx.getLCtx)
+
+partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
+  if let .some mvarId' := (← get).mvarMap.find? srcMVarId then
+    return mvarId'
+  let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
+  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
+    let lctx' ← translateLCtx
+    let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
+    Meta.withLCtx lctx' localInstances' do
+      let target' ← translateExpr srcDecl.type
+      Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
+  addTranslatedMVar srcMVarId mvar.mvarId!
+  return mvar.mvarId!
+end
+
+def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
+    : MetaTranslateM MVarId := do
+  withTheReader Context (λ ctx => { ctx with
+    sourceMCtx := context?.map (·.mctx) |>.getD {},
+    sourceLCtx := termInfo.lctx,
+  }) do
+    let type := termInfo.expectedType?.get!
+    let lctx' ← translateLCtx
+    let mvar ← Meta.withLCtx lctx' #[] do
+      let type' ← translateExpr type
+      Meta.mkFreshExprSyntheticOpaqueMVar type'
+    return mvar.mvarId!
+
+
+def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
+    : MetaTranslateM (List MVarId) := do
+  withTheReader Context (λ ctx => { ctx with sourceMCtx := tacticInfo.mctxBefore }) do
+    tacticInfo.goalsBefore.mapM translateMVarId
+
+
+end MetaTranslate
+
+export MetaTranslate (MetaTranslateM)
+
+end Pantograph.Frontend
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index c186503..b09ef81 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -26,8 +26,8 @@ theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) +
    sorry
   "
   let goalStates ← (collectSorrysFromSource sketch).run' {}
-  let [goalState] := goalStates | panic! "Illegal number of states"
-  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+  let [goalState] := goalStates | panic! "Incorrect number of states"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
     {
       target := { pp? := "∀ (n m : Nat), n = m" },
       vars := #[
@@ -49,8 +49,8 @@ example : ∀ (n m: Nat), n + m = m + n := by
   sorry
   "
   let goalStates ← (collectSorrysFromSource sketch).run' {}
-  let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}"
-  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
     {
       target := { pp? := "n + m = m + n" },
       vars := #[{
@@ -77,8 +77,8 @@ example : ∀ (n m: Nat), n + m = m + n := by
     sorry
   "
   let goalStates ← (collectSorrysFromSource sketch).run' {}
-  let [goalState] := goalStates | panic! s!"Illegal number of states: {goalStates.length}"
-  addTest $ LSpec.check "plus_n_Sm" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
     {
       target := { pp? := "0 + m = m" },
       vars := #[{
@@ -87,6 +87,7 @@ example : ∀ (n m: Nat), n + m = m + n := by
       }]
     },
     {
+      userName? := .some "zero",
       target := { pp? := "0 + m = m + 0" },
       vars := #[{
         userName := "m",
@@ -110,6 +111,7 @@ example : ∀ (n m: Nat), n + m = m + n := by
       }]
     },
     {
+      userName? := .some "succ",
       target := { pp? := "n + 1 + m = m + (n + 1)" },
       vars := #[{
         userName := "m",
@@ -127,12 +129,47 @@ example : ∀ (n m: Nat), n + m = m + n := by
     }
   ])
 
+def test_sorry_in_coupled: TestT MetaM Unit := do
+  let sketch := "
+example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
+  intro y
+  apply Exists.intro
+  case h => sorry
+  case w => sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "y + 1 = ?w" },
+      vars := #[{
+           userName := "y",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    },
+    {
+      userName? := .some "w",
+      target := { pp? := "Nat" },
+      vars := #[{
+           userName := "y✝",
+           isInaccessible := true,
+           type? := .some { pp? := "Nat" },
+        }, {
+           userName := "y",
+           type? := .some { pp? := "Nat" },
+        }
+      ],
+    }
+  ])
+
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
     ("sorry_in_middle", test_sorry_in_middle),
     ("sorry_in_induction", test_sorry_in_induction),
+    ("sorry_in_coupled", test_sorry_in_coupled),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

From a03eeddc9bea63caf91b20bdbbbd4cf9e5133b79 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 3 Oct 2024 11:46:09 -0700
Subject: [PATCH 12/13] fix: Variable duplication in nested translation

---
 Pantograph/Frontend/MetaTranslate.lean | 22 +++++++++++++---------
 Test/Frontend.lean                     |  4 ----
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
index 82f8dfc..1a12029 100644
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -83,21 +83,25 @@ partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalD
 
 partial def translateLCtx : MetaTranslateM LocalContext := do
   resetFVarMap
+  let lctx ← MonadLCtx.getLCtx
+  assert! lctx.isEmpty
   (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do translateLocalDecl srcLocalDecl
+    let localDecl ← Meta.withLCtx lctx #[] do
+      translateLocalDecl srcLocalDecl
     pure $ lctx.addDecl localDecl
-  ) (← MonadLCtx.getLCtx)
+  ) lctx
 
 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
   if let .some mvarId' := (← get).mvarMap.find? srcMVarId then
     return mvarId'
-  let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
-  let mvar ← withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
-    let lctx' ← translateLCtx
-    let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
-    Meta.withLCtx lctx' localInstances' do
-      let target' ← translateExpr srcDecl.type
-      Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
+  let mvar ← Meta.withLCtx .empty #[] do
+    let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
+    withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
+      let lctx' ← translateLCtx
+      let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
+      Meta.withLCtx lctx' localInstances' do
+        let target' ← translateExpr srcDecl.type
+        Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
   addTranslatedMVar srcMVarId mvar.mvarId!
   return mvar.mvarId!
 end
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index b09ef81..68d961b 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -152,10 +152,6 @@ example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
       userName? := .some "w",
       target := { pp? := "Nat" },
       vars := #[{
-           userName := "y✝",
-           isInaccessible := true,
-           type? := .some { pp? := "Nat" },
-        }, {
            userName := "y",
            type? := .some { pp? := "Nat" },
         }

From d0321e72ddb477a5eea1ebee346c5ee00512d22e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 5 Oct 2024 14:49:17 -0700
Subject: [PATCH 13/13] feat: Add message diagnostics to frontend.process

---
 Pantograph/Frontend/Basic.lean |  8 +++++++
 Pantograph/Protocol.lean       | 13 +++++++---
 Repl.lean                      | 43 +++++++++++++++++-----------------
 Test/Integration.lean          | 43 ++++++++++++++++++----------------
 4 files changed, 63 insertions(+), 44 deletions(-)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 933424c..1074a94 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -42,6 +42,14 @@ structure CompilationStep where
   msgs : List Message
   trees : List Elab.InfoTree
 
+namespace CompilationStep
+
+@[export pantograph_frontend_compilation_step_message_strings_m]
+def messageStrings (step: CompilationStep) : IO (Array String) := do
+  List.toArray <$> step.msgs.mapM (·.toString)
+
+end CompilationStep
+
 
 /--
 Process one command, returning a `CompilationStep` and
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index abfeede..acc2681 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -298,11 +298,18 @@ structure InvokedTactic where
   goalAfter: String
   tactic: String
   deriving Lean.ToJson
-structure FrontendProcessResult where
+
+structure CompilationUnit where
   -- String boundaries of compilation units
-  units: List (Nat × Nat)
+  boundary: (Nat × Nat)
+  -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
-  goalStates?: Option (List (Nat × Array Goal)) := .none
+  goalStateId?: Option Nat := .none
+  goals: Array Goal := #[]
+  messages: Array String := #[]
+  deriving Lean.ToJson
+structure FrontendProcessResult where
+  units: List CompilationUnit
   deriving Lean.ToJson
 
 abbrev CR α := Except InteractionError α
diff --git a/Repl.lean b/Repl.lean
index 1277e73..7597164 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -216,35 +216,36 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           let env ← Lean.MonadEnv.getEnv
           pure <| .some env
       let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-      let m := Frontend.mapCompilationSteps λ step => do
-        let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        let tacticInvocations ← if args.invocations then
-            Frontend.collectTacticsFromCompilationStep step
+      let frontendM := Frontend.mapCompilationSteps λ step => do
+        let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
+        let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
+            let invocations ← Frontend.collectTacticsFromCompilationStep step
+            pure $ .some invocations
           else
-            pure []
+            pure .none
         let sorrys := if args.sorrys then
             Frontend.collectSorrys step
           else
             []
-        return (unitBoundary, tacticInvocations, sorrys)
-      let li ← m.run context |>.run' state
-      let units := li.map λ (unit, _, _) => unit
-      let invocations? := if args.invocations then
-          .some $ li.bind λ (_, invocations, _) => invocations
-        else
-          .none
-      let goalStates? ← if args.sorrys then do
-          let stateIds ← li.filterMapM λ (_, _, sorrys) => do
-            if sorrys.isEmpty then
-              return .none
+        let messages ← step.messageStrings
+        return (boundary, invocations?, sorrys, messages)
+      let li ← frontendM.run context |>.run' state
+      let units ← li.mapM λ (boundary, invocations?, sorrys, messages) => do
+        let (goalStateId?, goals) ← if sorrys.isEmpty then do
+            pure (.none, #[])
+          else do
             let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState goalState
             let goals ← goalSerialize goalState options
-            return .some (stateId, goals)
-          pure $ .some stateIds
-        else
-          pure .none
-      return .ok { units, invocations?, goalStates? }
+            pure (.some stateId, goals)
+        return {
+          boundary,
+          invocations?,
+          goalStateId?,
+          goals,
+          messages,
+        }
+      return .ok { units }
     catch e =>
       return .error $ errorI "frontend" (← e.toMessageData.toString)
 
diff --git a/Test/Integration.lean b/Test/Integration.lean
index b3d49fe..413ed1c 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -176,19 +176,21 @@ def test_frontend_process : Test :=
         ("sorrys", .bool false),
       ]
      ({
-       units := [(0, file.utf8ByteSize)],
-       invocations? := .some [
-         {
-           goalBefore := "⊢ ∀ (p : Prop), p → p",
-           goalAfter := goal1,
-           tactic := "intro p h",
-         },
-         {
-           goalBefore := goal1 ,
-           goalAfter := "",
-           tactic := "exact h",
-         },
-       ]
+       units := [{
+         boundary := (0, file.utf8ByteSize),
+         invocations? := .some [
+           {
+             goalBefore := "⊢ ∀ (p : Prop), p → p",
+             goalAfter := goal1,
+             tactic := "intro p h",
+           },
+           {
+             goalBefore := goal1 ,
+             goalAfter := "",
+             tactic := "exact h",
+           },
+         ]
+       }],
     }: Protocol.FrontendProcessResult),
   ]
 
@@ -212,13 +214,14 @@ def test_frontend_process_sorry : Test :=
         ("sorrys", .bool true),
       ]
      ({
-       units := [
-         (0, solved.utf8ByteSize),
-         (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
-       ],
-       goalStates? := [
-         (0, #[goal1]),
-       ]
+       units := [{
+         boundary := (0, solved.utf8ByteSize),
+       }, {
+         boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
+         goalStateId? := .some 0,
+         goals := #[goal1],
+         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       }],
     }: Protocol.FrontendProcessResult),
   ]