diff --git a/Main.lean b/Main.lean
index eb5240d..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
+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
   }
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/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
new file mode 100644
index 0000000..fd91823
--- /dev/null
+++ b/Pantograph/Frontend.lean
@@ -0,0 +1,4 @@
+/- Adapted from lean-training-data by semorrison -/
+import Pantograph.Frontend.Basic
+import Pantograph.Frontend.Elab
+import Pantograph.Frontend.MetaTranslate
diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Frontend/Basic.lean
similarity index 54%
rename from Pantograph/Compile/Frontend.lean
rename to Pantograph/Frontend/Basic.lean
index 3dbad85..1074a94 100644
--- a/Pantograph/Compile/Frontend.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
@@ -27,7 +28,9 @@ protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :
 end Lean.PersistentArray
 
 
-namespace Pantograph.Compile
+namespace Pantograph.Frontend
+
+abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
   fileName : String
@@ -39,12 +42,21 @@ 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
 `done : Bool`, indicating whether this was the last command.
 -/
-def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
+@[export pantograph_frontend_process_one_command_m]
+def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
@@ -57,30 +69,52 @@ 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 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 :: (← processFile)
+    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"
 
-def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe 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
-  processFile.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)
 
-
-end Pantograph.Compile
+end Pantograph.Frontend
diff --git a/Pantograph/Compile/Elab.lean b/Pantograph/Frontend/Elab.lean
similarity index 61%
rename from Pantograph/Compile/Elab.lean
rename to Pantograph/Frontend/Elab.lean
index 79833f3..2036aea 100644
--- a/Pantograph/Compile/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -1,9 +1,12 @@
-
+/- Adapted from https://github.com/semorrison/lean-training-data -/
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
 
-import Pantograph.Compile.Frontend
+import Pantograph.Frontend.Basic
+import Pantograph.Frontend.MetaTranslate
+import Pantograph.Goal
+import Pantograph.Protocol
 
 open Lean
 
@@ -75,7 +78,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
 
@@ -86,6 +89,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. -/
@@ -121,17 +125,17 @@ 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,
 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
@@ -142,5 +146,64 @@ 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 ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      return t.pretty
+    return { goalBefore, goalAfter, tactic }
 
-end Pantograph.Compile
+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
+    | .ofTacticInfo { stx, .. } =>
+      -- The `sorry` term is distinct from the `sorry` tactic
+      stx.isOfKind `Lean.Parser.Tactic.tacticSorry
+    | _ => false
+  infos.map fun (info, context?, _) => { info, context? }
+
+-- NOTE: Plural deliberately not spelled "sorries"
+@[export pantograph_frontend_collect_sorrys_m]
+def collectSorrys (step: CompilationStep) : List InfoWithContext :=
+  step.trees.bind collectSorrysInTree
+
+
+
+/--
+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 InfoWithContext) : MetaM GoalState := do
+  assert! !sorrys.isEmpty
+  let goalsM := sorrys.mapM λ i => do
+    match i.info with
+    | .ofTermInfo termInfo  => do
+      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      return [mvarId]
+    | .ofTacticInfo tacticInfo => do
+      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+    | _ => panic! "Invalid info"
+  let goals := (← goalsM.run {} |>.run' {}).bind id
+  let root := match goals with
+    | [] => panic! "This function cannot be called on an empty list"
+    | [g] => g
+    | _ => { name := .anonymous }
+  GoalState.createFromMVars goals root
+
+
+
+end Pantograph.Frontend
diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean
new file mode 100644
index 0000000..1a12029
--- /dev/null
+++ b/Pantograph/Frontend/MetaTranslate.lean
@@ -0,0 +1,133 @@
+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
+  let lctx ← MonadLCtx.getLCtx
+  assert! lctx.isEmpty
+  (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
+    let localDecl ← Meta.withLCtx lctx #[] do
+      translateLocalDecl srcLocalDecl
+    pure $ lctx.addDecl localDecl
+  ) lctx
+
+partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
+  if let .some mvarId' := (← get).mvarMap.find? srcMVarId then
+    return mvarId'
+  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
+
+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/Pantograph/Goal.lean b/Pantograph/Goal.lean
index f248923..79e3004 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
 
 
@@ -48,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
@@ -145,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
@@ -385,20 +394,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 e88efa3..acc2681 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -284,21 +284,32 @@ 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
+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
-  units?: Option $ List (Nat × Nat)
-  invocations?: Option $ List InvokedTactic
+
+structure CompilationUnit where
+  -- String boundaries of compilation units
+  boundary: (Nat × Nat)
+  -- Tactic invocations
+  invocations?: Option (List InvokedTactic) := .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/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/Pantograph/Version.lean b/Pantograph/Version.lean
index ed33cbb..2decbc1 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.18"
+def version := "0.2.19"
 
 end Pantograph
diff --git a/README.md b/README.md
index 06ae690..04213ae 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
 
@@ -114,6 +101,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
 
@@ -130,6 +121,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:
@@ -143,8 +153,11 @@ 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.
 
-Note that there isn't a 1-1 correspondence between executable (REPL) commands
-and library functions.
+The executable can be used as-is, but linking against the shared library
+requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
+between executable (REPL) commands and library functions.
+
+Inject any project path via the `pantograph_init_search` function.
 
 ## Developing
 
@@ -152,7 +165,11 @@ 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
 ```
@@ -161,14 +178,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
-```
diff --git a/Repl.lean b/Repl.lean
index ef77d56..7597164 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
@@ -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}"
@@ -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,
@@ -201,20 +200,53 @@ 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
+    let options := (← get).options
     try
-      let steps ← Compile.processSource module
-      let units? := if args.compilationUnits then
-          .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-        else
-          .none
-      let invocations? ← if args.invocations then
-          pure $ .some (← Compile.collectTacticsFromCompilation steps)
-        else
+      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
-      return .ok { units?, invocations? }
+        else do
+          let env ← Lean.MonadEnv.getEnv
+          pure <| .some env
+      let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
+      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 .none
+        let sorrys := if args.sorrys then
+            Frontend.collectSorrys step
+          else
+            []
+        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
+            pure (.some stateId, goals)
+        return {
+          boundary,
+          invocations?,
+          goalStateId?,
+          goals,
+          messages,
+        }
+      return .ok { units }
     catch e =>
-      return .error $ errorI "compile" (← e.toMessageData.toString)
+      return .error $ errorI "frontend" (← e.toMessageData.toString)
 
-end Pantograph
+end Pantograph.Repl
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
new file mode 100644
index 0000000..68d961b
--- /dev/null
+++ b/Test/Frontend.lean
@@ -0,0 +1,172 @@
+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_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
+   sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  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 := #[
+      ]
+    },
+    {
+      target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
+      vars := #[{
+        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!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← 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!"Incorrect number of states: {goalStates.length}"
+  addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
+    {
+      target := { pp? := "0 + m = m" },
+      vars := #[{
+        userName := "m",
+        type? := .some { pp? := "Nat" },
+      }]
+    },
+    {
+      userName? := .some "zero",
+      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" },
+      }]
+    },
+    {
+      userName? := .some "succ",
+      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 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",
+           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))
+
+end Pantograph.Test.Frontend
diff --git a/Test/Integration.lean b/Test/Integration.lean
index b82962b..413ed1c 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)
@@ -161,6 +161,71 @@ 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 := [{
+         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),
+  ]
+
+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.6",
+      target := { pp? := .some "p → p" },
+      vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
+    }
+    step "frontend.process"
+      [
+        ("file", .str file),
+        ("invocations", .bool false),
+        ("sorrys", .bool true),
+      ]
+     ({
+       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),
+  ]
+
+
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let context: Context := {
@@ -182,6 +247,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 invocation", test_frontend_process),
+    ("frontend.process sorry", test_frontend_process_sorry),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 
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),