23 changed files with 678 additions and 1181 deletions
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -63,10 +63,7 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
      (List.range numFields)
    mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
-def _root_.Lean.Name.isAuxLemma (n : Name) : Bool :=
+def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
  match n with
  | .str _ s => "_proof_".isPrefixOf s
  | _ => false
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas_m]
@ -454,6 +451,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
    dependentMVars?,
  }
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
      : MetaM Protocol.Goal := do
@ -519,6 +517,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
    return {
      name := goal.name.toString,
      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
      target := (← serializeExpression options (← instantiate mvarDecl.type)),
      vars := vars.reverse.toArray
    }
@ -528,20 +527,17 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
 protected def GoalState.serializeGoals
      (state: GoalState)
      (parent: Option GoalState := .none)
      (options: @&Protocol.Options := {}):
    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
  goals.mapM fun goal => do
    let fragment := match state.fragments[goal]? with
      | .none => .tactic
      | .some $ .calc .. => .calc
      | .some $ .conv .. => .conv
      | .some $ .convSentinel .. => .conv
    match state.mctx.findDecl? goal with
    | .some mvarDecl =>
-      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
-      pure { serializedGoal with fragment }
+      pure serializedGoal
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 /-- Print the metavariables in a readable format -/
@ -607,9 +603,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
-    parentHasMVar (mvarId: MVarId): Bool := match parent? with
+    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
      | .some state => state.mctx.decls.contains mvarId
      | .none => true
 initialize
  registerTraceClass `Pantograph.Delate
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -4,7 +4,6 @@ import Pantograph.Protocol
 import Pantograph.Serial
 import Lean.Environment
 import Lean.Replay
 import Lean.Util.Path
 open Lean
 open Pantograph
@ -131,19 +130,17 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
      } }
    | _ => pure core
  let result ← if args.source?.getD false then
-      try
+      let srcSearchPath ← initSrcSearchPath
-        let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
+      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? := sourceUri?.map (toString ·),
+        sourceUri?,
        sourceStart?,
        sourceEnd?,
      }
      catch _e =>
        .pure result
    else
      .pure result
  return result
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -10,68 +10,24 @@ import Lean
 namespace Pantograph
 open Lean
 /-- The acting area of a tactic -/
 inductive Site where
  -- Dormant all other goals
  | focus (goal : MVarId)
  -- Move the goal to the first in the list
  | prefer (goal : MVarId)
  -- Execute as-is, no goals go dormant
  | unfocus
  deriving BEq, Inhabited
 instance : Coe MVarId Site where
  coe := .focus
 instance : ToString Site where
  toString
    | .focus { name } => s!"[{name}]"
    | .prefer { name } => s!"[{name},...]"
    | .unfocus => "[*]"
 /-- Executes a `TacticM` on a site and return affected goals -/
 protected def Site.runTacticM (site : Site)
  { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m] [MonadMCtx m] [MonadError m]
  (f : m α) : m (α × List MVarId) :=
  match site with
  | .focus goal => do
    Elab.Tactic.setGoals [goal]
    let a ← f
    return (a, [goal])
  | .prefer goal => do
    let before ← Elab.Tactic.getUnsolvedGoals
    let otherGoals := before.filter (· != goal)
    Elab.Tactic.setGoals (goal :: otherGoals)
    let a ← f
    let after ← Elab.Tactic.getUnsolvedGoals
    let parents := before.filter (¬ after.contains ·)
    Elab.Tactic.pruneSolvedGoals
    return (a, parents)
  | .unfocus => do
    let before ← Elab.Tactic.getUnsolvedGoals
    let a ← f
    let after ← Elab.Tactic.getUnsolvedGoals
    let parents := before.filter (¬ after.contains ·)
    Elab.Tactic.pruneSolvedGoals
    return (a, parents)
 /--
-Kernel view of the state of a proof
+Represents an interconnected set of metavariables, or a state in proof search
 -/
 structure GoalState where
  -- Captured `TacticM` state
  savedState : Elab.Tactic.SavedState
-  -- The root goal which is the search target
+  -- The root hole which is the search target
  root: MVarId
-  -- Parent goals assigned to produce this state
+  -- Parent state metavariable source
-  parentMVars : List MVarId := []
+  parentMVar?: Option MVarId
-  -- Any goal associated with a fragment has a partial tactic which has not
+  -- Existence of this field shows that we are currently in `conv` mode.
-  -- finished executing.
+  -- (convRhs, goal, dormant)
-  fragments : FragmentMap := .empty
+  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
-
+  -- Previous RHS for calc, so we don't have to repeat it every time
-def throwNoGoals { m α } [Monad m] [MonadError m] : m α := throwError "no goals to be solved"
+  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
  calcPrevRhs?: Option (MVarId × Expr) := .none
@[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@ -86,6 +42,7 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
  return {
    root := root.mvarId!,
    savedState,
    parentMVar? := .none,
  }
@[export pantograph_goal_state_create_from_mvars_m]
 protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
@ -94,19 +51,13 @@ protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): Met
  return {
    root,
    savedState,
    parentMVar? := .none,
  }
-@[always_inline]
+@[export pantograph_goal_state_is_conv]
 protected def GoalState.isConv (state: GoalState): Bool :=
  state.convMVar?.isSome
 protected def GoalState.goals (state: GoalState): List MVarId :=
  state.savedState.tactic.goals
@[always_inline]
 protected def GoalState.mainGoal? (state : GoalState) : Option MVarId :=
  state.goals.head?
@[always_inline]
 protected def GoalState.actingGoal? (state : GoalState) (site : Site) : Option MVarId := do
  match site with
  | .focus goal | .prefer goal => return goal
  | .unfocus => state.mainGoal?
@[export pantograph_goal_state_goals]
 protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
@ -118,10 +69,8 @@ protected def GoalState.env (state: GoalState): Environment :=
 protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
  let mvarDecl ← state.mctx.findDecl? mvarId
  return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
@[always_inline]
 protected def GoalState.metaState (state: GoalState): Meta.State :=
  state.savedState.term.meta.meta
@[always_inline]
 protected def GoalState.coreState (state: GoalState): Core.SavedState :=
  state.savedState.term.meta.core
@ -129,18 +78,18 @@ protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: Met
  mvarId.withContext m |>.run' (← read) state.metaState
 protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
  Meta.mapMetaM <| state.withContext' mvarId
 /-- Uses context of the first parent -/
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.parentMVars[0]!
+  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
  Meta.mapMetaM <| state.withContext' state.root
-private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
+private def GoalState.mvars (state: GoalState): SSet MVarId :=
-  modifyGetThe Core.State (fun st => ((),
+  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
 -- Restore the name generator and macro scopes of the core state
-protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
-  restoreCoreMExtra state.coreState
+  let savedCore := state.coreState
  modifyGetThe Core.State (fun st => ((),
    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
  state.restoreCoreMExtra
  state.savedState.term.meta.restore
@ -151,13 +100,42 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
  state.restoreElabM
  Elab.Tactic.setGoals [goal]
@[export pantograph_goal_state_focus]
 protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
  let goal ← state.savedState.tactic.goals[goalId]?
  return {
    state with
    savedState := {
      state.savedState with
      tactic := { goals := [goal] },
    },
    calcPrevRhs? := .none,
  }
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
  -- Prune parents solved goals
  let mctx := state.mctx
  let parentGoals := parent.goals.filter λ goal =>
    let isDuplicate := state.goals.contains goal
    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
    (¬ isDuplicate) && (¬ isSolved)
  {
    state with
    savedState := {
      state.savedState with
      tactic := { goals := state.goals ++ parentGoals },
    },
  }
 /--
-Brings into scope a list of goals. User must ensure `goals` are distinct.
+Brings into scope a list of goals. User must ensure `goals` is distinct.
 -/
@[export pantograph_goal_state_resume]
 protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
-  if ¬ (goals.all (state.mctx.decls.contains ·)) then
+  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
-    let invalid_goals := goals.filter (λ goal => ¬ state.mctx.decls.contains goal) |>.map (·.name.toString)
+    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
    .error s!"Goals {invalid_goals} are not in scope"
  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
  let unassigned := goals.filter λ goal =>
@ -195,219 +173,27 @@ protected def GoalState.isSolved (goalState : GoalState) : Bool :=
    | .some e => ¬ e.hasExprMVar
    | .none => true
  goalState.goals.isEmpty && solvedRoot
@[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
  let parent ← goalState.parentMVar?
  let expr := goalState.mctx.eAssignment.find! parent
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
  return expr
@[export pantograph_goal_state_get_mvar_e_assignment]
 protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
  let expr ← goalState.mctx.eAssignment.find? mvarId
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
  return expr
@[export pantograph_goal_state_parent_exprs]
 protected def GoalState.parentExprs (state : GoalState) : List Expr :=
  state.parentMVars.map λ goal => state.getMVarEAssignment goal |>.get!
@[always_inline]
 protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
  state.parentMVars.length == 1
@[always_inline]
 protected def GoalState.parentExpr! (state : GoalState) : Expr :=
  assert! state.parentMVars.length == 1
  (state.getMVarEAssignment state.parentMVars[0]!).get!
 deriving instance BEq for DelayedMetavarAssignment
 /-- Given states `dst`, `src`, and `src'`, where `dst` and `src'` are
 descendants of `src`, replay the differential `src' - src` in `dst`. Colliding
 metavariable and lemma names will be automatically renamed to ensure there is no
 collision. This implements branch unification. Unification might be impossible
 if conflicting assignments exist. We also assume the monotonicity property: In a
 chain of descending goal states, a mvar cannot be unassigned, and once assigned
 its assignment cannot change. -/
@[export pantograph_goal_state_replay_m]
 protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState :=
  withTraceNode `Pantograph.GoalState.replay (fun _ => return m!"replay") do
  let srcNGen := src.coreState.ngen
  let srcNGen' := src'.coreState.ngen
  let dstNGen := dst.coreState.ngen
  assert! srcNGen.namePrefix == srcNGen'.namePrefix
  assert! srcNGen.namePrefix == dstNGen.namePrefix
  assert! src.mctx.depth == src'.mctx.depth
  assert! src.mctx.depth == dst.mctx.depth
  let diffNGenIdx := dst.coreState.ngen.idx - srcNGen.idx
  trace[Pantograph.GoalState.replay] "Merging ngen {srcNGen.idx} -> ({srcNGen'.idx}, {dstNGen.idx})"
  -- True if the name is generated after `src`
  let isNewName : Name → Bool
    | .num pref n =>
      pref == srcNGen.namePrefix ∧ n ≥ srcNGen.idx
    | _ => false
  let mapId : Name → Name
    | id@(.num pref n) =>
      if isNewName id then
        .num pref (n + diffNGenIdx)
      else
        id
    | id => id
  let mapMVar : MVarId → MVarId
    | { name } => ⟨mapId name⟩
  let rec mapLevel : Level → Level
    | .succ x => .succ (mapLevel x)
    | .max l1 l2 => .max (mapLevel l1) (mapLevel l2)
    | .imax l1 l2 => .imax (mapLevel l1) (mapLevel l2)
    | .mvar { name } => .mvar ⟨mapId name⟩
    | l => l
  let mapExpr (e : Expr) : CoreM Expr := Core.transform e λ
    | .sort level => pure $ .done $ .sort (mapLevel level)
    | .mvar { name } => pure $ .done $ .mvar ⟨mapId name⟩
    | _ => pure .continue
  let mapDelayedAssignment (d : DelayedMetavarAssignment) : CoreM DelayedMetavarAssignment := do
    let { mvarIdPending, fvars } := d
    return {
      mvarIdPending := mapMVar mvarIdPending,
      fvars := ← fvars.mapM mapExpr,
    }
  let mapLocalDecl (ldecl : LocalDecl) : CoreM LocalDecl := do
    let ldecl := ldecl.setType (← mapExpr ldecl.type)
    if let .some value := ldecl.value? then
      return ldecl.setValue (← mapExpr value)
    else
      return ldecl
  let { term := savedTerm@{ meta := savedMeta@{ core, meta := meta@{ mctx, .. } }, .. }, .. } := dst.savedState
  trace[Pantograph.GoalState.replay] "Merging mvars {src.mctx.mvarCounter} -> ({src'.mctx.mvarCounter}, {dst.mctx.mvarCounter})"
  let mctx := {
    mctx with
    mvarCounter := mctx.mvarCounter + (src'.mctx.mvarCounter - src.mctx.mvarCounter),
    lDepth := src'.mctx.lDepth.foldl (init := mctx.lDepth) λ acc lmvarId@{ name } depth =>
      if src.mctx.lDepth.contains lmvarId then
        acc
      else
        acc.insert ⟨mapId name⟩ depth
    decls := ← src'.mctx.decls.foldlM (init := mctx.decls) λ acc _mvarId@{ name } decl => do
      if decl.index < src.mctx.mvarCounter then
        return acc
      let mvarId := ⟨mapId name⟩
      let decl := {
        decl with
        lctx := ← decl.lctx.foldlM (init := .empty) λ acc decl => do
          let decl ← mapLocalDecl decl
          return acc.addDecl decl,
        type := ← mapExpr decl.type,
      }
      return acc.insert mvarId decl
    -- Merge mvar assignments
    userNames := src'.mctx.userNames.foldl (init := mctx.userNames) λ acc userName mvarId =>
      if acc.contains userName then
        acc
      else
        acc.insert userName mvarId,
    lAssignment := src'.mctx.lAssignment.foldl (init := mctx.lAssignment) λ acc lmvarId' l =>
      let lmvarId := ⟨mapId lmvarId'.name⟩
      if mctx.lAssignment.contains lmvarId then
        -- Skip the intersecting assignments for now
        acc
      else
        let l := mapLevel l
        acc.insert lmvarId l,
    eAssignment := ← src'.mctx.eAssignment.foldlM (init := mctx.eAssignment) λ acc mvarId' e => do
      let mvarId := ⟨mapId mvarId'.name⟩
      if mctx.eAssignment.contains mvarId then
        -- Skip the intersecting assignments for now
        return acc
      else
        let e ← mapExpr e
        return acc.insert mvarId e,
    dAssignment := ← src'.mctx.dAssignment.foldlM (init := mctx.dAssignment) λ acc mvarId' d => do
      let mvarId := ⟨mapId mvarId'.name⟩
      if mctx.dAssignment.contains mvarId then
        return acc
      else
        let d ← mapDelayedAssignment d
        return acc.insert mvarId d
  }
  let ngen := {
    core.ngen with
    idx := core.ngen.idx + (srcNGen'.idx - srcNGen.idx)
  }
  -- Merge conflicting lmvar and mvar assignments using `isDefEq`
  let savedMeta := {
    savedMeta with
    core := {
      core with
      ngen,
    }
    meta := {
      meta with
      mctx,
    }
  }
  let m : MetaM Meta.SavedState := Meta.withMCtx mctx do
    restoreCoreMExtra savedMeta.core
    savedMeta.restore
    for (lmvarId, l') in src'.mctx.lAssignment do
      if isNewName lmvarId.name then
        continue
      let .some l ← getLevelMVarAssignment? lmvarId | continue
      let l' := mapLevel l'
      trace[Pantograph.GoalState.replay] "Merging level assignments on {lmvarId.name}"
      unless ← Meta.isLevelDefEq l l' do
        throwError "Conflicting assignment of level metavariable {lmvarId.name}"
    for (mvarId, e') in src'.mctx.eAssignment do
      if isNewName mvarId.name then
        continue
      if ← mvarId.isDelayedAssigned then
        throwError "Conflicting assignment of expr metavariable (e != d) {mvarId.name}"
      let .some e ← getExprMVarAssignment? mvarId | continue
      let e' ← mapExpr e'
      trace[Pantograph.GoalState.replay] "Merging expr assignments on {mvarId.name}"
      unless ← Meta.isDefEq e e' do
        throwError "Conflicting assignment of expr metavariable (e != e) {mvarId.name}"
    for (mvarId, d') in src'.mctx.dAssignment do
      if isNewName mvarId.name then
        continue
      if ← mvarId.isAssigned then
        throwError "Conflicting assignment of expr metavariable (d != e) {mvarId.name}"
      let .some d ← getDelayedMVarAssignment? mvarId | continue
      trace[Pantograph.GoalState.replay] "Merging expr (delayed) assignments on {mvarId.name}"
      unless d == d' do
        throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}"
    Meta.saveState
  let goals := dst.savedState.tactic.goals ++
    src'.savedState.tactic.goals.map (⟨mapId ·.name⟩)
  let fragments ← src'.fragments.foldM (init := dst.fragments) λ acc mvarId' fragment' => do
    let mvarId := ⟨mapId mvarId'.name⟩
    let fragment ← fragment'.map mapExpr
    if let .some _fragment0 := acc[mvarId]? then
      throwError "Conflicting fragments on {mvarId.name}"
    return acc.insert mvarId fragment
  return {
    dst with
    savedState := {
      tactic := {
        goals
      },
      term := {
        savedTerm with
        meta := ← m.run',
      },
    },
    parentMVars := dst.parentMVars ++ src.parentMVars.map mapMVar,
    fragments,
  }
 --- Tactic execution functions ---
 /--
 These descendants serve as "seed" mvars. If a MVarError's mvar is related 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. See the rationales document for the
 inspiration of this function.
 -/
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
 -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
  -- 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 _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
  let mut alreadyVisited : MVarIdSet := {}
@ -422,7 +208,6 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
        result := mvarDeps.foldl (·.insert ·) result
  return result.toList
 /-- Merger of two unique lists -/
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
  let li2' := li2.filter (¬ li1.contains ·)
  li1 ++ li2'
@ -432,29 +217,25 @@ Set `guardMVarErrors` to true to capture mvar errors. Lean will not
 automatically collect mvars from text tactics (vide
 `test_tactic_failure_synthesize_placeholder`)
 -/
-protected def GoalState.step' { α } (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
+protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
-  : Elab.TermElabM (α × GoalState) := do
+  : Elab.TermElabM GoalState := do
-  let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
+  unless (← getMCtx).decls.contains goal do
-    |>.run { elaborator := .anonymous }
+    throwError s!"Goal is not in context: {goal.name}"
-    |>.run state.savedState.tactic
+  goal.checkNotAssigned `GoalState.step
  let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
  let nextElabState ← MonadBacktrack.saveState
  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let goals ← if guardMVarErrors then
-      parentMVars.foldlM (init := goals) λ goals parent => do
+      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
        let errors ← collectAllErroredMVars parent
        return mergeMVarLists goals errors
    else
      pure goals
-  let state' := {
+  return {
    state with
    savedState := { term := nextElabState, tactic := { goals }, },
-    parentMVars,
+    parentMVar? := .some goal,
    calcPrevRhs? := .none,
  }
  return (a, state')
 protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
  : Elab.TermElabM GoalState :=
  Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors
 /-- Response for executing a tactic -/
 inductive TacticResult where
@ -467,80 +248,66 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message : String)
-private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array String) := do
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
  let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
  let hasErrors := newMessages.any (·.severity == .error)
  let newMessages ← newMessages.mapM λ m => m.toString
  Core.resetMessageLog
  return (hasErrors, newMessages.toArray)
-/-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
-def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
+protected def GoalState.tryTacticM
-  assert! (← Core.getMessageLog).toList.isEmpty
+    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
    (guardMVarErrors : Bool := false)
    : Elab.TermElabM TacticResult := do
  let prevMessageLength := state.coreState.messages.toList.length
  try
-    let state ← elabM
+    let nextState ← state.step goal tacticM guardMVarErrors
    -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog
+    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
    if hasError then
      return .failure newMessages
    else
-      return .success state newMessages
+      return .success nextState newMessages
  catch exception =>
    match exception with
    | .internal _ =>
-      let (_, messages) ← dumpMessageLog
+      let (_, messages) ← dumpMessageLog prevMessageLength
      return .failure messages
    | _ => return .failure #[← exception.toMessageData.toString]
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
    (state: GoalState) (site : Site)
    (tacticM: Elab.Tactic.TacticM Unit)
    (guardMVarErrors : Bool := false)
    : Elab.TermElabM TacticResult :=
  withCapturingError do
    state.step site tacticM guardMVarErrors
 /-- Execute a string tactic on given state. Restores TermElabM -/
@[export pantograph_goal_state_try_tactic_m]
-protected def GoalState.tryTactic (state: GoalState) (site : Site) (tactic: String):
+protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
    Elab.TermElabM TacticResult := do
  state.restoreElabM
  let .some goal := state.actingGoal? site | throwNoGoals
  if let .some fragment := state.fragments[goal]? then
    return ← withCapturingError do
      let (fragments, state') ← state.step' site do
        fragment.step goal tactic $ state.fragments.erase goal
      return { state' with fragments }
  -- Normal tactic without fragment
  let tactic ← match Parser.runParserCategory
-    (env := ← getEnv)
+    (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
+    (catName := if state.isConv then `conv else `tactic)
    (input := tactic)
    (fileName := ← getFileName) with
    | .ok stx => pure $ stx
    | .error error => return .parseError error
-  let tacticM := Elab.Tactic.evalTactic tactic
+  assert! ¬ (← goal.isAssigned)
-  withCapturingError do
+  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
    state.step site tacticM (guardMVarErrors := true)
-- Specialized Tactics
+protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
-
+      Elab.TermElabM TacticResult := do
 protected def GoalState.tryAssign (state : GoalState) (site : Site) (expr : String)
    : Elab.TermElabM TacticResult := do
  state.restoreElabM
  let expr ← match Parser.runParserCategory
-    (env := ← getEnv)
+    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := expr)
    (fileName := ← getFileName) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.tryTacticM site $ Tactic.evalAssign expr
+  state.tryTacticM goal $ Tactic.evalAssign expr
-protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : String) (type : String)
+-- Specialized Tactics
-    : Elab.TermElabM TacticResult := do
+
 protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  let type ← match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
@ -549,56 +316,150 @@ protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : S
    (fileName := ← getFileName) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.tryTacticM site $ Tactic.evalLet binderName.toName type
+  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
 /-- Enter conv tactic mode -/
-@[export pantograph_goal_state_conv_enter_m]
+protected def GoalState.conv (state: GoalState) (goal: MVarId):
 protected def GoalState.convEnter (state : GoalState) (site : Site) :
      Elab.TermElabM TacticResult := do
-  let .some goal := state.actingGoal? site | throwNoGoals
+  if state.convMVar?.isSome then
  if let .some (.conv ..) := state.fragments[goal]? then
    return .invalidAction "Already in conv state"
-  withCapturingError do
+  goal.checkNotAssigned `GoalState.conv
-    let (fragments, state') ← state.step' site Fragment.enterConv
+  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
-    return {
+    state.restoreTacticM goal
      state' with
      fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
        acc.insert goal fragment
    }
-/-- Exit from a tactic fragment. -/
+    -- See Lean.Elab.Tactic.Conv.convTarget
-@[export pantograph_goal_state_fragment_exit_m]
+    let convMVar ← Elab.Tactic.withMainContext do
-protected def GoalState.fragmentExit (state : GoalState) (site : Site):
+      let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
      Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
      pure rhs.mvarId!
    return (← MonadBacktrack.saveState, convMVar)
  try
    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
    -- Other goals are now dormant
    let otherGoals := state.goals.filter $ λ g => g != goal
    return .success {
      root := state.root,
      savedState := nextSavedState
      parentMVar? := .some goal,
      convMVar? := .some (convRhs, goal, otherGoals),
      calcPrevRhs? := .none
    } #[]
  catch exception =>
    return .failure #[← exception.toMessageData.toString]
 /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
@[export pantograph_goal_state_conv_exit_m]
 protected def GoalState.convExit (state: GoalState):
      Elab.TermElabM TacticResult := do
-  let .some goal := state.actingGoal? site | throwNoGoals
+  let (convRhs, convGoal, _) ← match state.convMVar? with
-  let .some fragment := state.fragments[goal]? |
+    | .some mvar => pure mvar
-    return .invalidAction "Goal does not have a fragment"
+    | .none => return .invalidAction "Not in conv state"
-  withCapturingError do
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-    let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
+    -- Vide `Lean.Elab.Tactic.Conv.convert`
-    return {
+    state.savedState.restore
-      state' with
+
-      fragments,
+    -- Close all existing goals with `refl`
-    }
+    for mvarId in (← Elab.Tactic.getGoals) do
      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
    Elab.Tactic.pruneSolvedGoals
    unless (← Elab.Tactic.getGoals).isEmpty do
      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
    Elab.Tactic.setGoals [convGoal]
    let targetNew ← instantiateMVars (.mvar convRhs)
    let proof ← instantiateMVars (.mvar convGoal)
    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
    MonadBacktrack.saveState
  try
    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
    return .success {
      root := state.root,
      savedState := nextSavedState
      parentMVar? := .some convGoal,
      convMVar? := .none
      calcPrevRhs? := .none
    } #[]
  catch exception =>
    return .failure #[← exception.toMessageData.toString]
 protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
-  let .some (.calc prevRhs?) := state.fragments[goal]? | .none
+  let (mvarId, rhs) ← state.calcPrevRhs?
-  prevRhs?
+  if mvarId == goal then
    .some rhs
  else
    .none
@[export pantograph_goal_state_try_calc_m]
 protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  if state.convMVar?.isSome then
    return .invalidAction "Cannot initiate `calc` while in `conv` state"
  let `(term|$pred) ← match Parser.runParserCategory
    (env := state.env)
    (catName := `term)
    (input := pred)
    (fileName := ← getFileName) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  goal.checkNotAssigned `GoalState.tryCalc
  let calcPrevRhs? := state.calcPrevRhsOf? goal
  let decl ← goal.getDecl
  let target ← instantiateMVars decl.type
  let tag := decl.userName
  try
    goal.withContext do
-@[export pantograph_goal_state_calc_enter_m]
+    let mut step ← Elab.Term.elabType <| ← do
-protected def GoalState.calcEnter (state : GoalState) (site : Site)
+      if let some prevRhs := calcPrevRhs? then
-  : Elab.TermElabM TacticResult := do
+        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
-  let .some goal := state.actingGoal? site | throwNoGoals
+      else
-  if let .some _ := state.fragments[goal]? then
+        pure pred
    return .invalidAction "Goal already has a fragment"
  withCapturingError do
    let fragment := Fragment.enterCalc
    let fragments := state.fragments.insert goal fragment
    return {
      state with
      fragments,
    }
-initialize
+    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
-  registerTraceClass `Pantograph.GoalState.replay
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
    if let some prevRhs := calcPrevRhs? then
      unless ← Meta.isDefEqGuarded lhs prevRhs do
        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
    -- Creates a mvar to represent the proof that the calc tactic solves the
    -- current branch
    -- In the Lean `calc` tactic this is gobbled up by
    -- `withCollectingNewGoalsFrom`
    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
      (userName := tag ++ `calc)
    let mvarBranch := proof.mvarId!
    let mut proofType ← Meta.inferType proof
    let mut remainder? := Option.none
    -- The calc tactic either solves the main goal or leaves another relation.
    -- Replace the main goal, and save the new goal if necessary
    unless ← Meta.isDefEq proofType target do
      let rec throwFailed :=
        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
      let lastStep := mkApp2 r rhs rhs'
      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
      unless ← Meta.isDefEq proofType target do throwFailed
      remainder? := .some lastStepGoal.mvarId!
    goal.assign proof
    let goals := [ mvarBranch ] ++ remainder?.toList
    let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
    return .success {
      root := state.root,
      savedState := {
        term := ← MonadBacktrack.saveState,
        tactic := { goals },
      },
      parentMVar? := .some goal,
      calcPrevRhs?
    } #[]
  catch exception =>
    return .failure #[← exception.toMessageData.toString]
 end Pantograph
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -69,7 +69,7 @@ def createCoreContext (options: Array String): IO Core.Context := do
@[export pantograph_create_core_state]
 def createCoreState (imports: Array String): IO Core.State := do
  let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str.toName }))
+    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
    (loadExts := true)
@ -117,10 +117,10 @@ def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState :
@[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
-  runMetaM <| state.serializeGoals options
+  runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
  : CoreM Protocol.GoalPrintResult := runMetaM do
  state.restoreMetaM
@ -130,10 +130,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
        serializeExpression options (← instantiateAll expr)
    else
      pure .none
-  let parentExprs? ← if parentExprs then
+  let parent? ← if parentExpr then
-      .some <$> state.parentMVars.mapM λ parent => parent.withContext do
+      state.parentExpr?.mapM λ expr => state.withParentContext do
-        let val := state.getMVarEAssignment parent |>.get!
+        serializeExpression options (← instantiateAll expr)
        serializeExpression options (← instantiateAll val)
    else
      pure .none
  let goals ← if goals then
@ -149,7 +148,7 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
  let env ← getEnv
  return {
    root?,
-    parentExprs?,
+    parent?,
    goals,
    extraMVars,
    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
@ -158,26 +157,26 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bo
  }
@[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (site : Site) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
  let type ← match (← parseTermM type) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.restoreElabM
-  state.tryTacticM site $ Tactic.evalHave binderName.toName type
+  state.tryTacticM goal $ Tactic.evalHave binderName.toName type
@[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (site : Site) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
  let expr ← match (← parseTermM expr) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.restoreElabM
-  state.tryTacticM site $ Tactic.evalDefine binderName.toName expr
+  state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
@[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (site : Site) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
  let expr ← match (← parseTermM expr) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.restoreElabM
-  state.tryTacticM site $ Tactic.evalDraft expr
+  state.tryTacticM goal (Tactic.evalDraft expr)
 -- Cancel the token after a timeout.
@[export pantograph_run_cancel_token_with_timeout_m]
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -60,17 +60,12 @@ structure Variable where
  type?: Option Expression  := .none
  value?: Option Expression := .none
  deriving Lean.ToJson
 inductive Fragment where
  | tactic
  | conv
  | calc
  deriving BEq, DecidableEq, Repr, Lean.ToJson
 structure Goal where
  /-- Name of the metavariable -/
  name: String := ""
-  /-- User-facing name -/
+  /-- Name of the metavariable -/
  userName?: Option String  := .none
-  fragment : Fragment := .tactic
+  /-- Is the goal in conversion mode -/
  isConversion: Bool        := false
  /-- target expression type -/
  target: Expression
  /-- Variables -/
@ -92,7 +87,6 @@ structure InteractionError where
  deriving Lean.ToJson
 def errorIndex (desc: String): InteractionError := { error := "index", desc }
 def errorOperation (desc: String): InteractionError := { error := "operation", desc }
 def errorExpr (desc: String): InteractionError := { error := "expr", desc }
@ -254,17 +248,17 @@ structure GoalStartResult where
  root: String
  deriving Lean.ToJson
 structure GoalTactic where
  -- Identifiers for tree, state, and goal
  stateId: Nat
-  -- If omitted, act on the first goal
+  goalId: Nat := 0
  goalId?: Option Nat := .none
  -- If set to true, goal will not go dormant. Defaults to `automaticMode`
  autoResume?: Option Bool := .none
  -- One of the fields here must be filled
  tactic?: Option String := .none
  mode?: Option String := .none -- Changes the current category to {"tactic", "calc", "conv"}
  expr?: Option String := .none
  have?: Option String := .none
  let?: Option String := .none
  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
@ -314,8 +308,8 @@ structure GoalPrint where
  -- Print root?
  rootExpr?: Option Bool := .some False
-  -- Print the parent expressions
+  -- Print the parent expr?
-  parentExprs?: Option Bool := .some False
+  parentExpr?: Option Bool := .some False
  -- Print goals?
  goals?: Option Bool := .some False
  -- Print values of extra mvars?
@ -325,7 +319,7 @@ structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
  -- The filling expression of the parent goal
-  parentExprs?: Option (List Expression) := .none
+  parent?: Option Expression := .none
  goals: Array Goal := #[]
  extraMVars: Array Expression := #[]
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -103,8 +103,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
      tactic
    }
    root,
-    parentMVars,
+    parentMVar?,
-    fragments,
+    convMVar?,
    calcPrevRhs?,
  } := goalState
  Pantograph.pickle path (
    env.constants.map₂,
@ -115,8 +116,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :
    tactic,
    root,
-    parentMVars,
+    parentMVar?,
-    fragments,
+    convMVar?,
    calcPrevRhs?,
  )
@[export pantograph_goal_state_unpickle_m]
@ -131,8 +133,9 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    tactic,
    root,
-    parentMVars,
+    parentMVar?,
-    fragments,
+    convMVar?,
    calcPrevRhs?,
  ), region) ← Pantograph.unpickle (
    PHashMap Name ConstantInfo ×
@ -142,8 +145,9 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    Elab.Tactic.State ×
    MVarId ×
-    List MVarId ×
+    Option MVarId ×
-    FragmentMap
+    Option (MVarId × MVarId × List MVarId) ×
    Option (MVarId × Expr)
  ) path
  let env ← env.replay (Std.HashMap.ofList map₂.toList)
  let goalState := {
@ -162,8 +166,9 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
      tactic,
    },
    root,
-    parentMVars,
+    parentMVar?,
-    fragments,
+    convMVar?,
    calcPrevRhs?,
  }
  return (goalState, region)
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@ -1,3 +1,2 @@
 import Pantograph.Tactic.Assign
 import Pantograph.Tactic.Fragment
 import Pantograph.Tactic.Prograde
--- a/Pantograph/Tactic/Fragment.lean
+++ b/Pantograph/Tactic/Fragment.lean
@ -1,188 +0,0 @@
 /- Fragmented tactics are the tactics which can give incremental feedback and
 whose integrity as a block is crucial to its operation. e.g. `calc` or `conv`.
 Here, a unified system handles all fragments.
 Inside a tactic fragment, the parser category may be different. An incomplete
 fragmented tactic may not be elaboratable..
 In line with continuation/resumption paradigms, the exit function of a fragment
 tactic is responsible for resuming incomplete goals with fragments. For example,
 when a conversion tactic finishes, the sentinels should resume the root of the
 conversion tactic goal. The user cannot be expected to execute this resumption,
 since the root is automatically dormanted at the entry of the conversion tactic
 mode.
 -/
 import Lean.Meta
 import Lean.Elab
 open Lean
 namespace Pantograph
 inductive Fragment where
  | calc (prevRhs? : Option Expr)
  | conv (rhs : MVarId)
  -- This goal is spawned from a `conv`
  | convSentinel (parent : MVarId)
  deriving BEq, Inhabited
 abbrev FragmentMap := Std.HashMap MVarId Fragment
 def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2
 protected def FragmentMap.filter (map : FragmentMap) (pred : MVarId → Fragment → Bool) : FragmentMap :=
  map.fold (init := FragmentMap.empty) λ acc mvarId fragment =>
    if pred mvarId fragment then
      acc.insert mvarId fragment
    else
      acc
 protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr) : CoreM Fragment :=
  let mapMVar (mvarId : MVarId) : CoreM MVarId :=
    return (← mapExpr (.mvar mvarId)) |>.mvarId!
  match fragment with
  | .calc prevRhs? => return .calc (← prevRhs?.mapM mapExpr)
  | .conv rhs => do
    let rhs' ← mapMVar rhs
    return .conv rhs'
  | .convSentinel parent => do
    return .convSentinel (← mapMVar parent)
 protected def Fragment.enterCalc : Fragment := .calc .none
 protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
  let goal ← Elab.Tactic.getMainGoal
  goal.checkNotAssigned `GoalState.conv
  let (rhs, newGoal) ← goal.withContext do
    let target ← instantiateMVars (← goal.getType)
    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor target
    pure (rhs.mvarId!, newGoal.mvarId!)
  Elab.Tactic.replaceMainGoal [newGoal]
  return FragmentMap.empty
    |>.insert goal (.conv rhs)
    |>.insert newGoal (.convSentinel goal)
 protected partial def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
  : Elab.Tactic.TacticM FragmentMap :=
  match fragment with
  | .calc .. => do
    Elab.Tactic.setGoals [goal]
    return fragments.erase goal
  | .conv rhs => do
    let goals := (← Elab.Tactic.getGoals).filter λ descendant =>
      match fragments[descendant]? with
      | .some s => (.convSentinel goal) == s
      | _ => false -- Not a conv goal from this
    -- Close all existing goals with `refl`
    for mvarId in goals do
      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
    unless (← goals.filterM (·.isAssignedOrDelayedAssigned)).isEmpty do
      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (goals)}"
    -- Ensure the meta tactic runs on `goal` even if its dormant by forcing resumption
    Elab.Tactic.setGoals $ goal :: (← Elab.Tactic.getGoals)
    let targetNew ← instantiateMVars (.mvar rhs)
    let proof ← instantiateMVars (.mvar goal)
    Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
    -- Try to solve maiinline by rfl
    let mvarId ← Elab.Tactic.getMainGoal
    liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
    Elab.Tactic.pruneSolvedGoals
    return fragments.filter λ mvarId fragment =>
      !(mvarId == goal || fragment == .convSentinel goal)
  | .convSentinel parent =>
    let parentFragment := fragments[parent]!
    parentFragment.exit parent (fragments.erase goal)
 protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (map : FragmentMap)
  : Elab.Tactic.TacticM FragmentMap := goal.withContext do
  assert! ¬ (← goal.isAssigned)
  match fragment with
  | .calc prevRhs? => do
    let .ok stx := Parser.runParserCategory
      (env := ← getEnv)
      (catName := `term)
      (input := s)
      (fileName := ← getFileName) | throwError s!"Failed to parse calc element {s}"
    let `(term|$pred) := stx
    let decl ← goal.getDecl
    let target ← instantiateMVars decl.type
    let tag := decl.userName
    let mut step ← Elab.Term.elabType <| ← do
      if let some prevRhs := prevRhs? then
        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
      else
        pure pred
    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
    if let some prevRhs := prevRhs? then
      unless ← Meta.isDefEqGuarded lhs prevRhs do
        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
    -- Creates a mvar to represent the proof that the calc tactic solves the
    -- current branch
    -- In the Lean `calc` tactic this is gobbled up by
    -- `withCollectingNewGoalsFrom`
    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
      (userName := tag ++ `calc)
    let mvarBranch := proof.mvarId!
    let mut proofType ← Meta.inferType proof
    let mut remainder? := Option.none
    -- The calc tactic either solves the main goal or leaves another relation.
    -- Replace the main goal, and save the new goal if necessary
    unless ← Meta.isDefEq proofType target do
      let rec throwFailed :=
        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
      let lastStep := mkApp2 r rhs rhs'
      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
      unless ← Meta.isDefEq proofType target do throwFailed
      remainder? := .some lastStepGoal.mvarId!
    goal.assign proof
    let goals := [ mvarBranch ] ++ remainder?.toList
    Elab.Tactic.setGoals goals
    match remainder? with
    | .some goal => return map.erase goal |>.insert goal $ .calc (.some rhs)
    | .none => return map
  | .conv .. => do
    throwError "Direct operation on conversion tactic parent goal is not allowed"
  | fragment@(.convSentinel parent) => do
    assert! isLHSGoal? (← goal.getType) |>.isSome
    let tactic ← match Parser.runParserCategory
      (env := ← MonadEnv.getEnv)
      (catName := `conv)
      (input := s)
      (fileName := ← getFileName) with
      | .ok stx => pure $ stx
      | .error error => throwError error
    let oldGoals ← Elab.Tactic.getGoals
    -- Label newly generated goals as conv sentinels
    Elab.Tactic.evalTactic tactic
    let newConvGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
      -- conv tactic might generate non-conv goals
      if oldGoals.contains g then
        return false
      return isLHSGoal? (← g.getType) |>.isSome
    -- Conclude the conv by exiting the parent fragment if new goals is empty
    if newConvGoals.isEmpty then
      let hasSiblingFragment := map.fold (init := false) λ flag _ fragment =>
        if flag then
          true
        else match fragment with
          | .convSentinel parent' => parent == parent'
          | _ => false
      if ¬ hasSiblingFragment then
        -- This fragment must exist since we have conv goals
        let parentFragment := map[parent]!
        -- All descendants exhausted. Exit from the parent conv.
        return ← parentFragment.exit parent map
    return newConvGoals.foldl (init := map) λ acc g =>
      acc.insert g fragment
 end Pantograph
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,6 +1,6 @@
 namespace Pantograph
@[export pantograph_version]
-def version := "0.3.3"
+def version := "0.3.1"
 end Pantograph
--- a/Repl.lean
+++ b/Repl.lean
@ -97,77 +97,6 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
  }
  runCoreM $ termElabM.run' context state |>.run'
 section Goal
 def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
  let state ← getMainState
  let .some goalState := state.goalStates[args.stateId]? |
    Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
  let unshielded := args.autoResume?.getD state.options.automaticMode
  let site ← match args.goalId?, unshielded with
    | .some goalId, true => do
      let .some goal := goalState.goals[goalId]? |
        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
      pure (.prefer goal)
    | .some goalId, false => do
      let .some goal := goalState.goals[goalId]? |
        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
      pure (.focus goal)
    | .none, true => pure .unfocus
    | .none, false => do
      let .some goal := goalState.mainGoal? |
        Protocol.throw $ Protocol.errorIndex s!"No goals to be solved"
      pure (.focus goal)
  let nextGoalState?: Except _ TacticResult ← liftTermElabM do
    -- NOTE: Should probably use a macro to handle this...
    match args.tactic?, args.mode?, args.expr?, args.have?, args.let?, args.draft?  with
    | .some tactic, .none, .none, .none, .none, .none => do
      pure $ Except.ok $ ← goalState.tryTactic site tactic
    | .none, .some mode, .none, .none, .none, .none => match mode with
      | "tactic" => do -- Exit from the current fragment
        pure $ Except.ok $ ← goalState.fragmentExit site
      | "conv" => do
        pure $ Except.ok $ ← goalState.convEnter site
      | "calc" => do
        pure $ Except.ok $ ← goalState.calcEnter site
      | _ => pure $ .error $ Protocol.errorOperation s!"Invalid mode {mode}"
    | .none, .none, .some expr, .none, .none, .none => do
      pure $ Except.ok $ ← goalState.tryAssign site expr
    | .none, .none, .none, .some type, .none, .none => do
      let binderName := args.binderName?.getD ""
      pure $ Except.ok $ ← goalState.tryHave site binderName type
    | .none, .none, .none, .none, .some type, .none => do
      let binderName := args.binderName?.getD ""
      pure $ Except.ok $ ← goalState.tryLet site binderName type
    | .none, .none, .none, .none, .none, .some draft => do
      pure $ Except.ok $ ← goalState.tryDraft site draft
    | _, _, _, _, _, _ =>
      pure $ .error $ Protocol.errorOperation
        "Exactly one of {tactic, mode, expr, have, let, draft} must be supplied"
  match nextGoalState? with
  | .error error => Protocol.throw error
  | .ok (.success nextGoalState messages) => do
    let nextStateId ← newGoalState nextGoalState
    let parentExprs := nextGoalState.parentExprs
    let hasSorry := parentExprs.any (·.hasSorry)
    let hasUnsafe := parentExprs.any ((← getEnv).hasUnsafe ·)
    let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
    return {
      nextStateId? := .some nextStateId,
      goals? := .some goals,
      messages? := .some messages,
      hasSorry,
      hasUnsafe,
    }
  | .ok (.parseError message) =>
    return { messages? := .none, parseError? := .some message }
  | .ok (.invalidAction message) =>
    Protocol.throw $ errorI "invalid" message
  | .ok (.failure messages) =>
    return { messages? := .some messages }
 end Goal
 section Frontend
 structure CompilationUnit where
@ -296,6 +225,7 @@ def execute (command: Protocol.Command): MainM Json := do
    return toJson error
  where
  errorCommand := errorI "command"
  errorIndex := errorI "index"
  errorIO := errorI "io"
  -- Command Functions
  reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
@ -360,7 +290,7 @@ def execute (command: Protocol.Command): MainM Json := do
      | .some expr, .none => goalStartExpr expr |>.run
      | .none, .some copyFrom => do
        (match (← getEnv).find? <| copyFrom.toName with
-        | .none => return .error <| Protocol.errorIndex s!"Symbol not found: {copyFrom}"
+        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
        | .some cInfo => return .ok (← GoalState.create cInfo.type))
      | _, _ =>
        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
@ -369,14 +299,74 @@ def execute (command: Protocol.Command): MainM Json := do
    | .ok goalState =>
      let stateId ← newGoalState goalState
      return { stateId, root := goalState.root.name.toString }
  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.stateId]? |
      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
    let .some goal := goalState.goals[args.goalId]? |
      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
    let nextGoalState?: Except _ TacticResult ← liftTermElabM 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
        pure <| Except.ok <| ← goalState.tryTactic goal tactic
      | .none, .some expr, .none, .none, .none, .none, .none => do
        pure <| Except.ok <| ← goalState.tryAssign goal expr
      | .none, .none, .some type, .none, .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
        let binderName := args.binderName?.getD ""
        pure <| Except.ok <| ← goalState.tryLet goal binderName type
      | .none, .none, .none, .none, .some pred, .none, .none => do
        pure <| Except.ok <| ← goalState.tryCalc goal pred
      | .none, .none, .none, .none, .none, .some true, .none => do
        pure <| Except.ok <| ← goalState.conv goal
      | .none, .none, .none, .none, .none, .some false, .none => 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, let, calc, conv, draft} must be supplied"
        pure $ .error error
    match nextGoalState? with
    | .error error => Protocol.throw error
    | .ok (.success nextGoalState messages) => do
      let nextGoalState ← match state.options.automaticMode, args.conv? with
        | true, .none => do
          pure $ nextGoalState.immediateResume goalState
        | true, .some true => pure nextGoalState
        | true, .some false => do
          let .some (_, _, dormantGoals) := goalState.convMVar? |
            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
            Protocol.throw $ errorIO "Resuming known goals"
          pure result
        | false, _ => pure nextGoalState
      let nextStateId ← newGoalState nextGoalState
      let parentExpr := nextGoalState.parentExpr?.get!
      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
      return {
        nextStateId? := .some nextStateId,
        goals? := .some goals,
        messages? := .some messages,
        hasSorry := parentExpr.hasSorry,
        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
      }
    | .ok (.parseError message) =>
      return { messages? := .none, parseError? := .some message }
    | .ok (.invalidAction message) =>
      Protocol.throw $ errorI "invalid" message
    | .ok (.failure messages) =>
      return { messages? := .some messages }
  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
    let state ← getMainState
    let .some target := state.goalStates[args.target]? |
-      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.target}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
    let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
      | .some branchId, .none => do
        match state.goalStates[branchId]? with
-        | .none => Protocol.throw $ Protocol.errorIndex s!"Invalid state index {branchId}"
+        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
        | .some branch => pure $ target.continue branch
      | .none, .some goals =>
        let goals := goals.toList.map (λ n => { name := n.toName })
@ -399,11 +389,11 @@ def execute (command: Protocol.Command): MainM Json := do
  goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
    let result ← liftMetaM <| goalPrint
        goalState
        (rootExpr := args.rootExpr?.getD False)
-        (parentExprs := args.parentExprs?.getD False)
+        (parentExpr := args.parentExpr?.getD False)
        (goals := args.goals?.getD False)
        (extraMVars := args.extraMVars?.getD #[])
        (options := state.options)
@ -411,7 +401,7 @@ def execute (command: Protocol.Command): MainM Json := do
  goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.id]? |
-      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
    goalStatePickle goalState args.path
    return {}
  goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -69,8 +69,6 @@ end Condensed
 def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
 def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
  state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
 def TacticResult.toString : TacticResult → String
  | .success state _messages => s!".success ({state.goals.length} goals)"
@ -96,14 +94,12 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
  | .ok a            => return a
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
  runCoreMSeq env metaM.run'
-def runTermElabMInMeta { α } (termElabM: Elab.TermElabM α): MetaM α :=
+def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
  termElabM.run' (ctx := defaultElabContext)
 def runTermElabMInCore { α } (termElabM: Elab.TermElabM α): CoreM α :=
  (runTermElabMInMeta termElabM).run'
 def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
-def exprToStr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
+def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 def strToTermSyntax (s: String): CoreM Syntax := do
  let .ok stx := Parser.runParserCategory
@ -161,13 +157,6 @@ end Monadic
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
  IO LSpec.TestSeq :=
  runTermElabMSeq env $ runTest t
 def transformTestT { α } { μ μ' : Type → Type }
    [Monad μ] [Monad μ'] [MonadLiftT (ST IO.RealWorld) μ] [MonadLiftT (ST IO.RealWorld) μ']
    (tr : {β : Type} → μ β  → μ' β) (m : TestT μ α) : TestT μ' α := do
  let tests ← get
  let (a, tests) ← tr (β := α × LSpec.TestSeq) (m.run tests)
  set tests
  return a
 def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
  { userName, type }
@ -183,26 +172,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
    })).toArray
  }
 namespace Tactic
 /-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
 exercises the aux lemma generator. -/
 def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
  let type ← instantiateMVars type
  let value ← instantiateMVars value
  if type.hasExprMVar then
    throwError "Type has expression mvar"
  if value.hasExprMVar then
    throwError "value has expression mvar"
  let goal ← Elab.Tactic.getMainGoal
  goal.withContext do
  let name ← Meta.mkAuxLemma [] type value
  unless ← Meta.isDefEq type (← goal.getType) do
    throwError "Type provided is incorrect"
  goal.assign (.const name [])
 end Tactic
 end Test
 end Pantograph
--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@ -51,7 +51,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
    ("λ 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)"),
-    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"),
+    ("(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) =>
    let termElabM := do
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -30,6 +30,7 @@ def test_symbol_visibility: IO LSpec.TestSeq := do
  let entries: List (Name × Bool) := [
    ("Nat.add_comm".toName, false),
    ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
  ]
  let suite := entries.foldl (λ suites (symbol, target) =>
    let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
@ -95,10 +96,10 @@ def test_symbol_location (env : Environment) : TestT IO Unit := do
    -- Extraction of source doesn't work for symbols in `Init` for some reason
    checkTrue "file" result.sourceUri?.isNone
-    checkEq "sourceStart" (result.sourceStart?.map (·.column)) <| .some 0
+    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88
+    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
-    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero", "Init.Grind.Tactics"]
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
    checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 def test_matcher (env : Environment) : TestT IO Unit := do
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -88,10 +88,10 @@ def test_tactic : Test := do
   ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
-  step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+  step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
   ({
     root? := .some { pp? := "fun x => ?m.11"},
-     parentExprs? := .some [{ pp? := .some "fun x => ?m.11" }],
+     parent? := .some { pp? := .some "fun x => ?m.11" },
   }: Protocol.GoalPrintResult)
  step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
@ -104,7 +104,7 @@ example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
  simp
 def test_tactic_timeout : Test := do
  step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.355" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult)
  -- timeout of 10 milliseconds
  step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
   ({ }: Protocol.OptionsSetResult)
@ -277,9 +277,9 @@ def test_frontend_process_sorry : Test := do
 def test_import_open : Test := do
  let header := "import Init\nopen Nat\nuniverse u"
  let goal1: Protocol.Goal := {
-    name := "_uniq.77",
+    name := "_uniq.67",
    target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.76", userName := "n", type? := .some { pp? := .some "Nat" }}],
+    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
  }
  step "frontend.process"
    ({
@ -294,7 +294,7 @@ def test_import_open : Test := do
     ],
   }: Protocol.FrontendProcessResult)
  step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.75" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult)
  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
   ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
  step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -55,7 +55,6 @@ def main (args: List String) := do
    ("Delate", Delate.suite),
    ("Serial", Serial.suite),
    ("Tactic/Assign", Tactic.Assign.suite),
    ("Tactic/Fragment", Tactic.Fragment.suite),
    ("Tactic/Prograde", Tactic.Prograde.suite),
    ("Tactic/Special", Tactic.Special.suite),
  ]
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -25,8 +25,8 @@ def test_instantiate_mvar: TestM Unit := do
      addTest $ assertUnreachable e
      return ()
  let t ← Lean.Meta.inferType expr
-  checkEq "typing" (toString (← serializeExpressionSexp t))
+  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
-    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
  return ()
 def startProof (expr: String): TestM (Option GoalState) := do
@ -118,9 +118,8 @@ def test_m_couple_simp: TestM Unit := do
  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
  let n := state1.goals[2]!
  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
-    #[#[toString n.name], #[toString n.name], #[]])
+    #[#["_uniq.38"], #["_uniq.38"], #[]])
  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
    | .success state _ => pure state
@ -159,10 +158,10 @@ def test_m_couple_simp: TestM Unit := do
      addTest $ assertUnreachable "(5 root)"
      return ()
  let rootStr: String := toString (← Lean.Meta.ppExpr root)
-  checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
  let unfoldedRoot ←  unfoldAuxLemmas root
-  checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
+  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
-    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
  return ()
 def test_proposition_generation: TestM Unit := do
@ -253,33 +252,20 @@ def test_partial_continuation: TestM Unit := do
      addTest $ assertUnreachable $ msg
      return ()
    | .ok state => pure state
-  checkEq "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?))
+  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
  -- Continuation should fail if the state does not exist:
  match state0.resume coupled_goals with
-  | .error error => checkEq "(continuation failure message)" error "Goals [_uniq.44, _uniq.45, _uniq.42, _uniq.51] are not in scope"
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
-  | .ok _ => fail "(continuation should fail)"
+  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
  -- Continuation should fail if some goals have not been solved
  match state2.continue state1 with
-  | .error error => checkEq "(continuation failure message)" error "Target state has unresolved goals"
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
-  | .ok _ => fail "(continuation should fail)"
+  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
  return ()
 def test_branch_unification : TestM Unit := do
  let .ok rootTarget ← elabTerm (← `(term|∀ (p q : Prop), p → p ∧ (p ∨ q))) .none | unreachable!
  let state ← GoalState.create rootTarget
  let .success state _  ← state.tacticOn' 0 (← `(tactic|intro p q h)) | fail "intro failed to run"
  let .success state _  ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | fail "apply And.intro failed to run"
  let .success state1 _  ← state.tacticOn' 0 (← `(tactic|exact h)) | fail "exact h failed to run"
  let .success state2 _  ← state.tacticOn' 1 (← `(tactic|apply Or.inl)) | fail "apply Or.inl failed to run"
  checkEq "(state2 goals)" state2.goals.length 1
  let state' ← state2.replay state state1
  checkEq "(state' goals)" state'.goals.length 1
  let .success stateT _ ← state'.tacticOn' 0 (← `(tactic|exact h)) | fail "exact h failed to run"
  let .some root := stateT.rootExpr? | fail "Root expression must exist"
  checkEq "(root)" (toString $ ← Meta.ppExpr root) "fun p q h => ⟨h, Or.inl h⟩"
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  let tests := [
@ -287,8 +273,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("2 < 5", test_m_couple),
    ("2 < 5", test_m_couple_simp),
    ("Proposition Generation", test_proposition_generation),
-    ("Partial Continuation", test_partial_continuation),
+    ("Partial Continuation", test_partial_continuation)
    ("Branch Unification", test_branch_unification),
  ]
  tests.map (fun (name, test) => (name, proofRunner env test))
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -32,7 +32,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
    let expr ← parseSentence expr
    return .some $ ← GoalState.create (expr := expr)
-private def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
    (userName?: Option String := .none): Protocol.Goal :=
  {
    name,
@ -43,7 +43,7 @@ private def buildNamedGoal (name: String) (nameType: List (String × String)) (t
      type? := .some { pp? := .some x.snd },
    })).toArray
  }
-private def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
    Protocol.Goal :=
  {
    userName?,
@ -53,7 +53,7 @@ private def buildGoal (nameType: List (String × String)) (target: String) (user
      type? := .some { pp? := .some x.snd },
    })).toArray
  }
-private def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
  let coreContext: Lean.Core.Context ← createCoreContext #[]
@ -66,18 +66,18 @@ private def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.Te
    return a
 def test_identity: TestM Unit := do
-  let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
+  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
-  let state0 ← GoalState.create (expr := rootTarget)
+  let tactic := "intro p h"
-  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
+  let state1 ← match ← state0.tacticOn 0 tactic with
    | .success state _ => pure state
    | other => do
      fail other.toString
      return ()
  let inner := "_uniq.11"
-  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
    #[inner])
  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 -- Individual test cases
@ -117,6 +117,41 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
  return ()
 def test_delta_variable: TestM Unit := do
  let options: Protocol.Options := { noRepeat := true }
  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
  addTest $ LSpec.check "Start goal" state?.isSome
  let state0 ← match state? with
    | .some state => pure state
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
    #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
  return ()
  where
 -- Like `buildGoal` but allow certain variables to be elided.
  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
    {
      target := { pp? := .some target},
      vars := (nameType.map fun x => ({
        userName := x.fst,
        type? := x.snd.map (λ type => { pp? := type }),
      })).toArray
    }
 example (w x y z : Nat) (p : Nat → Prop)
        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
@ -177,8 +212,8 @@ def test_or_comm: TestM Unit := do
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
-  checkTrue "(0 parent)" state0.parentMVars.isEmpty
+  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
-  checkTrue "(0 root)" state0.rootExpr?.isNone
+  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
  let tactic := "intro p q h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
@ -202,11 +237,11 @@ def test_or_comm: TestM Unit := do
        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
      ]
    }])
-  checkTrue "(1 parent)" state1.hasUniqueParent
+  checkTrue "(1 parent)" state1.parentExpr?.isSome
  checkTrue "(1 root)" $ ¬ state1.isSolved
  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
  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
@ -221,11 +256,11 @@ def test_or_comm: TestM Unit := do
  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
    #[caseL, caseR])
-  checkTrue "(2 parent exists)" state2.hasUniqueParent
+  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
  checkTrue "(2 root)" $ ¬ state2.isSolved
  let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
  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}))"
@ -241,7 +276,7 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr!)
+    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}))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
@ -251,7 +286,7 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← instantiateAll state4_1.parentExpr!
+  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
@ -301,6 +336,193 @@ def test_or_comm: TestM Unit := do
      ]
    }
 example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
  intro a b c1 c2 h
  conv =>
    lhs
    congr
    . rw [Nat.add_comm]
    . rfl
  exact h
 def test_conv: TestM Unit := do
  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
  let state0 ← match state? with
    | .some state => pure state
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
  let tactic := "intro a b c1 c2 h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[interiorGoal [] "a + b + c1 = b + a + c2"])
  let state2 ← match ← state1.conv (state1.get! 0) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
  let convTactic := "rhs"
  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
  let convTactic := "lhs"
  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
  let convTactic := "congr"
  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[
      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
    ])
  let convTactic := "rw [Nat.add_comm]"
  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
  let convTactic := "rfl"
  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[])
  let state4_1 ← match state6_1.continue state4 with
    | .ok state => pure state
    | .error e => do
      addTest $ expectationFailure "continue" e
      return ()
  let convTactic := "rfl"
  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[])
  let state1_1 ← match ← state6.convExit with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  let tactic := "exact h"
  let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[])
  where
    h := "b + a + c1 = b + a + c2"
    interiorGoal (free: List (String × String)) (target: String) :=
      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
      buildGoal free target
 example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
  intro a b c d h1 h2
  calc a + b = b + c := by apply h1
    _ = c + d := by apply h2
 def test_calc: TestM Unit := do
  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
  let state0 ← match state? with
    | .some state => pure state
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
  let tactic := "intro a b c d h1 h2"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[interiorGoal [] "a + b = c + d"])
  let pred := "a + b = b + c"
  let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[
      interiorGoal [] "a + b = b + c" (.some "calc"),
      interiorGoal [] "b + c = c + d"
    ])
  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
  let tactic := "apply h1"
  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3 ← match state2m.continue state2 with
    | .ok state => pure state
    | .error e => do
      addTest $ expectationFailure "continue" e
      return ()
  let pred := "_ = c + d"
  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[
      interiorGoal [] "b + c = c + d" (.some "calc")
    ])
  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
  let tactic := "apply h2"
  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
  where
    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
      buildGoal free target userName?
 def test_tactic_failure_unresolved_goals : TestM Unit := do
  let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
  let state0 ← match state? with
@ -377,8 +599,11 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("identity", test_identity),
    ("Nat.add_comm", test_nat_add_comm false),
    ("Nat.add_comm manual", test_nat_add_comm true),
    ("Nat.add_comm delta", test_delta_variable),
    ("arithmetic", test_arith),
    ("Or.comm", test_or_comm),
    ("conv", test_conv),
    ("calc", test_calc),
    ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
    ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
    ("deconstruct", test_deconstruct),
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -7,6 +7,9 @@ open Lean
 namespace Pantograph.Test.Serial
 def tempPath : IO System.FilePath := do
  Prod.snd <$> IO.FS.createTempFile
 structure MultiState where
  coreContext : Core.Context
  env: Environment
@ -27,22 +30,22 @@ def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (
    set $ (← getThe LSpec.TestSeq) ++ tests
    return (a, state')
-def test_pickling_environment : TestM Unit := do
+def test_environment_pickling : TestM Unit := do
  let coreSrc : Core.State := { env := ← getEnv }
  let coreDst : Core.State := { env := ← getEnv }
  let name := `mystery
-  IO.FS.withTempFile λ _ envPicklePath => do
+  let envPicklePath ← tempPath
  let ((), _) ← runCoreM coreSrc do
    let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
    let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
-    let c := Declaration.defnDecl <| mkDefinitionValEx
+    let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
      (name := name)
      (levelParams := [])
      (type := type)
      (value := value)
-      (hints := mkReducibilityHintsRegularEx 1)
+      (hints := Lean.mkReducibilityHintsRegularEx 1)
-      (safety := .safe)
+      (safety := Lean.DefinitionSafety.safe)
      (all := [])
    addDecl c
    environmentPickle (← getEnv) envPicklePath
@ -53,10 +56,13 @@ def test_pickling_environment : TestM Unit := do
    let anotherName := `mystery2
    checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone
-def test_goal_state_simple : TestM Unit := do
+  IO.FS.removeFile envPicklePath
 def test_goal_state_pickling_simple : TestM Unit := do
  let coreSrc : Core.State := { env := ← getEnv }
  let coreDst : Core.State := { env := ← getEnv }
-  IO.FS.withTempFile λ _ statePath => do
+  let statePath ← tempPath
  let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
  let stateGenerate : MetaM GoalState := runTermElabMInMeta do
    GoalState.create type
@ -72,36 +78,13 @@ def test_goal_state_simple : TestM Unit := do
    let types ← metaM.run'
    checkTrue "Goals" $ types[0]!.equal type
-def test_pickling_env_extensions : TestM Unit := do
+  IO.FS.removeFile statePath
  let coreSrc : Core.State := { env := ← getEnv }
  let coreDst : Core.State := { env := ← getEnv }
  IO.FS.withTempFile λ _ statePath => do
  let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do
    let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
    let state ← GoalState.create e
    let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable!
    let goal := state.goals[0]!
    let (type, value) ← goal.withContext do
      let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
      let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
      pure (type, value)
    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
    let parentExpr := state1.parentExpr!
    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
    goalStatePickle state1 statePath
  let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
    let (state1, _) ← goalStateUnpickle statePath (← getEnv)
    let parentExpr := state1.parentExpr!
    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
  return ()
 structure Test where
  name : String
  routine: TestM Unit
-protected def Test.run (test: Test) (env: Environment) : IO LSpec.TestSeq := do
+protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do
  -- Create the state
  let state : MultiState := {
    coreContext := ← createCoreContext #[],
@ -112,11 +95,10 @@ protected def Test.run (test: Test) (env: Environment) : IO LSpec.TestSeq := do
  | .error e =>
    return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "")
-def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
+def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
  let tests: List Test := [
-    { name := "environment", routine := test_pickling_environment, },
+    { name := "environment_pickling", routine := test_environment_pickling, },
-    { name := "goal simple", routine := test_goal_state_simple, },
+    { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, },
    { name := "extensions", routine := test_pickling_env_extensions, },
  ]
  tests.map (fun test => (test.name, test.run env))
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -1,4 +1,3 @@
 import Test.Tactic.Assign
 import Test.Tactic.Fragment
 import Test.Tactic.Prograde
 import Test.Tactic.Special
--- a/Test/Tactic/Fragment.lean
+++ b/Test/Tactic/Fragment.lean
@ -1,312 +0,0 @@
 import Pantograph.Goal
 import Test.Common
 open Lean
 namespace Pantograph.Test.Tactic.Fragment
 private def buildGoal (nameType: List (String × String)) (target: String):
    Protocol.Goal :=
  {
    target := { pp? := .some target},
    vars := (nameType.map fun x => ({
      userName := x.fst,
      type? := .some { pp? := .some x.snd },
    })).toArray
  }
 abbrev TestM := TestT $ Elab.TermElabM
 example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
  intro a b c1 c2 h
  conv =>
    lhs
    congr
    . rw [Nat.add_comm]
    . rfl
  exact h
 def test_conv_simple: TestM Unit := do
  let rootTarget ← parseSentence "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2"
  let state0 ← GoalState.create rootTarget
  let tactic := "intro a b c1 c2 h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
    #[interiorGoal [] "a + b + c1 = b + a + c2"])
  let goalConv := state1.goals[0]!
  let state2 ← match ← state1.convEnter (state1.get! 0) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) =
    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }])
  let convTactic := "rhs"
  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) =
    #[{ interiorGoal [] "b + a + c2" with fragment := .conv }])
  let convTactic := "lhs"
  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) =
    #[{ interiorGoal [] "a + b + c1" with fragment := .conv }])
  let convTactic := "congr"
  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) =
    #[
      { interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" },
      { interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" }
    ])
  let convTactic := "rw [Nat.add_comm]"
  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) =
    #[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }])
  let convTactic := "rfl"
  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals).map (·.devolatilize) =
    #[])
  let state4_1 ← match state6_1.continue state4 with
    | .ok state => pure state
    | .error e => do
      addTest $ expectationFailure "continue" e
      return ()
  let convTactic := "rfl"
  let state1_1 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"  · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
    #[interiorGoal [] "b + a + c1 = b + a + c2"])
  checkEq "(fragments)" state1_1.fragments.size 0
  /-
  let state1_1 ← match ← state6.fragmentExit goalConv with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  -/
  let tactic := "exact h"
  let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← stateF.serializeGoals).map (·.devolatilize) =
    #[])
  where
    h := "b + a + c1 = b + a + c2"
    interiorGoal (free: List (String × String)) (target: String) :=
      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
      buildGoal free target
 example (p : Prop) (x y z : Nat) : p → (p → x = y) → x + z = y + z ∧ p := by
  intro hp hi
  apply And.intro
  conv =>
    rhs
    arg 1
    rw [←hi]
    rfl
    tactic => exact hp
  exact hp
 def test_conv_unshielded : TestM Unit := do
  let rootTarget ← parseSentence "∀ (p : Prop) (x y z : Nat), p → (p → x = y) → x + z = y + z ∧ p"
  let state ← GoalState.create rootTarget
  let tactic := "intro p x y z hp hi"
  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
  let tactic := "apply And.intro"
  let .success state _ ← state.tacticOn 0 tactic | fail "apply failed"
  let .success state _ ← state.convEnter (.prefer state.goals[0]!) | fail "Cannot enter conversion tactic mode"
  let .success state _ ← state.tryTactic .unfocus "rhs" | fail "rhs failed"
  let tactic := "arg 1"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
    #[
      { interiorGoal [] "y" with fragment := .conv },
      { interiorGoal [] "p" with userName? := "right", },
    ]
  let tactic := "rw [←hi]"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" state.goals.length 3
  let tactic := "rfl"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
    #[
      interiorGoal [] "p",
      { interiorGoal [] "p" with userName? := "right", },
    ]
  checkEq "(n goals)" state.goals.length 2
  checkEq "(fragments)" state.fragments.size 0
  let tactic := "exact hp"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  let tactic := "exact hp"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  let root? := state.rootExpr?
  checkTrue "root" root?.isSome
  where
  interiorGoal (free: List (String × String)) (target: String) :=
    let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free
    buildGoal free target
 example : ∀ (x y z w : Nat), y = z → x + z = w → x + y = w := by
  intro x y z w hyz hxzw
  conv =>
    lhs
    arg 2
    rw [hyz]
    rfl
  exact hxzw
 def test_conv_unfinished : TestM Unit := do
  let rootTarget ← parseSentence "∀ (x y z w : Nat), y = z → x + z = w → x + y = w"
  let state ← GoalState.create rootTarget
  let tactic := "intro x y z w hyz hxzw"
  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
  let convParent := state.goals[0]!
  let .success state _ ← state.convEnter (.prefer convParent) | fail "Cannot enter conversion tactic mode"
  let .success state _ ← state.tryTactic .unfocus "lhs" | fail "rhs failed"
  let tactic := "arg 2"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
    #[
      { interiorGoal [] "y" with fragment := .conv },
    ]
  let tactic := "rw [hyz]"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
    #[
      { interiorGoal [] "z" with fragment := .conv },
    ]
  checkTrue "  (fragment)" $ state.fragments.contains state.mainGoal?.get!
  checkTrue "  (fragment parent)" $ state.fragments.contains convParent
  checkTrue "  (main goal)" state.mainGoal?.isSome
  let tactic := "rfl"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
    #[
      interiorGoal [] "x + z = w",
    ]
  checkEq "(fragments)" state.fragments.size 0
  checkEq s!"  {tactic}" state.goals.length 1
  let tactic := "exact hxzw"
  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
  let root? := state.rootExpr?
  checkTrue "root" root?.isSome
  where
  interiorGoal (free: List (String × String)) (target: String) :=
    let free := [("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("w", "Nat"), ("hyz", "y = z"), ("hxzw", "x + z = w")] ++ free
    buildGoal free target
 example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
  intro a b c d h1 h2
  calc a + b = b + c := by apply h1
    _ = c + d := by apply h2
 def test_calc: TestM Unit := do
  let rootTarget ← parseSentence "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d"
  let state0 ← GoalState.create rootTarget
  let tactic := "intro a b c d h1 h2"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
    #[interiorGoal [] "a + b = c + d"])
  let pred := "a + b = b + c"
  let .success state1 _ ← state1.calcEnter state1.mainGoal?.get! | fail "Could not enter calc"
  let state2 ← match ← state1.tacticOn 0 pred with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) =
    #[
      { interiorGoal [] "a + b = b + c" with userName? := .some "calc" },
      { interiorGoal [] "b + c = c + d" with fragment := .calc },
    ])
  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
  let tactic := "apply h1"
  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  let state3 ← match state2m.continue state2 with
    | .ok state => pure state
    | .error e => do
      addTest $ expectationFailure "continue" e
      return ()
  let pred := "_ = c + d"
  let state4 ← match ← state3.tacticOn 0 pred with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals).map (·.devolatilize) =
    #[
      { interiorGoal [] "b + c = c + d" with userName? := .some "calc" },
    ])
  addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
  let tactic := "apply h2"
  let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
    | .success state _ => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  checkEq "(fragments)" state4m.fragments.size 0
  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
  where
    interiorGoal (free: List (String × String)) (target: String) :=
      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
      buildGoal free target
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  [
    ("conv simple", test_conv_simple),
    ("conv unshielded", test_conv_unshielded),
    ("conv unfinished", test_conv_unfinished),
    ("calc", test_calc),
  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 end Pantograph.Test.Tactic.Fragment
--- a/doc/repl.md
+++ b/doc/repl.md
@ -13,7 +13,7 @@ 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.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`
@ -28,19 +28,17 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
  Start a new proof from a given expression or symbol
-* `goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}`:
+* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
-  Execute a tactic string on a given goal site. The tactic is supplied as additional
+  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
-  key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
  - `{ "tactic": <tactic> }`: Executes a tactic in the current mode
  - `{ "mode": <mode> }`: Enter a different tactic mode. The permitted values
    are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must
    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
    to the previous `rhs`.
  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
-  - `{ "let": <expr>, "binderName": <name> }`: Execute `let` and creates a branch goal
+  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into
+    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
-    goals. Coupling is not allowed.
+    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.
  If the `goals` field does not exist, the tactic execution has failed. Read
  `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
@ -54,9 +52,9 @@ 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>], readHeader: <bool>, inheritEnv: <bool>, invocations:
-  <string>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
+  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
  Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": output-path`), the sorrys and type errors into goal states
+  (`"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`. Conditionally inherit the environment from executing the file.
--- a/flake.lock
+++ b/flake.lock
@ -5,11 +5,11 @@
        "nixpkgs-lib": "nixpkgs-lib"
      },
      "locked": {
-        "lastModified": 1749398372,
+        "lastModified": 1743550720,
-        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
        "owner": "hercules-ci",
        "repo": "flake-parts",
-        "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
        "type": "github"
      },
      "original": {
@ -44,11 +44,11 @@
        ]
      },
      "locked": {
-        "lastModified": 1750369222,
+        "lastModified": 1743534244,
-        "narHash": "sha256-KFFTVbciXUaHgeGN1yiaUtY88OLGU0gElXx5SfICDKg=",
+        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "015ecd25206734d582a1b15dd11eb10be35ca555",
+        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
        "type": "github"
      },
      "original": {
@ -59,11 +59,11 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1750151854,
+        "lastModified": 1743975612,
-        "narHash": "sha256-3za+1J9FifMetO7E/kwgyW+dp+8pPBNlWKfcBovnn6M=",
+        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
        "owner": "nixos",
        "repo": "nixpkgs",
-        "rev": "ad5c70bcc5cc5178205161b7a7d61a6e80f6d244",
+        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
        "type": "github"
      },
      "original": {
@ -75,11 +75,11 @@
    },
    "nixpkgs-lib": {
      "locked": {
-        "lastModified": 1748740939,
+        "lastModified": 1743296961,
-        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
+        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
        "owner": "nix-community",
        "repo": "nixpkgs.lib",
-        "rev": "656a64127e9d791a334452c6b6606d17539476e2",
+        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
        "type": "github"
      },
      "original": {
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.19.0
`@ -1 +1 @@`
	`leanprover/lean4:v4.20.1`	`leanprover/lean4:v4.19.0`