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 1/8] 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
-- 
2.44.1


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 2/8] 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)
-- 
2.44.1


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 3/8] 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))
 
-- 
2.44.1


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 4/8] 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))
 
-- 
2.44.1


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 5/8] 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. -/
-- 
2.44.1


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 6/8] 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
-```
-- 
2.44.1


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 7/8] 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
 
 
 
-- 
2.44.1


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 8/8] 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
   }
-- 
2.44.1