31 changed files with 361 additions and 732 deletions
--- a/Main.lean
+++ b/Main.lean
@ -10,26 +10,23 @@ open Pantograph.Protocol

 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
-  match s.trim.get? 0 with
-  | .some '{' =>
-    -- Parse in Json mode
+  let s := s.trim
+  match s.get? 0 with
+  | .some '{' => -- Parse in Json mode
    Lean.fromJson? (← Lean.Json.parse s)
-  | .some _ =>
-    -- Parse in line mode
+  | .some _ => -- Parse in line mode
    let offset := s.posOf ' ' |> s.offsetOfPos
    if offset = s.length then
      return { cmd := s.take offset, payload := Lean.Json.null }
    else
      let payload ← s.drop offset |> Lean.Json.parse
      return { cmd := s.take offset, payload := payload }
-  | .none =>
-    throw "Command is empty"
+  | .none => throw "Command is empty"

-partial def loop : MainM Unit := do repeat do
+partial def loop : MainM Unit := do
  let state ← get
  let command ← (← IO.getStdin).getLine
-  -- Halt the program if empty line is given
-  if command.trim.length = 0 then break
+  if command.trim.length = 0 then return ()
  match parseCommand command with
  | .error error =>
    let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
@ -46,21 +43,25 @@ partial def loop : MainM Unit := do repeat do
      let message ← e.toMessageData.toString
      let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
      IO.println error.compress
+  loop


 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
    IO.println s!"{Pantograph.version}"
    return

  Pantograph.initSearch ""

-  -- Separate imports and options
-  let (options, imports) := args.partition (·.startsWith "--")
-  let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
+  let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.toArray |> Pantograph.createCoreContext
+  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
  let coreState ← Pantograph.createCoreState imports.toArray
-  let context: Context := {}
+  let context: Context := {
+    imports
+  }
  try
    let coreM := loop.run context |>.run' {}
    IO.println "ready."
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -12,56 +12,24 @@ open Lean

 namespace Pantograph

-inductive Projection where
-  -- Normal field case
-  | field (projector : Name) (numParams : Nat)
-  -- Singular inductive case
-  | singular (recursor : Name) (numParams : Nat) (numFields : Nat)
-
-/-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
-@[export pantograph_analyze_projection]
-def analyzeProjection (env: Environment) (e: Expr): Projection :=
-  let (typeName, idx, _) := match e with
-    | .proj typeName idx struct => (typeName, idx, struct)
-    | _ => panic! "Argument must be proj"
-  if (getStructureInfo? env typeName).isSome then
-    let ctor := getStructureCtor env typeName
-    let fieldName := getStructureFields env typeName |>.get! idx
-    let projector := getProjFnForField? env typeName fieldName |>.get!
-    .field projector ctor.numParams
-  else
-    let recursor := mkRecOnName typeName
-    let ctor := getStructureCtor env typeName
-    .singular recursor ctor.numParams ctor.numFields
-
-def anonymousLevel : Level := .mvar ⟨.anonymous⟩
+structure ProjectionApplication where
+  projector: Name
+  numParams: Nat
+  inner: Expr

@[export pantograph_expr_proj_to_app]
-def exprProjToApp (env: Environment) (e: Expr): Expr :=
-  let anon : Expr := .mvar ⟨.anonymous⟩
-  match analyzeProjection env e with
-  | .field projector numParams =>
-    let info := match env.find? projector with
-      | .some info => info
-      | _ => panic! "Illegal projector"
-    let callee := .const projector $ List.replicate info.numLevelParams anonymousLevel
-    let args := (List.replicate numParams anon) ++ [e.projExpr!]
-    mkAppN callee args.toArray
-  | .singular recursor numParams numFields =>
-    let info := match env.find? recursor with
-      | .some info => info
-      | _ => panic! "Illegal recursor"
-    let callee := .const recursor $ List.replicate info.numLevelParams anonymousLevel
-    let typeArgs := List.replicate numParams anon
-    -- Motive type can be inferred directly
-    let motive := .lam .anonymous anon anon .default
-    let major := e.projExpr!
-    -- Generate a lambda of `numFields` parameters, and returns the `e.projIdx!` one.
-    let induct := List.foldl
-      (λ acc _ => .lam .anonymous anon acc .default)
-      (.bvar $ (numFields - e.projIdx! - 1))
-      (List.range numFields)
-    mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
+def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+  let (typeName, idx, inner) := match e with
+    | .proj typeName idx inner => (typeName, idx, inner)
+    | _ => panic! "Argument must be proj"
+  let ctor := getStructureCtor env typeName
+  let fieldName := getStructureFields env typeName |>.get! idx
+  let projector := getProjFnForField? env typeName fieldName |>.get!
+  {
+    projector,
+    numParams := ctor.numParams,
+    inner,
+  }

 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _

@ -296,36 +264,38 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n

 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serializeSortLevel (level: Level) : String :=
+partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
  let k := level.getOffset
  let u := level.getLevelOffset
  let u_str := match u with
    | .zero => "0"
    | .succ _ => panic! "getLevelOffset should not return .succ"
    | .max v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
      s!"(:max {v} {w})"
    | .imax v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
      s!"(:imax {v} {w})"
    | .param name =>
+      let name := serializeName name sanitize
      s!"{name}"
    | .mvar id =>
-      let name := id.name
+      let name := serializeName id.name sanitize
      s!"(:mv {name})"
  match k, u with
  | 0, _ => u_str
  | _, .zero => s!"{k}"
  | _, _ => s!"(+ {u_str} {k})"

+
 /--
 Completely serializes an expression tree. Json not used due to compactness

 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
  self expr
  where
  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@ -364,10 +334,9 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
        let name := mvarId.name
        pure s!"(:{pref} {name})"
    | .sort level =>
-      let level := serializeSortLevel level
+      let level := serializeSortLevel level sanitize
      pure s!"(:sort {level})"
    | .const declName _ =>
-      let declName := serializeName declName (sanitize := false)
      -- The universe level of the const expression is elided since it should be
      -- inferrable from surrounding expression
      pure s!"(:c {declName})"
@ -400,29 +369,24 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
      -- is wrapped in a :lit sexp.
      let v' := match v with
        | .natVal val => toString val
-        | .strVal val => IR.EmitC.quoteString val
+        | .strVal val => s!"\"{val}\""
      pure s!"(:lit {v'})"
    | .mdata _ inner =>
      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
      -- It may become necessary to incorporate the metadata.
      self inner
-    | .proj typeName idx inner => do
+    | .proj _ _ _ => do
      let env ← getEnv
-      match analyzeProjection env e with
-      | .field projector numParams =>
-        let autos := String.intercalate " " (List.replicate numParams "_")
-        let inner' ← self inner
-        pure s!"((:c {projector}) {autos} {inner'})"
-      | .singular _ _ _ =>
-        let typeName' := serializeName typeName (sanitize := false)
-        let e' ← self e
-        pure s!"(:proj {typeName'} {idx} {e'})"
+      let projApp := exprProjToApp env e
+      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
+      let inner ← self projApp.inner
+      pure s!"((:c {projApp.projector}) {autos} {inner})"
  -- Elides all unhygenic names
  binderInfoSexp : Lean.BinderInfo → String
    | .default => ""
-    | .implicit => " :i"
-    | .strictImplicit => " :si"
-    | .instImplicit => " :ii"
+    | .implicit => " :implicit"
+    | .strictImplicit => " :strictImplicit"
+    | .instImplicit => " :instImplicit"

 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
  let pp?: Option String ← match options.printExprPretty with
@ -568,7 +532,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
        then instantiateAll decl.type
        else pure $ decl.type
      let type_sexp ← if options.printSexp then
-          let sexp ← serializeExpressionSexp type
+          let sexp ← serializeExpressionSexp type (sanitize := false)
          pure <| " " ++ sexp
        else
          pure ""
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -43,22 +43,6 @@ def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
  if isNameInternal n || info.isUnsafe
  then Option.none
  else Option.some <| toCompactSymbolName n info
-def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
-  let env ← Lean.MonadEnv.getEnv
-  return {
-    imports := env.header.imports.map toString,
-    modules := env.header.moduleNames.map (·.toString),
-  }
-def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do
-  let env ← Lean.MonadEnv.getEnv
-  let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
-    return .error $ Protocol.errorIndex s!"Module not found {args.module}"
-  let data := env.header.moduleData[i]!
-  return .ok {
-    imports := data.imports.map toString,
-    constNames := data.constNames.map (·.toString),
-    extraConstNames := data.extraConstNames.map (·.toString),
-  }
 def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
  let env ← Lean.MonadEnv.getEnv
  let names := env.constants.fold (init := #[]) (λ acc name info =>
@ -74,7 +58,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
    | some info => pure info
  let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat)
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
  let value? := match args.value?, info with
    | .some true, _ => info.value?
    | .some false, _ => .none
@ -96,7 +80,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
      then value?.map (λ e =>
        e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
      else .none,
-    module? := module?.map (·.toString)
+    module? := module?
  }
  let result ← match info with
    | .inductInfo induct => pure { core with inductInfo? := .some {
@ -129,20 +113,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
          k := r.k,
      } }
    | _ => pure core
-  let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
-      let declRange? ← findDeclarationRanges? name
-      let sourceStart? := declRange?.map (·.range.pos)
-      let sourceEnd? := declRange?.map (·.range.endPos)
-      .pure {
-        result with
-        sourceUri?,
-        sourceStart?,
-        sourceEnd?,
-      }
-    else
-      .pure result
  return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
  let env ← Lean.MonadEnv.getEnv
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
  let s := (← get).commandState
  let before := s.env
  let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back!
+  let stx := (← get).commands.back
  let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
  let s' := (← get).commandState
  let after := s'.env
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=

@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
    | info@(.ofTacticInfo _) => info.isOriginal
    | _ => false
-  let tactics := tacticInfoTrees.flatMap collectTactics
+  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
@ -104,20 +104,14 @@ structure InfoWithContext where
  info: Elab.Info
  context?: Option Elab.ContextInfo := .none

-structure GoalCollectionOptions where
-  collectTypeErrors : Bool := false
-
-private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
+private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
  let infos ← t.findAllInfoM none fun i ctx? => match i with
-    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
+    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
      let .some ctx := ctx? | return (false, true)
      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
        if expectedType?.isNone then
          throw $ .userError "Sorry of indeterminant type is not allowed"
        return (true, false)
-      unless options.collectTypeErrors do
-        return (false, true)
      let .some expectedType := expectedType? | return (false, true)
      let typeMatch ← ctx.runMetaM lctx do
        let type ← Meta.inferType expr
@ -136,9 +130,8 @@ private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOpt

 -- NOTE: Plural deliberately not spelled "sorries"
@[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
-  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
+def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
+  return (← step.trees.mapM collectSorrysInTree).join

 structure AnnotatedGoalState where
  state : GoalState
@ -148,39 +141,29 @@ structure AnnotatedGoalState where
 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`.
-
-WARNING: Behaviour is unstable when there are multiple `sorry`s. Consider using
-the draft tactic instead.
 -/
@[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
-  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
  assert! !sorrys.isEmpty
-  withEnv env do
-    let goalsM := sorrys.mapM λ i => do
-      match i.info with
-      | .ofTermInfo termInfo  => do
-        let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-        if (← mvarId.getType).hasSorry then
-          throwError s!"Coupling is not allowed in drafting"
-        return [(mvarId, stxByteRange termInfo.stx)]
-      | .ofTacticInfo tacticInfo => do
-        let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-        for mvarId in mvarIds do
-          if (← mvarId.getType).hasSorry then
-            throwError s!"Coupling is not allowed in drafting"
-        let range := stxByteRange tacticInfo.stx
-        return mvarIds.map (·, range)
-      | _ => panic! "Invalid info"
-    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-    let goals := annotatedGoals.map Prod.fst
-    let srcBoundaries := annotatedGoals.map Prod.snd
-    let root := match goals with
-      | [] => panic! "No MVars generated"
-      | [g] => g
-      | _ => { name := .anonymous }
-    let state ← GoalState.createFromMVars goals root
-    return { state, srcBoundaries }
+  let goalsM := sorrys.mapM λ i => do
+    match i.info with
+    | .ofTermInfo termInfo  => do
+      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      return [(mvarId, stxByteRange termInfo.stx)]
+    | .ofTacticInfo tacticInfo => do
+      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      let range := stxByteRange tacticInfo.stx
+      return mvarIds.map (·, range)
+    | _ => panic! "Invalid info"
+  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
+  let goals := annotatedGoals.map Prod.fst
+  let srcBoundaries := annotatedGoals.map Prod.snd
+  let root := match goals with
+    | [] => panic! "No MVars generated"
+    | [g] => g
+    | _ => { name := .anonymous }
+  let state ← GoalState.createFromMVars goals root
+  return { state, srcBoundaries }


@[export pantograph_frontend_collect_new_defined_constants_m]
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@ -26,8 +26,6 @@ protected def Info.stx? : Info → Option Syntax
  | .ofFVarAliasInfo      _    => none
  | .ofFieldRedeclInfo    info => info.stx
  | .ofOmissionInfo       info => info.stx
-  | .ofChoiceInfo         info => info.stx
-  | .ofPartialTermInfo    info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
  match i.stx? with
@ -89,9 +87,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
  | .context ctx tree => tree.filter p m |>.map (.context ctx)
  | .node info children =>
    if p info then
-      [.node info (children.toList.map (filter p m)).flatten.toPArray']
+      [.node info (children.toList.map (filter p m)).join.toPArray']
    else
-      (children.toList.map (filter p m)).flatten
+      (children.toList.map (filter p m)).join
  | .hole mvar => if m mvar then [.hole mvar] else []

 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@ -105,7 +103,7 @@ partial def InfoTree.findAllInfo
  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
  | .node i children  =>
    let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
    head ++ tail
  | _ => []

@ -121,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
    let (flagCollect, flagRecurse) ← pred i context?
    let head := if flagCollect then [(i, context?, children)] else []
    let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
-    return head ++ (← tail).flatten
+    return head ++ (← tail).join
  | _ => return []

@[export pantograph_infotree_to_string_m]
@ -143,8 +141,6 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
      | .ofFVarAliasInfo _ => pure "[fvar]"
      | .ofFieldRedeclInfo _ => pure "[field_redecl]"
      | .ofOmissionInfo _ => pure "[omission]"
-      | .ofChoiceInfo _ => pure "[choice]"
-      | .ofPartialTermInfo  _ => pure "[partial_term]"
      let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
      return s!"{node}\n{children}"
    else throw <| IO.userError "No `ContextInfo` available."
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@ -68,8 +68,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
    match e with
    | .fvar fvarId =>
      let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
-      -- Delegating this to `Meta.check` later
-      --assert! (← getLCtx).contains fvarId'
+      assert! (← getLCtx).contains fvarId'
      return .done $ .fvar fvarId'
    | .mvar mvarId => do
      -- Must not be assigned
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -183,8 +183,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
  -- to one of these seed mvars, it means an error has occurred when a tactic
  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
  -- need to manually find them and save them into the goal list.
-
-  let descendants ←  Meta.getMVars (.mvar src)
+  let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
  let mut alreadyVisited : MVarIdSet := {}
  let mut result : MVarIdSet := {}
@ -238,34 +237,25 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message: String)

-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
-      if m.severity == .error then
-        return .some $ ← m.toString
-      else
-        return .none
-  Core.resetMessageLog
-  return newMessages.toArray
-
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
-protected def GoalState.tryTacticM
-    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
-    (guardMVarErrors : Bool := false)
-    : Elab.TermElabM TacticResult := do
-  let prevMessageLength := state.coreState.messages.toList.length
+protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false):
+      Elab.TermElabM TacticResult := do
  try
    let nextState ← state.step goal tacticM guardMVarErrors

    -- Check if error messages have been generated in the core.
-    let newMessages ← dumpMessageLog prevMessageLength
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
+      |>.filterMapM λ m => do
+        if m.severity == .error then
+          return .some $ ← m.toString
+        else
+          return .none
+    Core.resetMessageLog
    if ¬ newMessages.isEmpty then
-      return .failure newMessages
+      return .failure newMessages.toArray
    return .success nextState
  catch exception =>
-    match exception with
-    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
-    | _ => return .failure #[← exception.toMessageData.toString]
+    return .failure #[← exception.toMessageData.toString]

 /-- Execute a string tactic on given state. Restores TermElabM -/
@[export pantograph_goal_state_try_tactic_m]
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -138,36 +138,17 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
  runMetaM <| state.serializeGoals (parent := .none) options

@[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
-  : CoreM Protocol.GoalPrintResult := runMetaM do
-  state.restoreMetaM
-
-  let root? ← if rootExpr then
-      state.rootExpr?.mapM λ expr => state.withRootContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let parent? ← if parentExpr then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let goals ← if goals then
-      goalSerialize state options
-    else
-      pure #[]
-  let extraMVars ← extraMVars.mapM λ mvarId => do
-    let mvarId: MVarId := { name := mvarId.toName }
-    let .some _ ← mvarId.findDecl? | return {}
-    state.withContext mvarId do
-      let .some expr ← getExprMVarAssignment? mvarId | return {}
-      serializeExpression options (← instantiateAll expr)
-  return {
-    root?,
-    parent?,
-    goals,
-    extraMVars,
-  }
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+  runMetaM do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr =>
+        state.withRootContext do
+          serializeExpression options (← instantiateAll expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr =>
+        state.withParentContext do
+          serializeExpression options (← instantiateAll expr)),
+    }

@[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
@ -207,14 +188,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: Stri
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-@[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
-  let expr ← match (← parseTermM expr) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.tryTacticM goal (Tactic.evalDraft expr)
@[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
  runTermElabM <| state.tryLet goal binderName type
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -5,7 +5,6 @@ Note that no command other than `InteractionError` may have `error` as one of
 its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
-import Lean.Data.Position

 namespace Pantograph.Protocol

@ -112,24 +111,6 @@ structure ExprEchoResult where
  type: Expression
  deriving Lean.ToJson

-- Describe the current state of the environment
-structure EnvDescribe where
-  deriving Lean.FromJson
-structure EnvDescribeResult where
-  imports : Array String
-  modules : Array String
-  deriving Lean.ToJson
-
-- Describe a module
-structure EnvModuleRead where
-  module : String
-  deriving Lean.FromJson
-structure EnvModuleReadResult where
-  imports: Array String
-  constNames: Array String
-  extraConstNames: Array String
-  deriving Lean.ToJson
-
 -- Print all symbols in environment
 structure EnvCatalog where
  deriving Lean.FromJson
@ -140,13 +121,11 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
  name: String
-  -- Show the value expressions; By default definitions values are shown and
-  -- theorem values are hidden.
+  -- If true/false, show/hide the value expressions; By default definitions
+  -- values are shown and theorem values are hidden.
  value?: Option Bool := .some false
-  -- Show the type and value dependencies
+  -- If true, show the type and value dependencies
  dependency?: Option Bool := .some false
-  -- Show source location
-  source?: Option Bool := .some false
  deriving Lean.FromJson
 -- See `InductiveVal`
 structure InductInfo where
@ -193,11 +172,6 @@ structure EnvInspectResult where
  inductInfo?:      Option InductInfo      := .none
  constructorInfo?: Option ConstructorInfo := .none
  recursorInfo?:    Option RecursorInfo    := .none
-
-  -- Location in source
-  sourceUri?: Option String := .none
-  sourceStart?: Option Lean.Position := .none
-  sourceEnd?: Option Lean.Position := .none
  deriving Lean.ToJson

 structure EnvAdd where
@ -255,7 +229,6 @@ structure GoalTactic where
  calc?: Option String := .none
  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
  conv?: Option Bool := .none
-  draft?: Option String := .none

  -- In case of the `have` tactic, the new free variable name is provided here
  binderName?: Option String := .none
@ -298,23 +271,12 @@ structure GoalDeleteResult where

 structure GoalPrint where
  stateId: Nat
-
-  -- Print root?
-  rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
-  -- Print goals?
-  goals?: Option Bool := .some False
-  -- Print values of extra mvars?
-  extraMVars?: Option (Array String) := .none
  deriving Lean.FromJson
 structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
  -- The filling expression of the parent goal
-  parent?: Option Expression := .none
-  goals: Array Goal := #[]
-  extraMVars: Array Expression := #[]
+  parent?: Option Expression
  deriving Lean.ToJson

 -- Diagnostic Options, not available in REPL
@ -346,13 +308,11 @@ 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
-  -- collect tactic invocations
+  -- If set to true, collect tactic invocations
  invocations: Bool := false
-  -- collect `sorry`s
+  -- If set to true, collect `sorry`s
  sorrys: Bool := false
-  -- collect type errors
-  typeErrorsAsGoals: Bool := false
-  -- list new constants from each compilation step
+  -- If set to true, extract new constants
  newConstants: Bool := false
  deriving Lean.FromJson
 structure InvokedTactic where
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -59,12 +59,6 @@ and then add the new constants.
 def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
  Pantograph.pickle path (env.header.imports, env.constants.map₂)

-def resurrectEnvironment
-  (imports : Array Import)
-  (map₂ : PHashMap Name ConstantInfo)
-  : IO Environment := do
-  let env ← importModules imports {} 0
-  env.replay (Std.HashMap.ofList map₂.toList)
 /--
 Unpickle an `Environment` from disk.

@ -74,7 +68,8 @@ and then replace the new constants.
@[export pantograph_env_unpickle_m]
 def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
-  return (← resurrectEnvironment imports map₂, region)
+  let env ← importModules imports {} 0
+  return (← env.replay (Std.HashMap.ofList map₂.toList), region)


 open Lean.Core in
@ -93,9 +88,7 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
    savedState := {
      term := {
        meta := {
-          core := {
-            env, nextMacroScope, ngen, ..
-          },
+          core,
          meta,
        }
        «elab»,
@ -107,10 +100,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
    convMVar?,
    calcPrevRhs?,
  } := goalState
+  --let env := core.env
  Pantograph.pickle path (
-    env.constants.map₂,
-
-    ({ nextMacroScope, ngen } : CompactCoreState),
+    ({ core with } : CompactCoreState),
    meta,
    «elab»,
    tactic,
@ -125,8 +117,6 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
 def goalStateUnpickle (path : System.FilePath) (env : Environment)
    : IO (GoalState × CompactedRegion) := unsafe do
  let ((
-    map₂,
-
    compactCore,
    meta,
    «elab»,
@ -137,8 +127,6 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    convMVar?,
    calcPrevRhs?,
  ), region) ← Pantograph.unpickle (
-    PHashMap Name ConstantInfo ×
-
    CompactCoreState ×
    Meta.State ×
    Elab.Term.State ×
@ -149,7 +137,6 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    Option (MVarId × MVarId × List MVarId) ×
    Option (MVarId × Expr)
  ) path
-  let env ← env.replay (Std.HashMap.ofList map₂.toList)
  let goalState := {
    savedState := {
      term := {
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@ -27,38 +27,5 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
  goal.assign expr
  Elab.Tactic.replaceMainGoal nextGoals

-def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
-  Meta.transform src λ
-    | .app (.app (.const ``sorryAx ..) type) .. => do
-      let type ← instantiateMVars type
-      if type.hasSorry then
-        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
-      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
-      modify (mvar.mvarId! :: .)
-      pure $ .done mvar
-    | _ => pure .continue
-
-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
-def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
-  goal.checkNotAssigned `Pantograph.Tactic.draft
-  let exprType ← Meta.inferType expr
-  let goalType ← goal.getType
-  unless ← Meta.isDefEq goalType exprType do
-    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
-
-  let (expr', holes) ← sorryToHole expr |>.run []
-  goal.assign expr'
-  return holes.reverse
-
-def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
-  let target ← Elab.Tactic.getMainTarget
-  let goal ← Elab.Tactic.getMainGoal
-  let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
-    (expectedType? := .some target)
-    (tagSuffix := .anonymous)
-    (allowNaturalHoles := true)
-  let draftGoals ← draft goal expr
-  Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
-

 end Pantograph.Tactic
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
  let fvarId ← mkFreshFVarId
  let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
  let mvarUpstream ←
-    Meta.withLCtx lctxUpstream #[] do
+    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
      Meta.withNewLocalInstances #[.fvar fvarId] 0 do
        let mvarUpstream ← mkUpstreamMVar mvarId
        --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,6 +1,6 @@
 namespace Pantograph

@[export pantograph_version]
-def version := "0.2.25"
+def version := "0.2.22"

 end Pantograph
--- a/Repl.lean
+++ b/Repl.lean
@ -3,9 +3,8 @@ import Pantograph

 namespace Pantograph.Repl

-open Lean
-
 structure Context where
+  imports: List String

 /-- Stores state of the REPL -/
 structure State where
@ -14,9 +13,7 @@ structure State where
  goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty

 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context $ StateRefT State CoreM
-/-- Fallible subroutine return type -/
-abbrev CR α := Except Protocol.InteractionError α
+abbrev MainM := ReaderT Context (StateT State Lean.CoreM)

 def newGoalState (goalState: GoalState) : MainM Nat := do
  let state ← get
@ -28,105 +25,29 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
  return stateId


-def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
+-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
+-- certain monadic features in `MainM`
+abbrev CR α := Except Protocol.InteractionError α
+
+def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
  metaM.run'
-def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
+def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
  termElabM.run' (ctx := defaultElabContext) |>.run'

-section Frontend
-
-structure CompilationUnit where
-  -- Should be the penultimate environment, but this is ok
-  env : Environment
-  boundary : Nat × Nat
-  invocations : List Protocol.InvokedTactic
-  sorrys : List Frontend.InfoWithContext
-  messages : Array String
-  newConstants : List Name
-
-def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-  let options := (← get).options
-  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 Environment ← if args.fileName?.isSome then
-      pure .none
-    else do
-      let env ← getEnv
-      pure <| .some env
-  let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
-    Frontend.mapCompilationSteps λ step => do
-    let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-    let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations then
-        Frontend.collectTacticsFromCompilationStep step
-      else
-        pure []
-    let sorrys ← if args.sorrys then
-        Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
-      else
-        pure []
-    let messages ← step.messageStrings
-    let newConstants ← if args.newConstants then
-        Frontend.collectNewDefinedConstants step
-      else
-        pure []
-    return {
-      env := step.before,
-      boundary,
-      invocations,
-      sorrys,
-      messages,
-      newConstants
-    }
-  let li ← frontendM.run context |>.run' state
-  let units ← li.mapM λ step => withEnv step.env do
-    let newConstants? := if args.newConstants then
-        .some $ step.newConstants.toArray.map λ name => name.toString
-      else
-        .none
-    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
-        pure (.none, .none, .none)
-      else do
-        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
-        let stateId ← newGoalState state
-        let goals ← goalSerialize state options
-        let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
-        pure (.some stateId, .some goals, .some srcBoundaries)
-    let invocations? := if args.invocations then .some step.invocations else .none
-    return {
-      boundary := step.boundary,
-      messages := step.messages,
-      invocations?,
-      goalStateId?,
-      goals?,
-      goalSrcBoundaries?,
-      newConstants?,
-    }
-  return .ok { units }
-
-end Frontend
-
 /-- Main loop command of the REPL -/
-def execute (command: Protocol.Command): MainM Json := do
-  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → MainM (CR β)): MainM Json :=
-    match fromJson? command.payload with
+def execute (command: Protocol.Command): MainM Lean.Json := do
+  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
+    match Lean.fromJson? command.payload with
    | .ok args => do
      match (← comm args) with
-      | .ok result =>  return toJson result
-      | .error ierror => return toJson ierror
-    | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
+      | .ok result =>  return Lean.toJson result
+      | .error ierror => return Lean.toJson ierror
+    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
  try
    match command.cmd with
    | "reset"         => run reset
    | "stat"          => run stat
    | "expr.echo"     => run expr_echo
-    | "env.describe"  => run env_describe
-    | "env.module_read" => run env_module_read
    | "env.catalog"   => run env_catalog
    | "env.inspect"   => run env_inspect
    | "env.add"       => run env_add
@ -145,10 +66,10 @@ def execute (command: Protocol.Command): MainM Json := do
    | cmd =>
      let error: Protocol.InteractionError :=
        errorCommand s!"Unknown command {cmd}"
-      return toJson error
+      return Lean.toJson error
  catch ex => do
    let error ← ex.toMessageData.toString
-    return toJson $ errorIO error
+    return Lean.toJson $ errorIO error
  where
  errorCommand := errorI "command"
  errorIndex := errorI "index"
@ -158,17 +79,12 @@ def execute (command: Protocol.Command): MainM Json := do
    let state ← get
    let nGoals := state.goalStates.size
    set { state with nextId := 0, goalStates := .empty }
-    Core.resetMessageLog
+    Lean.Core.resetMessageLog
    return .ok { nGoals }
  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
    let state ← get
    let nGoals := state.goalStates.size
    return .ok { nGoals }
-  env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
-    let result ← Environment.describe args
-    return .ok result
-  env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
-    Environment.moduleRead args
  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
    let result ← Environment.catalog args
    return .ok result
@ -178,12 +94,12 @@ def execute (command: Protocol.Command): MainM Json := do
  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
    Environment.addDecl args
  env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
-    let env ← MonadEnv.getEnv
+    let env ← Lean.MonadEnv.getEnv
    environmentPickle env args.path
    return .ok {}
  env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
    let (env, _) ← environmentUnpickle args.path
-    setEnv env
+    Lean.setEnv env
    return .ok {}
  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
    let state ← get
@ -208,7 +124,7 @@ def execute (command: Protocol.Command): MainM 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 env ← MonadEnv.getEnv
+    let env ← Lean.MonadEnv.getEnv
    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
      | .none, .some copyFrom =>
@ -229,27 +145,24 @@ def execute (command: Protocol.Command): MainM Json := do
    let .some goal := goalState.goals.get? args.goalId |
      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
-      -- NOTE: Should probably use a macro to handle this...
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
+      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
+      | .some tactic, .none, .none, .none, .none, .none => do
        pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none => do
        pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
+      | .none, .none, .some type, .none, .none, .none => do
        let binderName := args.binderName?.getD ""
        pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none, .none => do
+      | .none, .none, .none, .some type, .none, .none => do
        let binderName := args.binderName?.getD ""
        pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none, .none => do
+      | .none, .none, .none, .none, .some pred, .none => do
        pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
+      | .none, .none, .none, .none, .none, .some true => do
        pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
+      | .none, .none, .none, .none, .none, .some false => do
        pure <| Except.ok <| ← goalState.convExit
-      | .none, .none, .none, .none, .none, .none, .some draft => do
-        pure <| Except.ok <| ← goalState.tryDraft goal draft
-      | _, _, _, _, _, _, _ =>
+      | _, _, _, _, _, _ =>
        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
        pure $ Except.error $ error
    match nextGoalState? with
@ -310,13 +223,7 @@ def execute (command: Protocol.Command): MainM Json := do
    let state ← get
    let .some goalState := state.goalStates[args.stateId]? |
      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint
-        goalState
-        (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
-        (goals := args.goals?.getD False)
-        (extraMVars := args.extraMVars?.getD #[])
-        (options := state.options)
+    let result ← runMetaInMainM <| goalPrint goalState state.options
    return .ok result
  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
    let state ← get
@ -325,12 +232,66 @@ def execute (command: Protocol.Command): MainM Json := do
    goalStatePickle goalState args.path
    return .ok {}
  goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
-    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv)
    let id ← newGoalState goalState
    return .ok { id }
  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+    let options := (← get).options
    try
-      frontend_process_inner args
+      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 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
+            pure []
+        let messages ← step.messageStrings
+        let newConstants ← if args.newConstants then
+            Frontend.collectNewDefinedConstants step
+          else
+            pure []
+        return (step.before, boundary, invocations?, sorrys, messages, newConstants)
+      let li ← frontendM.run context |>.run' state
+      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
+        let newConstants? := if args.newConstants then
+            .some $ newConstants.toArray.map λ name => name.toString
+          else
+            .none
+        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
+            pure (.none, .none, .none)
+          else do
+            let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
+            let stateId ← newGoalState state
+            let goals ← goalSerialize state options
+            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+            pure (.some stateId, .some goals, .some srcBoundaries)
+        return {
+          boundary,
+          messages,
+          invocations?,
+          goalStateId?,
+          goals?,
+          goalSrcBoundaries?,
+          newConstants?,
+        }
+      return .ok { units }
    catch e =>
      return .error $ errorI "frontend" (← e.toMessageData.toString)

--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -48,12 +48,6 @@ namespace Condensed
 deriving instance BEq, Repr for LocalDecl
 deriving instance BEq, Repr for Goal

-- Enable string interpolation
-instance : ToString FVarId where
-  toString id := id.name.toString
-instance : ToString MVarId where
-  toString id := id.name.toString
-
 protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
  {
    decl with fvarId := { name := .anonymous }
@ -149,8 +143,6 @@ def runTest (t: TestT m Unit): m LSpec.TestSeq :=
  Prod.snd <$> t.run LSpec.TestSeq.done
 def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
  t.run LSpec.TestSeq.done
-def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
-  runCoreMSeq env (runTest coreM) options

 end Monadic

--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@ -35,7 +35,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
    ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
    -- These ones are normal and easy
    ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
-    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
    -- Handling of higher order types
    ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
    ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
@ -50,8 +50,8 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
  let entries: List (String × (List Name) × String) := [
    ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
-    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
  ]
  entries.foldlM (λ suites (source, levels, target) =>
@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
            .default)
        .implicit)
      .implicit,
-      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
    ),
  ]
  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
@ -96,23 +96,6 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
    let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
    return LSpec.TestSeq.done

-def test_projection_prod (env: Environment) : IO LSpec.TestSeq:= runTest do
-  let struct := .app (.bvar 1) (.bvar 0)
-  let expr := .proj `Prod 1 struct
-  let .field projector numParams := analyzeProjection env expr |
-    fail "`Prod has fields"
-  checkEq "projector" projector `Prod.snd
-  checkEq "numParams" numParams 2
-
-def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
-  let struct := .app (.bvar 1) (.bvar 0)
-  let expr := .proj `Exists 1 struct
-  let .singular recursor numParams numFields := analyzeProjection env expr |
-    fail "`Exists has no projectors"
-  checkEq "recursor" recursor `Exists.recOn
-  checkEq "numParams" numParams 2
-  checkEq "numFields" numFields 2
-
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  [
    ("serializeName", do pure test_serializeName),
@ -121,8 +104,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("Sexp from elaborated expr", test_sexp_of_elab env),
    ("Sexp from expr", test_sexp_of_expr env),
    ("Instance", test_instance env),
-    ("Projection Prod", test_projection_prod env),
-    ("Projection Exists", test_projection_exists env),
  ]

 end Pantograph.Test.Delate
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -97,29 +97,11 @@ def test_inspect: IO LSpec.TestSeq := do
    ) LSpec.TestSeq.done
  runCoreMSeq env inner

-def test_symbol_location : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
-  addTest $ ← runTestCoreM env do
-    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
-    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
-
-    -- Extraction of source doesn't work for symbols in `Init` for some reason
-    checkTrue "file" result.sourceUri?.isNone
-    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
-    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
-    checkTrue "constNames" $ constNames.contains "Nat.succ_add"
-
 def suite: List (String × IO LSpec.TestSeq) :=
  [
    ("Catalog", test_catalog),
    ("Symbol Visibility", test_symbol_visibility),
    ("Inspect", test_inspect),
-    ("Symbol Location", runTest test_symbol_location),
  ]

 end Pantograph.Test.Environment
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@ -6,12 +6,11 @@ import Test.Common
 open Lean Pantograph
 namespace Pantograph.Test.Frontend

-def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
-    : MetaM (List GoalState) := do
+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 (step.before, ← Frontend.collectSorrys step options)
+    return (step.before, ← Frontend.collectSorrys step)
  let li ← m.run context |>.run' state
  let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
    if sorrys.isEmpty then
@ -182,10 +181,9 @@ def test_capture_type_mismatch : TestT MetaM Unit := do
  let input := "
 def mystery (k: Nat) : Nat := true
  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
+  let goalStates ← (collectSorrysFromSource input).run' {}
  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
+  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
    {
      target := { pp? := "Nat" },
      vars := #[{
@ -195,16 +193,6 @@ def mystery (k: Nat) : Nat := true
    }
  ]

-def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
-  let input := "
-example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
-  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
-  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
-  ]
-
 def collectNewConstants (source: String) : MetaM (List (List Name)) := do
  let filename := "<anonymous>"
  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
@ -239,7 +227,6 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
    ("sorry_in_coupled", test_sorry_in_coupled),
    ("environment_capture", test_environment_capture),
    ("capture_type_mismatch", test_capture_type_mismatch),
-    --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
    ("collect_one_constant", test_collect_one_constant),
    ("collect_one_theorem", test_collect_one_theorem),
  ]
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -72,8 +72,8 @@ def test_tactic : Test :=
     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+    step "goal.print" [("stateId", .num 1)]
+     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
     ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
  ]
@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
    ],
  }
  let goal2l: Protocol.Goal := {
-    name := "_uniq.61",
+    name := "_uniq.59",
    userName? := .some "inl",
    target := { pp? := .some "q ∨ p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
    ],
  }
  let goal2r: Protocol.Goal := {
-    name := "_uniq.74",
+    name := "_uniq.72",
    userName? := .some "inr",
    target := { pp? := .some "q ∨ p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
    ],
  }
  let goal3l: Protocol.Goal := {
-    name := "_uniq.80",
+    name := "_uniq.78",
    userName? := .some "inl.h",
    target := { pp? := .some "p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
    ],
  }
  [
@ -171,11 +171,10 @@ def test_frontend_process : Test :=
    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
    step "frontend.process"
      [
-        ("file",              .str file),
-        ("invocations",       .bool true),
-        ("sorrys",            .bool false),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants",      .bool false),
+        ("file", .str file),
+        ("invocations", .bool true),
+        ("sorrys", .bool false),
+        ("newConstants", .bool false),
      ]
     ({
       units := [{
@ -216,7 +215,6 @@ def test_frontend_process_sorry : Test :=
        ("file", .str file),
        ("invocations", .bool false),
        ("sorrys", .bool true),
-        ("typeErrorsAsGoals", .bool false),
        ("newConstants", .bool false),
      ]
     ({
@ -235,7 +233,9 @@ def test_frontend_process_sorry : Test :=

 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
  -- Setup the environment for execution
-  let context: Context := {}
+  let context: Context := {
+    imports := ["Init"]
+  }
  let commands: MainM LSpec.TestSeq :=
    steps.foldlM (λ suite step => do
      let result ← step
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -53,7 +53,6 @@ def main (args: List String) := do
    ("Proofs", Proofs.suite env_default),
    ("Delate", Delate.suite env_default),
    ("Serial", Serial.suite env_default),
-    ("Tactic/Assign", Tactic.Assign.suite env_default),
    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
    ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -239,7 +239,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Roundtrip
@ -253,7 +253,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Continuation should fail if the state does not exist:
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -97,7 +97,7 @@ def test_identity: TestM Unit := do
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
    #[inner])
  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")

 -- Individual test cases
@ -241,15 +241,13 @@ def test_or_comm: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [state1g0] := state1.goals | fail "Should have 1 goal"
-  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
-    let lctx ← getLCtx
-    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
-      panic! "Incorrect number of decls"
-    pure (fvP, fvQ, fvH)
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
    #[{
-      name := state1g0.name.toString,
+      name := state1g0,
      target := { pp? := .some "q ∨ p" },
      vars := #[
        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@ -261,7 +259,7 @@ def test_or_comm: TestM Unit := do
  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone

  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
  let tactic := "cases h"
  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@ -271,16 +269,14 @@ def test_or_comm: TestM Unit := do
      return ()
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  let [state2g0, state2g1] := state2.goals |
-    fail s!"Should have 2 goals, but it has {state2.goals.length}"
-  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
+  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
    #[caseL, caseR])
  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone

  let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
  let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@ -296,9 +292,8 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
-  let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
@ -564,15 +559,12 @@ def test_nat_zero_add: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
    #[
-      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
    ])

  let tactic := "exact n"
@ -655,15 +647,13 @@ def test_nat_zero_add_alt: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
+  let major := "_uniq.68"
  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
    #[
-      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
    ])

  let tactic := "intro x"
@ -680,7 +670,8 @@ def test_nat_zero_add_alt: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
  let state2b ← match state3m2.resume [conduit] with
    | .ok state => pure state
@ -690,26 +681,20 @@ def test_nat_zero_add_alt: TestM Unit := do

  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN ← state2b.withContext conduit do
-    let lctx ← getLCtx
-    pure $ lctx.getFVarIds.get! 0 |>.name
+  let fvN := "_uniq.63"
  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
-  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
-  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
-  let nL' := nL + 4
-  let nR' := nR + 5
+  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
    #[
      {
-        name := mvarConduit.name.toString,
+        name := "_uniq.70",
        userName? := .some "conduit",
        target := {
-          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
+          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
        },
        vars := #[{
-          name := fvN.toString,
+          name := fvN,
          userName := "n",
          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
        }],
@ -735,6 +720,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]

+
 def test_tactic_failure_synthesize_placeholder : TestM Unit := do
  let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
  let state0 ← match state? with
@ -751,22 +737,19 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
      return ()

  let tactic := "simpa [h] using And.imp_left h _"
-  --let state2 ← match ← state1.tacticOn 0 tactic with
-  --  | .success state => pure state
-  --  | other => do
-  --    addTest $ assertUnreachable $ other.toString
-  --    return ()
+  let state2 ← match ← state1.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()

-  -- Volatile behaviour. This easily changes across Lean versions
-
-  --checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
-  --  buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
-  --]
-
-  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
-  checkEq s!"{tactic} fails" messages #[message]
+  checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
+    buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
+  ]

+  --let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
+  --let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
+  --checkEq s!"{tactic} fails" messages #[message]

 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  let tests := [
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -1,4 +1,3 @@
-import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
--- a/Test/Tactic/Assign.lean
+++ b/Test/Tactic/Assign.lean
@ -1,33 +0,0 @@
-import Lean.Meta
-import Lean.Elab
-import LSpec
-import Test.Common
-
-open Lean
-
-namespace Pantograph.Test.Tactic.Assign
-
-def test_draft : TestT Elab.TermElabM Unit := do
-  let expr := "forall (p : Prop), (p ∨ p) ∨ p"
-  let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
-  let expr ← parseSentence expr
-  Meta.forallTelescope expr $ λ _ body => do
-    let skeleton' ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := skeleton)
-      (fileName := ← getFileName) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalDraft skeleton'
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("draft", test_draft),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Assign
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
    let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
    addTest $ LSpec.check "apply" (results.length = 0)
    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
 def test_congr_arg : TestT Elab.TermElabM Unit := do
  let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
  let expr ← parseSentence expr
@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
      [
-        (`α, "Sort ?u.73"),
+        (`α, "Sort ?u.70"),
        (`a₁, "?α"),
        (`a₂, "?α"),
        (`f, "?α → Nat"),
@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
      [
-        (`α, "Sort ?u.165"),
+        (`α, "Sort ?u.159"),
        (`f₁, "?α → Nat"),
        (`f₂, "?α → Nat"),
        (`h, "?f₁ = ?f₂"),
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
        "Nat → Prop",
        "Nat",
        "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.74 = (n + 0 = n)",
+        "?motive ?m.67 = (n + 0 = n)",
      ])
    addTest test

@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
    let tactic := Tactic.evalMotivatedApply recursor
    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 74
+    let majorId := 67
    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
      [
        "Nat → Prop",
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do

    addTest $ ← conduit.withContext do
      let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")

 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  [
--- a/doc/repl.md
+++ b/doc/repl.md
@ -13,8 +13,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  only the values of definitions are printed.
 * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
  current environment to/from a file
-* `env.module_read { "module": <name }`: Reads a list of symbols from a module
-* `env.describe {}`: Describes the imports and modules in the current environment
 * `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`

@ -35,7 +33,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
    to the previous `rhs`.
  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
    exit, the goal id is ignored.
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
  Execute continuation/resumption
  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
@ -47,13 +44,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  state. The user is responsible to ensure the sender/receiver instances share
  the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
-  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
-  Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": true`), the sorrys and type errors into goal states
-  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
-  `sorrys`, this command additionally outputs the position of each captured
-  `sorry`. Warning: Behaviour is unstable in case of multiple `sorry`s. Use the
-  draft tactic if possible.
+  <bool>, sorrys: <bool>, newConstants: <bool> }`: Executes the Lean frontend on
+  a file, collecting the tactic invocations (`"invocations": true`), the
+  sorrys and type errors into goal states (`"sorrys": true`), and new constants
+  (`"newConstants": true`). In the case of `sorrys`, this command additionally
+  outputs the position of each captured `sorry`.

 ## Errors

--- a/flake.lock
+++ b/flake.lock
@ -42,11 +42,11 @@
        "nixpkgs": "nixpkgs"
      },
      "locked": {
-        "lastModified": 1736388194,
-        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
+        "lastModified": 1731711316,
+        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
+        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
        "type": "github"
      },
      "original": {
--- a/flake.nix
+++ b/flake.nix
@ -18,89 +18,82 @@
    lean4-nix,
    lspec,
    ...
-  }:
-    flake-parts.lib.mkFlake {inherit inputs;} {
-      flake = {
+  } : flake-parts.lib.mkFlake { inherit inputs; } {
+    flake = {
+    };
+    systems = [
+      "aarch64-linux"
+      "aarch64-darwin"
+      "x86_64-linux"
+      "x86_64-darwin"
+    ];
+    perSystem = { system, pkgs, ... }: let
+      pkgs = import nixpkgs {
+        inherit system;
+        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
      };
-      systems = [
-        "aarch64-linux"
-        "aarch64-darwin"
-        "x86_64-linux"
-        "x86_64-darwin"
-      ];
-      perSystem = {
-        system,
-        pkgs,
-        ...
-      }: let
-        pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
-        lspecLib = pkgs.lean.buildLeanPackage {
-          name = "LSpec";
-          roots = ["Main" "LSpec"];
-          src = "${lspec}";
-        };
-        project = pkgs.lean.buildLeanPackage {
-          name = "Pantograph";
-          roots = ["Pantograph"];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path)
-              && !(pkgs.lib.hasSuffix "Repl.lean" path);
-          });
-        };
-        repl = pkgs.lean.buildLeanPackage {
-          name = "Repl";
-          roots = ["Main" "Repl"];
-          deps = [project];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path);
-          });
-        };
-        test = pkgs.lean.buildLeanPackage {
-          name = "Test";
-          # NOTE: The src directory must be ./. since that is where the import
-          # root begins (e.g. `import Test.Environment` and not `import
-          # Environment`) and thats where `lakefile.lean` resides.
-          roots = ["Test.Main"];
-          deps = [lspecLib repl];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "Pantograph" path);
-          });
-        };
-      in rec {
-        packages = {
-          inherit (pkgs.lean) lean lean-all;
-          inherit (project) sharedLib iTree;
-          inherit (repl) executable;
-          default = repl.executable;
-        };
-        legacyPackages = {
-          inherit project;
-          leanPkgs = pkgs.lean;
-        };
-        checks = {
-          test =
-            pkgs.runCommand "test" {
-              buildInputs = [test.executable pkgs.lean.lean-all];
-            } ''
-              #export LEAN_SRC_PATH="${./.}"
-              ${test.executable}/bin/test > $out
-            '';
-        };
-        formatter = pkgs.alejandra;
-        devShells.default = pkgs.mkShell {
-          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
-        };
+      lspecLib = pkgs.lean.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
+      project = pkgs.lean.buildLeanPackage {
+        name = "Pantograph";
+        roots = [ "Pantograph" ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Repl.lean" path);
+        });
+      };
+      repl = pkgs.lean.buildLeanPackage {
+        name = "Repl";
+        roots = [ "Main" "Repl" ];
+        deps = [ project ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path);
+        });
+      };
+      test = pkgs.lean.buildLeanPackage {
+        name = "Test";
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib repl ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        });
+      };
+    in rec {
+      packages = {
+        inherit (pkgs.lean) lean lean-all;
+        inherit (project) sharedLib iTree;
+        inherit (repl) executable;
+        default = repl.executable;
+      };
+      legacyPackages = {
+        inherit project;
+        leanPkgs = pkgs.lean;
+      };
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable pkgs.lean.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
      };
    };
+  };
 }
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.12.0