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 :=
-  match n with
-  | .str _ s => "_proof_".isPrefixOf s
-  | _ => false
+def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _

 /-- 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)
-      pure { serializedGoal with fragment }
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
+      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
-      | .some state => state.mctx.decls.contains mvarId
-      | .none => true
+    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD 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 sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
-        let declRange? ← findDeclarationRanges? name
-        let sourceStart? := declRange?.map (·.range.pos)
-        let sourceEnd? := declRange?.map (·.range.endPos)
-        .pure {
-          result with
-          sourceUri? := sourceUri?.map (toString ·),
-          sourceStart?,
-          sourceEnd?,
-        }
-      catch _e =>
-        .pure result
+      let srcSearchPath ← initSrcSearchPath
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
+      let declRange? ← findDeclarationRanges? name
+      let sourceStart? := declRange?.map (·.range.pos)
+      let sourceEnd? := declRange?.map (·.range.endPos)
+      .pure {
+        result with
+        sourceUri?,
+        sourceStart?,
+        sourceEnd?,
+      }
    else
      .pure result
  return 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
-  parentMVars : List MVarId := []
+  -- Parent state metavariable source
+  parentMVar?: Option MVarId

-  -- Any goal associated with a fragment has a partial tactic which has not
-  -- finished executing.
-  fragments : FragmentMap := .empty
-
-def throwNoGoals { m α } [Monad m] [MonadError m] : m α := throwError "no goals to be solved"
+  -- Existence of this field shows that we are currently in `conv` mode.
+  -- (convRhs, goal, dormant)
+  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
+  -- Previous RHS for calc, so we don't have to repeat it every time
+  -- 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 :=
-  modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen }))
+private def GoalState.mvars (state: GoalState): SSet MVarId :=
+  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
 -- Restore the name generator and macro scopes of the core state
-protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
-  restoreCoreMExtra state.coreState
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
+  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
-    let invalid_goals := goals.filter (λ goal => ¬ state.mctx.decls.contains goal) |>.map (·.name.toString)
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
+  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
+    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 =>
@ -174,7 +152,7 @@ protected def GoalState.resume (state : GoalState) (goals : List MVarId) : Excep
 Brings into scope all goals from `branch`
 -/
@[export pantograph_goal_state_continue]
-protected def GoalState.continue (target : GoalState) (branch : GoalState) : Except String GoalState :=
+protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
  if !target.goals.isEmpty then
    .error s!"Target state has unresolved goals"
  else if target.root != branch.root then
@ -183,7 +161,7 @@ protected def GoalState.continue (target : GoalState) (branch : GoalState) : Exc
    target.resume (goals := branch.goals)

@[export pantograph_goal_state_root_expr]
-protected def GoalState.rootExpr? (goalState : GoalState) : Option Expr := do
+protected def GoalState.rootExpr? (goalState : GoalState): Option Expr := do
  if goalState.root.name == .anonymous then
    .none
  let expr ← goalState.mctx.eAssignment.find? goalState.root
@ -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.
-/
+-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-  -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
+  -- 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)
-  : Elab.TermElabM (α × GoalState) := do
-  let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
-    |>.run { elaborator := .anonymous }
-    |>.run state.savedState.tactic
+protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+  : Elab.TermElabM GoalState := do
+  unless (← getMCtx).decls.contains goal do
+    throwError s!"Goal is not in context: {goal.name}"
+  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
-        let errors ← collectAllErroredMVars parent
-        return mergeMVarLists goals errors
+      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
    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` -/
-def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
-  assert! (← Core.getMessageLog).toList.isEmpty
+/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.tryTacticM
+    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (guardMVarErrors : Bool := false)
+    : Elab.TermElabM TacticResult := do
+  let prevMessageLength := state.coreState.messages.toList.length
  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)
-    (catName := `tactic)
+    (env := ← MonadEnv.getEnv)
+    (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
-  withCapturingError do
-    state.step site tacticM (guardMVarErrors := true)
+  assert! ¬ (← goal.isAssigned)
+  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true

-- Specialized Tactics
-
-protected def GoalState.tryAssign (state : GoalState) (site : Site) (expr : String)
-    : Elab.TermElabM TacticResult := do
+protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (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)
-    : Elab.TermElabM TacticResult := do
+-- Specialized Tactics
+
+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.convEnter (state : GoalState) (site : Site) :
+protected def GoalState.conv (state: GoalState) (goal: MVarId):
      Elab.TermElabM TacticResult := do
-  let .some goal := state.actingGoal? site | throwNoGoals
-  if let .some (.conv ..) := state.fragments[goal]? then
+  if state.convMVar?.isSome then
    return .invalidAction "Already in conv state"
-  withCapturingError do
-    let (fragments, state') ← state.step' site Fragment.enterConv
-    return {
-      state' with
-      fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
-        acc.insert goal fragment
-    }
+  goal.checkNotAssigned `GoalState.conv
+  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
+    state.restoreTacticM goal

-/-- Exit from a tactic fragment. -/
-@[export pantograph_goal_state_fragment_exit_m]
-protected def GoalState.fragmentExit (state : GoalState) (site : Site):
+    -- See Lean.Elab.Tactic.Conv.convTarget
+    let convMVar ← Elab.Tactic.withMainContext do
+      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 .some fragment := state.fragments[goal]? |
-    return .invalidAction "Goal does not have a fragment"
-  withCapturingError do
-    let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
-    return {
-      state' with
-      fragments,
-    }
+  let (convRhs, convGoal, _) ← match state.convMVar? with
+    | .some mvar => pure mvar
+    | .none => return .invalidAction "Not in conv state"
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
+    -- Vide `Lean.Elab.Tactic.Conv.convert`
+    state.savedState.restore

-protected def GoalState.calcPrevRhsOf? (state : GoalState) (goal : MVarId) : Option Expr := do
-  let .some (.calc prevRhs?) := state.fragments[goal]? | .none
-  prevRhs?
+    -- 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)}"

-@[export pantograph_goal_state_calc_enter_m]
-protected def GoalState.calcEnter (state : GoalState) (site : Site)
-  : Elab.TermElabM TacticResult := do
-  let .some goal := state.actingGoal? site | throwNoGoals
-  if let .some _ := state.fragments[goal]? then
-    return .invalidAction "Goal already has a fragment"
-  withCapturingError do
-    let fragment := Fragment.enterCalc
-    let fragments := state.fragments.insert goal fragment
-    return {
-      state with
-      fragments,
-    }
+    Elab.Tactic.setGoals [convGoal]

-initialize
-  registerTraceClass `Pantograph.GoalState.replay
+    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 (mvarId, rhs) ← state.calcPrevRhs?
+  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
+
+    let mut step ← Elab.Term.elabType <| ← do
+      if let some prevRhs := calcPrevRhs? 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 := 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
-      .some <$> state.parentMVars.mapM λ parent => parent.withContext do
-        let val := state.getMVarEAssignment parent |>.get!
-        serializeExpression options (← instantiateAll val)
+  let parent? ← if parentExpr then
+      state.parentExpr?.mapM λ expr => state.withParentContext do
+        serializeExpression options (← instantiateAll expr)
    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,21 +60,16 @@ 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: String := ""
  /-- Name of the metavariable -/
-  name : String := ""
-  /-- User-facing name -/
-  userName? : Option String  := .none
-  fragment : Fragment := .tactic
+  userName?: Option String  := .none
+  /-- Is the goal in conversion mode -/
+  isConversion: Bool        := false
  /-- target expression type -/
-  target : Expression
+  target: Expression
  /-- Variables -/
-  vars : Array Variable      := #[]
+  vars: Array Variable      := #[]
  deriving Lean.ToJson


@ -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?: Option Nat := .none
-  -- If set to true, goal will not go dormant. Defaults to `automaticMode`
-  autoResume?: Option Bool := .none
+  goalId: Nat := 0
  -- 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
-  parentExprs?: Option Bool := .some False
+  -- Print the parent expr?
+  parentExpr?: Option Bool := .some False
  -- Print goals?
  goals?: Option Bool := .some False
  -- Print values of extra mvars?
@ -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,
-    fragments,
+    parentMVar?,
+    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,
-    fragments,
+    parentMVar?,
+    convMVar?,
+    calcPrevRhs?,
  )

@[export pantograph_goal_state_unpickle_m]
@ -131,8 +133,9 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
    tactic,

    root,
-    parentMVars,
-    fragments,
+    parentMVar?,
+    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 ×
-    FragmentMap
+    Option MVarId ×
+    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,
-    fragments,
+    parentMVar?,
+    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 "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88
+    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
+    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))
-    "((: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)))"
+  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.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))
-    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+  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)))")
  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?))
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]
+  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.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"
-  | .ok _ => fail "(continuation should fail)"
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
+  | .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"
-  | .ok _ => fail "(continuation should fail)"
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
+  | .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),
-    ("Branch Unification", test_branch_unification),
+    ("Partial Continuation", test_partial_continuation)
  ]
  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 := rootTarget)
-  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
+  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
+  let tactic := "intro p h"
+  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
-  checkTrue "(0 root)" state0.rootExpr?.isNone
+  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.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)
-      (safety := .safe)
+      (hints := Lean.mkReducibilityHintsRegularEx 1)
+      (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
-  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 ()
+  IO.FS.removeFile statePath

 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 := "goal simple", routine := test_goal_state_simple, },
-    { name := "extensions", routine := test_pickling_env_extensions, },
+    { name := "environment_pickling", routine := test_environment_pickling, },
+    { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, },
  ]
  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>], ...}`:
-  Execute a tactic string on a given goal site. The tactic is supplied as additional
-  key-value pairs in one of the following formats:
-  - `{ "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`.
+* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
+  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
  - `{ "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
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into
-    goals. Coupling is not allowed.
+  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+    be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
+    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,
-        "narHash": "sha256-tYBdgS56eXYaWVW3fsnPQ/nFlgWi/Z2Ymhyu21zVM98=",
+        "lastModified": 1743550720,
+        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
        "owner": "hercules-ci",
        "repo": "flake-parts",
-        "rev": "9305fe4e5c2a6fcf5ba6a3ff155720fbe4076569",
+        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
        "type": "github"
      },
      "original": {
@ -44,11 +44,11 @@
        ]
      },
      "locked": {
-        "lastModified": 1750369222,
-        "narHash": "sha256-KFFTVbciXUaHgeGN1yiaUtY88OLGU0gElXx5SfICDKg=",
+        "lastModified": 1743534244,
+        "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,
-        "narHash": "sha256-3za+1J9FifMetO7E/kwgyW+dp+8pPBNlWKfcBovnn6M=",
+        "lastModified": 1743975612,
+        "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,
-        "narHash": "sha256-rQaysilft1aVMwF14xIdGS3sj1yHlI6oKQNBRTF40cc=",
+        "lastModified": 1743296961,
+        "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