20 changed files with 185 additions and 280 deletions
--- a/Main.lean
+++ b/Main.lean
@ -8,12 +8,6 @@ import Repl
 open Pantograph.Repl
 open Pantograph.Protocol

-/-- Print a string to stdout without buffering -/
-def printImmediate (s : String) : IO Unit := do
-  let stdout ← IO.getStdout
-  stdout.putStr (s ++ "\n")
-  stdout.flush
-
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
  match s.trim.get? 0 with
@ -40,27 +34,27 @@ partial def loop : MainM Unit := do repeat do
  | .error error =>
    let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
    -- Using `Lean.Json.compress` here to prevent newline
-    printImmediate error.compress
+    IO.println error.compress
  | .ok command =>
    try
      let ret ← execute command
      let str := match state.options.printJsonPretty with
        | true => ret.pretty
        | false => ret.compress
-      printImmediate str
+      IO.println str
    catch e =>
      let message := e.toString
      let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      printImmediate error.compress
+      IO.println error.compress

-def main (args: List String): IO Unit := do
+
+unsafe def main (args: List String): IO Unit := do
  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
  if args == ["--version"] then do
    IO.println s!"{Pantograph.version}"
    return

-  unsafe do
-    Pantograph.initSearch ""
+  Pantograph.initSearch ""

  -- Separate imports and options
  let (options, imports) := args.partition (·.startsWith "--")
@ -68,7 +62,7 @@ def main (args: List String): IO Unit := do
  let coreState ← Pantograph.createCoreState imports.toArray
  try
    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
-    printImmediate "ready."
+    IO.println "ready."
    mainM
  catch ex =>
    let message := ex.toString
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
  self e := instantiateDelayedMVars e

 /--
-Convert an expression to an equivalent form with
+Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas or matchers
 3. No assigned mvars
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@ -154,31 +154,33 @@ the draft tactic instead.
 -/
@[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
  assert! !sorrys.isEmpty
-  let goalsM := sorrys.mapM λ i => do
-    match i.info with
-    | .ofTermInfo termInfo  => do
-      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      if (← mvarId.getType).hasSorry then
-        throwError s!"Coupling is not allowed in drafting"
-      return [(mvarId, stxByteRange termInfo.stx)]
-    | .ofTacticInfo tacticInfo => do
-      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-      for mvarId in mvarIds do
+  withEnv env do
+    let goalsM := sorrys.mapM λ i => do
+      match i.info with
+      | .ofTermInfo termInfo  => do
+        let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
        if (← mvarId.getType).hasSorry then
          throwError s!"Coupling is not allowed in drafting"
-      let range := stxByteRange tacticInfo.stx
-      return mvarIds.map (·, range)
-    | _ => panic! "Invalid info"
-  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-  let goals := annotatedGoals.map Prod.fst
-  let srcBoundaries := annotatedGoals.map Prod.snd
-  let root := match goals with
-    | [] => panic! "No MVars generated"
-    | [g] => g
-    | _ => { name := .anonymous }
-  let state ← GoalState.createFromMVars goals root
-  return { state, srcBoundaries }
+        return [(mvarId, stxByteRange termInfo.stx)]
+      | .ofTacticInfo tacticInfo => do
+        let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+        for mvarId in mvarIds do
+          if (← mvarId.getType).hasSorry then
+            throwError s!"Coupling is not allowed in drafting"
+        let range := stxByteRange tacticInfo.stx
+        return mvarIds.map (·, range)
+      | _ => panic! "Invalid info"
+    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+    let goals := annotatedGoals.map Prod.fst
+    let srcBoundaries := annotatedGoals.map Prod.snd
+    let root := match goals with
+      | [] => panic! "No MVars generated"
+      | [g] => g
+      | _ => { name := .anonymous }
+    let state ← GoalState.createFromMVars goals root
+    return { state, srcBoundaries }


@[export pantograph_frontend_collect_new_defined_constants_m]
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@ -118,7 +118,6 @@ partial def translateLCtx : MetaTranslateM LocalContext := do

 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
  if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
-    trace[Pantograph.Frontend.MetaTranslate] "Existing mvar id {srcMVarId.name} → {mvarId'.name}"
    return mvarId'
  let mvarId' ← Meta.withLCtx .empty #[] do
    let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
@ -135,7 +134,6 @@ partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
          let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
          assignDelayedMVar mvarId' fvars' mvarIdPending'
        pure mvarId'
-  trace[Pantograph.Frontend.MetaTranslate] "Translated {srcMVarId.name} → {mvarId'.name}"
  addTranslatedMVar srcMVarId mvarId'
  return mvarId'
 end
@ -150,7 +148,6 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
    let lctx' ← translateLCtx
    let mvar ← Meta.withLCtx lctx' #[] do
      let type' ← translateExpr type
-      trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
      Meta.mkFreshExprSyntheticOpaqueMVar type'
    return mvar.mvarId!

--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -113,14 +113,11 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
  }

 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume]
+@[export pantograph_goal_state_immediate_resume_parent]
 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)
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
  {
    state with
    savedState := {
@ -130,24 +127,25 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
  }

 /--
-Brings into scope a list of goals. User must ensure `goals` is distinct.
+Brings into scope a list of goals
 -/
@[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
  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 =>
-    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
-    ¬ isSolved
-  return {
-    state with
-    savedState := {
-      term := state.savedState.term,
-      tactic := { goals := unassigned },
-    },
-  }
+  else
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+    let unassigned := goals.filter (λ goal =>
+      let mctx := state.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
+      state with
+      savedState := {
+        term := state.savedState.term,
+        tactic := { goals := unassigned },
+      },
+    }
 /--
 Brings into scope all goals from `branch`
 -/
@ -161,18 +159,18 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
    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
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
-@[export pantograph_goal_state_is_solved]
-protected def GoalState.isSolved (goalState : GoalState) : Bool :=
-  let solvedRoot := match goalState.rootExpr? with
-    | .some e => ¬ e.hasExprMVar
-    | .none => true
-  goalState.goals.isEmpty && solvedRoot
+  if expr.hasExprMVar then
+    -- Must not assert that the goal state is empty here. We could be in a branch goal.
+    --assert! ¬goalState.goals.isEmpty
+    .none
+  else
+    assert! goalState.goals.isEmpty
+    return expr
@[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
  let parent ← goalState.parentMVar?
@ -240,20 +238,23 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
 /-- Response for executing a tactic -/
 inductive TacticResult where
  -- Goes to next state
-  | success (state : GoalState) (messages : Array String)
+  | success (state: GoalState)
  -- Tactic failed with messages
-  | failure (messages : Array String)
+  | failure (messages: Array String)
  -- Could not parse tactic
-  | parseError (message : String)
+  | parseError (message: String)
  -- The given action cannot be executed in the state
-  | invalidAction (message : String)
+  | invalidAction (message: String)

-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
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
+  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
+    |>.filterMapM λ m => do
+      if m.severity == .error then
+        return .some $ ← m.toString
+      else
+        return .none
  Core.resetMessageLog
-  return (hasErrors, newMessages.toArray)
+  return newMessages.toArray

 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
@ -265,16 +266,13 @@ protected def GoalState.tryTacticM
    let nextState ← state.step goal tacticM guardMVarErrors

    -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
-    if hasError then
+    let newMessages ← dumpMessageLog prevMessageLength
+    if ¬ newMessages.isEmpty then
      return .failure newMessages
-    else
-      return .success nextState newMessages
+    return .success nextState
  catch exception =>
    match exception with
-    | .internal _ =>
-      let (_, messages) ← dumpMessageLog prevMessageLength
-      return .failure messages
+    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
    | _ => return .failure #[← exception.toMessageData.toString]

 /-- Execute a string tactic on given state. Restores TermElabM -/
@ -343,7 +341,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
      parentMVar? := .some goal,
      convMVar? := .some (convRhs, goal, otherGoals),
      calcPrevRhs? := .none
-    } #[]
+    }
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

@ -380,7 +378,7 @@ protected def GoalState.convExit (state: GoalState):
      parentMVar? := .some convGoal,
      convMVar? := .none
      calcPrevRhs? := .none
-    } #[]
+    }
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

@ -458,7 +456,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
      },
      parentMVar? := .some goal,
      calcPrevRhs?
-    } #[]
+    }
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -123,9 +123,8 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
  : CoreM Protocol.GoalPrintResult := runMetaM do
  state.restoreMetaM

-  let rootExpr? := state.rootExpr?
  let root? ← if rootExpr then
-      rootExpr?.mapM λ expr => state.withRootContext do
+      state.rootExpr?.mapM λ expr => state.withRootContext do
        serializeExpression options (← instantiateAll expr)
    else
      pure .none
@ -144,15 +143,11 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
    state.withContext mvarId do
      let .some expr ← getExprMVarAssignment? mvarId | return {}
      serializeExpression options (← instantiateAll expr)
-  let env ← getEnv
  return {
    root?,
    parent?,
    goals,
    extraMVars,
-    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
-    rootHasUnsafe := rootExpr?.map (env.hasUnsafe ·) |>.getD false,
-    rootHasMVar := rootExpr?.map (·.hasExprMVar) |>.getD false,
  }

@[export pantograph_goal_have_m]
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -268,17 +268,14 @@ structure GoalTactic where
 structure GoalTacticResult where
  -- The next goal state id. Existence of this field shows success
  nextStateId?: Option Nat          := .none
-  -- If the array is empty, it shows the goals have been fully resolved. If this
-  -- is .none, there has been a tactic error.
-  goals?: Option (Array Goal)       := .none
+  -- If the array is empty, it shows the goals have been fully resolved.
+  goals?: Option (Array Goal)          := .none

-  messages? : Option (Array String) := .some #[]
+  -- Existence of this field shows tactic execution failure
+  tacticErrors?: Option (Array String) := .none

  -- Existence of this field shows the tactic parsing has failed
-  parseError? : Option String       := .none
-
-  hasSorry : Bool := false
-  hasUnsafe : Bool := false
+  parseError?: Option String := .none
  deriving Lean.ToJson
 structure GoalContinue where
  -- State from which the continuation acquires the context
@ -322,10 +319,6 @@ structure GoalPrintResult where
  parent?: Option Expression := .none
  goals: Array Goal := #[]
  extraMVars: Array Expression := #[]
-
-  rootHasSorry : Bool := false
-  rootHasUnsafe : Bool := false
-  rootHasMVar : Bool := true
  deriving Lean.ToJson

 -- Diagnostic Options, not available in REPL
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,6 +1,6 @@
 namespace Pantograph

@[export pantograph_version]
-def version := "0.3.1"
+def version := "0.3.0"

 end Pantograph
--- a/README.md
+++ b/README.md
@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"

 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```
--- a/Repl.lean
+++ b/Repl.lean
@ -5,8 +5,6 @@ namespace Pantograph.Repl

 open Lean

-set_option trace.Pantograph.Frontend.MetaTranslate true
-
 structure Context where
  coreContext : Core.Context

@ -63,10 +61,6 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
    catch ex =>
      let desc ← ex.toMessageData.toString
      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
-    finally
-      for {msg, ..} in (← getTraceState).traces do
-        IO.eprintln (← msg.format.toIO)
-      resetTraceState
  if let .some token := cancelTk? then
    runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
  let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
@ -155,7 +149,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.Fro
        .some $ step.newConstants.toArray.map λ name => name.toString
      else
        .none
-    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
        pure (.none, .none, .none)
      else do
        let ({ state, srcBoundaries }, goals) ← liftMetaM do
@ -325,10 +319,12 @@ def execute (command: Protocol.Command): MainM Json := do
        pure $ .error error
    match nextGoalState? with
    | .error error => Protocol.throw error
-    | .ok (.success nextGoalState messages) => do
+    | .ok (.success nextGoalState) => do
      let nextGoalState ← match state.options.automaticMode, args.conv? with
        | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+            Protocol.throw $ errorIO "Resuming known goals"
+          pure result
        | true, .some true => pure nextGoalState
        | true, .some false => do
          let .some (_, _, dormantGoals) := goalState.convMVar? |
@ -338,21 +334,17 @@ def execute (command: Protocol.Command): MainM Json := do
          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 }
+      return { parseError? := .some message }
    | .ok (.invalidAction message) =>
      Protocol.throw $ errorI "invalid" message
    | .ok (.failure messages) =>
-      return { messages? := .some messages }
+      return { tacticErrors? := .some messages }
  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
    let state ← getMainState
    let .some target := state.goalStates[args.target]? |
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -71,7 +71,7 @@ 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 TacticResult.toString : TacticResult → String
-  | .success state _messages => s!".success ({state.goals.length} goals)"
+  | .success state => s!".success ({state.goals.length} goals)"
  | .failure messages =>
    let messages := "\n".intercalate messages.toList
    s!".failure {messages}"
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -84,17 +84,12 @@ def test_tactic : Test :=
    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
-     ({
-       root? := .some { pp? := "fun x => ?m.11"},
-       parent? := .some { pp? := .some "fun x => ?m.11" },
-     }: Protocol.GoalPrintResult),
+     ({ 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),
    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
-     ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
-      Protocol.GoalTacticResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
-     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
+     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+      Protocol.GoalTacticResult)
  ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
  simp
@ -307,34 +302,6 @@ def test_import_open : Test :=
     ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
  ]

-/-- Ensure there cannot be circular references -/
-def test_frontend_process_circular : Test :=
-  let withSorry := "theorem mystery : 1 + 2 = 2 + 3 := sorry"
-  [
-    let goal1: Protocol.Goal := {
-      name := "_uniq.2",
-      target := { pp? := .some "1 + 2 = 2 + 3" },
-      vars := #[],
-    }
-    step "frontend.process"
-      ({
-        file? := .some withSorry,
-        sorrys := true,
-      }: Protocol.FrontendProcess)
-     ({
-       units := [{
-         boundary := (0, withSorry.utf8ByteSize),
-         goalStateId? := .some 0,
-         goals? := .some #[goal1],
-         goalSrcBoundaries? := .some #[(35, 40)],
-         messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
-       }],
-     }: Protocol.FrontendProcessResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic)
-     ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] }
-     : Protocol.GoalTacticResult),
-  ]
-
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
  -- Setup the environment for execution
  let coreContext ← createCoreContext #[]
@ -355,7 +322,6 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
    ("frontend.process invocation", test_frontend_process),
    ("frontend.process sorry", test_frontend_process_sorry),
    ("frontend.process import", test_import_open),
-    ("frontend.process circular", test_frontend_process_circular),
  ]
  tests.map (fun (name, test) => (name, runTest env test))

--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -55,7 +55,6 @@ def main (args: List String) := do
    ("Serial", Serial.suite env_default),
    ("Tactic/Assign", Tactic.Assign.suite env_default),
    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
-    ("Tactic/Special", Tactic.Special.suite env_default),
  ]
  let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
  LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -79,20 +79,20 @@ def test_m_couple: TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
  -- Set m to 3
  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  checkTrue "(1b root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
  let state1b ← match state2.continue state1 with
    | .error msg => do
      addTest $ assertUnreachable $ msg
@ -100,7 +100,7 @@ def test_m_couple: TestM Unit := do
    | .ok state => pure state
  addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ 3", .some "3 ≤ 5"])
-  checkTrue "(2 root)" $ ¬ state1b.isSolved
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

 def test_m_couple_simp: TestM Unit := do
  let state? ← startProof "(2: Nat) ≤ 5"
@ -111,7 +111,7 @@ def test_m_couple_simp: TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -122,11 +122,11 @@ def test_m_couple_simp: TestM Unit := do
    #[#["_uniq.38"], #["_uniq.38"], #[]])

  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  checkTrue "(1b root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
  let state1b ← match state2.continue state1 with
    | .error msg => do
      addTest $ assertUnreachable $ msg
@ -134,9 +134,9 @@ def test_m_couple_simp: TestM Unit := do
    | .ok state => pure state
  addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ 2", .some "2 ≤ 5"])
-  checkTrue "(2 root)" $ ¬ state1b.isSolved
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
  let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -146,7 +146,7 @@ def test_m_couple_simp: TestM Unit := do
      return ()
    | .ok state => pure state
  let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -173,7 +173,7 @@ def test_proposition_generation: TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -184,27 +184,27 @@ def test_proposition_generation: TestM Unit := do
      ])
  if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
    addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone

  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "?m.30 x"])
-  checkTrue "(2 root)" $ ¬ state2.isSolved
+  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone

  let assign := "Eq.refl x"
  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[])

-  checkTrue "(3 root)" state3.isSolved
+  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
  return ()

 def test_partial_continuation: TestM Unit := do
@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])

  let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -238,23 +238,23 @@ def test_partial_continuation: TestM Unit := do
      addTest $ assertUnreachable $ msg
      return ()
    | .ok state => pure state
-  addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue)" ((← 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
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Roundtrip
  --let coupled_goals := coupled_goals.map (λ g =>
  --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (·.name.toString)
-  let coupled_goals := coupled_goals.map ({ name := ·.toName })
+  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
+  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
  let state1b ← match state2.resume (goals := coupled_goals) with
    | .error msg => do
      addTest $ assertUnreachable $ msg
      return ()
    | .ok state => pure state
-  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue)" ((← 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
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Continuation should fail if the state does not exist:
  match state0.resume coupled_goals with
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -89,7 +89,7 @@ def test_identity: TestM Unit := do

  let tactic := "intro p h"
  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -116,7 +116,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn 0 "intro n m" with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -130,7 +130,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
    addTest $ assertUnreachable $ other.toString

  let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -148,14 +148,14 @@ def test_delta_variable: TestM Unit := do
      return ()

  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .success state _ => pure state
+    | .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
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -187,27 +187,27 @@ def test_arith: TestM Unit := do

  let tactic := "intros"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check tactic (state1.goals.length = 1)
-  checkTrue "(1 root)" state1.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
  let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
-  checkTrue "(2 root)" state2.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
  let tactic := "assumption"
  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.test tactic state3.goals.isEmpty
-  checkTrue "(3 root)" $ ¬ state3.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
  return ()

 -- Two ways to write the same theorem
@ -237,7 +237,7 @@ def test_or_comm: TestM Unit := do

  let tactic := "intro p q h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -257,15 +257,15 @@ def test_or_comm: TestM Unit := do
        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
      ]
    }])
-  checkTrue "(1 parent)" state1.parentExpr?.isSome
-  checkTrue "(1 root)" $ ¬ state1.isSolved
+  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
+  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone

  let state1parent ← state1.withParentContext do
    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
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -276,8 +276,8 @@ 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.parentExpr?.isSome
-  checkTrue "(2 root)" $ ¬ state2.isSolved
+  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone

  let state2parent ← state2.withParentContext do
    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
@ -291,7 +291,7 @@ def test_or_comm: TestM Unit := do
    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")

  let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -301,27 +301,27 @@ def test_or_comm: TestM Unit := do
  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)
  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
-  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
  let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
  let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
-  checkTrue "(4_2 root)" $ ¬ state4_2.isSolved
+  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
  -- Ensure the proof can continue from `state4_2`.
  let state2b ← match state4_2.continue state2 with
    | .error msg => do
@ -330,18 +330,18 @@ def test_or_comm: TestM Unit := do
    | .ok state => pure state
  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
  let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  checkTrue "(4_1 root)" $ ¬ state4_1.rootExpr?.get!.hasExprMVar
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome

  return ()
  where
@ -375,7 +375,7 @@ def test_conv: TestM Unit := do

  let tactic := "intro a b c1 c2 h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -383,7 +383,7 @@ def test_conv: TestM Unit := do
    #[interiorGoal [] "a + b + c1 = b + a + c2"])

  let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -392,7 +392,7 @@ def test_conv: TestM Unit := do

  let convTactic := "rhs"
  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -401,7 +401,7 @@ def test_conv: TestM Unit := do

  let convTactic := "lhs"
  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -410,7 +410,7 @@ def test_conv: TestM Unit := do

  let convTactic := "congr"
  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -422,7 +422,7 @@ def test_conv: TestM Unit := do

  let convTactic := "rw [Nat.add_comm]"
  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -431,7 +431,7 @@ def test_conv: TestM Unit := do

  let convTactic := "rfl"
  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -446,7 +446,7 @@ def test_conv: TestM Unit := do

  let convTactic := "rfl"
  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -454,14 +454,14 @@ def test_conv: TestM Unit := do
    #[])

  let state1_1 ← match ← state6.convExit with
-    | .success state _ => pure state
+    | .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
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -488,7 +488,7 @@ def test_calc: TestM Unit := do
      return ()
  let tactic := "intro a b c d h1 h2"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -496,7 +496,7 @@ def test_calc: TestM Unit := do
    #[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
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -510,7 +510,7 @@ def test_calc: TestM Unit := do

  let tactic := "apply h1"
  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -521,7 +521,7 @@ def test_calc: TestM Unit := do
      return ()
  let pred := "_ = c + d"
  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -532,7 +532,7 @@ def test_calc: TestM Unit := do
  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
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -553,7 +553,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do

  let tactic := "intro p"
  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -572,7 +572,7 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do

  let tactic := "intro p q r h"
  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -604,7 +604,7 @@ def test_deconstruct : TestM Unit := do

  let tactic := "intro p q ⟨hp, hq⟩"
  let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      fail other.toString
      return ()
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -1,3 +1,2 @@
 import Test.Tactic.Assign
 import Test.Tactic.Prograde
-import Test.Tactic.Special
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@ -56,7 +56,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
  let state0 ← GoalState.create rootExpr
  let tactic := "intro p q h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -65,7 +65,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do

  let expr := "Or.inl (Or.inl h)"
  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -75,7 +75,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
  let evalBind := "y"
  let evalExpr := "Or.inl h"
  let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -95,7 +95,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do

  let expr := "Or.inl y"
  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
 def test_define_root_expr : TestT Elab.TermElabM Unit := do
  --let rootExpr ← parseSentence "Nat"
  --let state0 ← GoalState.create rootExpr
-  --let .success state1 _ ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
  --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
  --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
  let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
  let state0 ← GoalState.create rootExpr
  let tactic := "intro p x"
-  let .success state1 _ ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
  let binderName := `binder
  let value := "x.fst"
  let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
  let tacticM := Tactic.evalDefine binderName expr
-  let .success state2 _ ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
  let tactic := s!"apply {binderName}"
-  let .success state3 _ ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
  let tactic := s!"exact 5"
-  let .success state4 _ ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
  let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
  addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")

@ -140,7 +140,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
  let state0 ← GoalState.create rootExpr
  let tactic := "intro p q h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -149,7 +149,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do

  let expr := "Or.inl (Or.inl h)"
  let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -159,7 +159,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
  let haveBind := "y"
  let haveType := "p ∨ q"
  let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -171,7 +171,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do

  let expr := "Or.inl h"
  let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -185,7 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
      return ()
  let expr := "Or.inl y"
  let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -200,7 +200,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
  let state0 ← GoalState.create rootExpr
  let tactic := "intro a p h"
  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -216,7 +216,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
    | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
    | false => state1.tryAssign (state1.get! 0) (expr := expr)
  let state2 ← match result2 with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -241,7 +241,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do

  let tactic := "exact 1"
  let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
@ -274,7 +274,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do

  let tactic := "exact Or.inl (Or.inl h)"
  let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
+    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
--- a/Test/Tactic/Special.lean
+++ b/Test/Tactic/Special.lean
@ -1,23 +0,0 @@
-import LSpec
-import Lean
-import Test.Common
-
-open Lean
-open Pantograph
-
-namespace Pantograph.Test.Tactic.Special
-
-def test_exact_q : TestT Elab.TermElabM Unit := do
-  let rootExpr ← parseSentence "1 + 2 = 2 + 3"
-  let state0 ← GoalState.create rootExpr
-  let tactic := "exact?"
-  let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic)
-  let .failure messages := state1? | fail "Must fail"
-  checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."]
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("exact?", test_exact_q),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Special
--- a/doc/rationale.md
+++ b/doc/rationale.md
@ -47,16 +47,11 @@ include:

 - If a tactic loses track of metavariables, it will not be caught until the end
  of the proof search. This is a bug in the tactic itself.
- Although a timeout feature exists in Pantograph, it relies on the coöperative
-  multitasking from the tactic implementation. There is nothing preventing a
-  buggy tactic from stalling Lean if it does not check for cancellation often.
- For the same reason as above, there is no graceful way to stop a tactic which
-  leaks infinite memory. Users who wish to have this behaviour should run
-  Pantograph in a controlled environment with limited allocations. e.g.
-  Linux control groups.
+- Timeouts for executing tactics is not available. Maybe this will change in the
+  future.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system. This question is also
-  not well-defined.
+  `def mystery : Nat := :=`) due to Lean's parsing system.
+

 ## References

--- a/doc/repl.md
+++ b/doc/repl.md
@ -39,8 +39,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  - `{ "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>]}`:
  Execute continuation/resumption
  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.