Merge pull request 'Enable handling of m-Coupled goals' (#20) from goal/dependency into dev

Reviewed-on: #20
2023-10-27 19:30:20 -07:00 · 2023-10-27 19:30:20 -07:00 · c19fd1bcfb
parent 7dc6e4e549 427d819349
commit c19fd1bcfb
16 changed files with 950 additions and 457 deletions
--- a/Main.lean
+++ b/Main.lean
@ -8,7 +8,7 @@ import Pantograph
 open Pantograph

 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parse_command (s: String): Except String Commands.Command := do
+def parseCommand (s: String): Except String Protocol.Command := do
  let s := s.trim
  match s.get? 0 with
  | .some '{' => -- Parse in Json mode
@ -26,9 +26,9 @@ unsafe def loop : MainM Unit := do
  let state ← get
  let command ← (← IO.getStdin).getLine
  if command.trim.length = 0 then return ()
-  match parse_command command with
+  match parseCommand command with
  | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
    -- Using `Lean.Json.compress` here to prevent newline
    IO.println error.compress
  | .ok command =>
--- a/7
+++ b/7
@ -6,7 +6,7 @@ TEST_EXE := build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)

 $(LIB) $(EXE): $(SOURCE)
-	lake build
+	lake build pantograph

 $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 test: $(TEST_EXE)
 	lake env $(TEST_EXE)

-.PHONY: test
+clean:
+	lake clean
+
+.PHONY: test clean
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -1,8 +1,8 @@
-import Pantograph.Commands
-import Pantograph.Serial
-import Pantograph.Symbols
-import Pantograph.Tactic
+import Pantograph.Goal
+import Pantograph.Protocol
 import Pantograph.SemihashMap
+import Pantograph.Serial
+import Pantograph.Symbol

 namespace Pantograph

@ -11,16 +11,16 @@ structure Context where

 /-- Stores state of the REPL -/
 structure State where
-  options: Commands.Options := {}
+  options: Protocol.Options := {}
  goalStates: SemihashMap GoalState := SemihashMap.empty

-- State monad
+/-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
-- monadic features in `MainM`
-abbrev CR α := Except Commands.InteractionError α
+-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
+-- certain monadic features in `MainM`
+abbrev CR α := Except Protocol.InteractionError α

-def execute (command: Commands.Command): MainM Lean.Json := do
+def execute (command: Protocol.Command): MainM Lean.Json := do
  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
    match Lean.fromJson? command.payload with
    | .ok args => do
@ -39,32 +39,33 @@ def execute (command: Commands.Command): MainM Lean.Json := do
  | "goal.start"     => run goal_start
  | "goal.tactic"    => run goal_tactic
  | "goal.delete"    => run goal_delete
+  | "goal.print"    => run goal_print
  | cmd =>
-    let error: Commands.InteractionError :=
+    let error: Protocol.InteractionError :=
      errorCommand s!"Unknown command {cmd}"
    return Lean.toJson error
  where
-  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
+  errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
  errorCommand := errorI "command"
  errorIndex := errorI "index"
  -- Command Functions
-  reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
+  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
    let state ← get
    let nGoals := state.goalStates.size
    set { state with goalStates := SemihashMap.empty }
    return .ok { nGoals }
-  stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
+  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
    let state ← get
    let nGoals := state.goalStates.size
    return .ok { nGoals }
-  lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
+  lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
    let env ← Lean.MonadEnv.getEnv
    let names := env.constants.fold (init := #[]) (λ acc name info =>
      match to_filtered_symbol name info with
      | .some x => acc.push x
      | .none => acc)
    return .ok { symbols := names }
-  lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
+  lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
    let name := str_to_name args.name
@ -84,7 +85,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
        value? := ← value?.mapM (λ v => serialize_expression state.options v),
        module? := module?
      }
-  expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
+  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
    match syntax_from_str env args.expr with
@ -101,7 +102,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
          }
        catch exception =>
          return .error $ errorI "typing" (← exception.toMessageData.toString)
-  options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
+  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
    let state ← get
    let options := state.options
    set { state with
@ -110,15 +111,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
        printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
        printExprPretty := args.printExprPretty?.getD options.printExprPretty,
        printExprAST := args.printExprAST?.getD options.printExprAST,
-        proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
+        noRepeat := args.noRepeat?.getD options.noRepeat,
        printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
        printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
      }
    }
    return .ok {  }
-  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
+  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
    return .ok (← get).options
-  goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
+  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
    let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@ -133,42 +134,55 @@ def execute (command: Commands.Command): MainM Lean.Json := do
        (match env.find? <| str_to_name copyFrom with
        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
        | .some cInfo => return .ok cInfo.type)
-      | .none, .none =>
-        return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
-      | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
+      | _, _ =>
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
    match expr? with
    | .error error => return .error error
    | .ok expr =>
      let goalState ← GoalState.create expr
-      let (goalStates, goalId) := state.goalStates.insert goalState
+      let (goalStates, stateId) := state.goalStates.insert goalState
      set { state with goalStates }
-      return .ok { goalId }
-  goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
+      return .ok { stateId }
+  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
    let state ← get
-    match state.goalStates.get? args.goalId with
-    | .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    | .some goalState =>
-      let result ← GoalState.execute goalState args.tactic |>.run state.options
-      match result with
-      | .success goals =>
-        if goals.isEmpty then
-          return .ok {}
-        else
-          -- Append all goals
-          let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr =>
-            let (map, indices, serializedGoals) := acc
-            let (goalState, sGoal) := itr
-            let (map, index) := map.insert goalState
-            (map, index :: indices, sGoal :: serializedGoals)
-            ) (state.goalStates, [], []) goals
-          set { state with goalStates }
-          return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
-      | .failure messages =>
+    match state.goalStates.get? args.stateId with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    | .some goalState => do
+      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
+        | .some tactic, .none => do
+          pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
+        | .none, .some expr => do
+          pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
+        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
+      match nextGoalState? with
+      | .error error => return .error error
+      | .ok (.success nextGoalState) =>
+        let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
+        set { state with goalStates }
+        let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
+        return .ok {
+          nextStateId? := .some nextStateId,
+          goals? := .some goals,
+        }
+      | .ok (.parseError message) =>
+        return .ok { parseError? := .some message }
+      | .ok (.indexError goalId) =>
+        return .error $ errorIndex s!"Invalid goal id index {goalId}"
+      | .ok (.failure messages) =>
        return .ok { tacticErrors? := .some messages }
-  goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
+  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
    let state ← get
-    let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
+    let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
    set { state with goalStates }
    return .ok {}
+  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
+    let state ← get
+    match state.goalStates.get? args.stateId with
+    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    | .some goalState => do
+      let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
+      return .ok {
+        root?,
+      }

 end Pantograph
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -0,0 +1,204 @@
+import Lean
+
+import Pantograph.Symbol
+
+def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
+  {
+    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
+  }
+
+
+namespace Pantograph
+open Lean
+
+structure GoalState where
+  savedState : Elab.Tactic.SavedState
+
+  -- The root hole which is the search target
+  root: MVarId
+  -- New metavariables acquired in this state
+  newMVars: SSet MVarId
+
+  -- The id of the goal in the parent
+  parentGoalId: Nat := 0
+
+abbrev M := Elab.TermElabM
+
+protected def GoalState.create (expr: Expr): M GoalState := do
+  -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
+  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+
+  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+  --let expr ← instantiateMVars expr
+  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let root := goal.mvarId!
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
+  return {
+    savedState,
+    root,
+    newMVars := SSet.insert .empty root,
+  }
+protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
+
+protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
+  state.savedState.term.restore
+  m
+
+protected def GoalState.mctx (state: GoalState): MetavarContext :=
+  state.savedState.term.meta.meta.mctx
+protected def GoalState.env (state: GoalState): Environment :=
+  state.savedState.term.meta.core.env
+private def GoalState.mvars (state: GoalState): SSet MVarId :=
+  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+
+/-- Inner function for executing tactic on goal state -/
+def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
+    M (Except (Array String) Elab.Tactic.SavedState):= do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
+    state.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      Elab.Tactic.evalTactic stx
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .error errors
+      else
+        return .ok (← MonadBacktrack.saveState)
+    catch exception =>
+      return .error #[← exception.toMessageData.toString]
+  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
+
+/-- Response for executing a tactic -/
+inductive TacticResult where
+  -- Goes to next state
+  | success (state: GoalState)
+  -- Tactic failed with messages
+  | failure (messages: Array String)
+  -- Could not parse tactic
+  | parseError (message: String)
+  -- The goal index is out of bounds
+  | indexError (goalId: Nat)
+
+/-- Execute tactic on given state -/
+protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
+    M TacticResult := do
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure $ goal
+    | .none => return .indexError goalId
+  let tactic ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `tactic)
+    (input := tactic)
+    (fileName := "<stdin>") with
+    | .ok stx => pure $ stx
+    | .error error => return .parseError error
+  match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
+  | .error errors =>
+    return .failure errors
+  | .ok nextSavedState =>
+    -- Assert that the definition of metavariables are the same
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    let prevMCtx := state.savedState.term.meta.meta.mctx
+    -- Generate a list of mvarIds that exist in the parent state; Also test the
+    -- assertion that the types have not changed on any mvars.
+    let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+        assert! prevMVarDecl.type == mvarDecl.type
+        return acc
+      else
+        return acc.insert mvarId
+      ) SSet.empty
+    return .success {
+      state with
+      savedState := nextSavedState
+      newMVars,
+      parentGoalId := goalId,
+    }
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := "<stdin>") with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let tacticM:  Elab.Tactic.TacticM TacticResult := do
+    state.savedState.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+      -- Attempt to unify the expression
+      let goalType ← goal.getType
+      let exprType ← Meta.inferType expr
+      if !(← Meta.isDefEq goalType exprType) then
+        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
+      goal.checkNotAssigned `GoalState.tryAssign
+      goal.assign expr
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .failure errors
+      else
+        let prevMCtx := state.savedState.term.meta.meta.mctx
+        let nextMCtx ← getMCtx
+        -- Generate a list of mvarIds that exist in the parent state; Also test the
+        -- assertion that the types have not changed on any mvars.
+        let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
+          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
+            assert! prevMVarDecl.type == mvarDecl.type
+            return acc
+          else
+            return mvarId :: acc
+          ) []
+        -- The new goals are the newMVars that lack an assignment
+        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
+        let nextSavedState ← MonadBacktrack.saveState
+        return .success {
+          state with
+          savedState := nextSavedState,
+          newMVars := newMVars.toSSet,
+          parentGoalId := goalId,
+        }
+    catch exception =>
+      return .failure #[← exception.toMessageData.toString]
+  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+
+/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/
+protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState :=
+  if target.root != graftee.root then
+    .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}"
+  -- Ensure goals are not dangling
+  else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then
+    .error s!"Some goals in target are not present in the graftee"
+  else
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+    let unassigned := target.goals.filter (λ goal =>
+      let mctx := graftee.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
+      savedState := {
+        term := graftee.savedState.term,
+        tactic := { goals := unassigned },
+      },
+      root := target.root,
+      newMVars := graftee.newMVars,
+    }
+
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
+  let expr := goalState.mctx.eAssignment.find! goalState.root
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasMVar 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
+    .some expr
+
+end Pantograph
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json

-namespace Pantograph.Commands
+namespace Pantograph.Protocol


 /-- Main Option structure, placed here to avoid name collision -/
@ -18,9 +18,10 @@ structure Options where
  printExprPretty: Bool    := true
  -- When enabled, print the raw AST of expressions
  printExprAST: Bool       := false
-  -- When enabled, the types and values of persistent variables in a proof goal
-  -- are not shown unless they are new to the proof step. Reduces overhead
-  proofVariableDelta: Bool := false
+  -- When enabled, the types and values of persistent variables in a goal
+  -- are not shown unless they are new to the proof step. Reduces overhead.
+  -- NOTE: that this assumes the type and assignment of variables can never change.
+  noRepeat: Bool := false
  -- See `pp.auxDecls`
  printAuxDecls: Bool      := false
  -- See `pp.implementationDetailHyps`
@ -43,7 +44,10 @@ structure Expression where
  deriving Lean.ToJson

 structure Variable where
-  name: String
+  /-- The internal name used in raw expressions -/
+  name: String := ""
+  /-- The name displayed to the user -/
+  userName: String
  /-- Does the name contain a dagger -/
  isInaccessible?: Option Bool := .none
  type?: Option Expression  := .none
@ -120,7 +124,7 @@ structure OptionsSet where
  printJsonPretty?: Option Bool
  printExprPretty?: Option Bool
  printExprAST?: Option Bool
-  proofVariableDelta?: Option Bool
+  noRepeat?: Option Bool
  printAuxDecls?: Option Bool
  printImplementationDetailHyps?: Option Bool
  deriving Lean.FromJson
@ -132,32 +136,55 @@ abbrev OptionsPrintResult := Options

 structure GoalStart where
  -- Only one of the fields below may be populated.
-  expr: Option String     -- Proof expression
-  copyFrom: Option String -- Theorem name
+  expr: Option String     -- Directly parse in an expression
+  copyFrom: Option String -- Copy the type from a theorem in the environment
  deriving Lean.FromJson
 structure GoalStartResult where
-  goalId: Nat := 0 -- Proof tree id
+  stateId: Nat := 0
  deriving Lean.ToJson
 structure GoalTactic where
  -- Identifiers for tree, state, and goal
-  goalId: Nat
-  tactic: String
+  stateId: Nat
+  goalId: Nat := 0
+  -- One of the fields here must be filled
+  tactic?: Option String := .none
+  expr?: Option String := .none
  deriving Lean.FromJson
 structure GoalTacticResult where
-  -- Existence of this field shows success
+  -- 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.
  goals?: Option (Array Goal)          := .none
-  -- Next proof state id, if successful
-  goalIds?: Option (Array Nat)          := .none
-  -- Existence of this field shows failure
+
+  -- 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
  deriving Lean.ToJson

-- Remove a bunch of goals.
+-- Remove goal states
 structure GoalDelete where
-  goalIds: List Nat
+  stateIds: List Nat
  deriving Lean.FromJson
 structure GoalDeleteResult where
  deriving Lean.ToJson

+structure GoalPrint where
+  stateId: Nat
+  deriving Lean.FromJson
+structure GoalPrintResult where
+  -- The root expression
+  root?: Option Expression
+  deriving Lean.ToJson

-end Pantograph.Commands
+-- Diagnostic Options, not available in REPL
+structure GoalDiag where
+  printContext: Bool := true
+  printValue: Bool := true
+  printNewMVars: Bool := false
+  -- Print all mvars
+  printAll: Bool := false
+
+
+end Pantograph.Protocol
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -3,7 +3,8 @@ All serialisation functions
 -/
 import Lean

-import Pantograph.Commands
+import Pantograph.Protocol
+import Pantograph.Goal

 namespace Pantograph
 open Lean
@ -28,34 +29,28 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
 def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabType syn
-    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
-    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
-    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
-    let expr ← instantiateMVars expr
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)
 def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
-    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
-    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
-    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
-    let expr ← instantiateMVars expr
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)


 --- Output Functions ---

-def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
+def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
  Meta.forallTelescope expr fun arr body => do
    let binders ← arr.mapM fun fvar => do
      return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
    return { binders, target := toString (← Meta.ppExpr body) }

-private def name_to_ast: Lean.Name → String
-  | .anonymous
-  | .num _ _ => ":anon"
+private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with
+  | .anonymous => ":anon"
+  | .num n i => match sanitize with
+    | false => s!"{toString n} {i}"
+    | true => ":anon"
  | n@(.str _ _) => toString n

 private def level_depth: Level → Nat
@ -108,89 +103,91 @@ def serialize_sort_level_ast (level: Level): String :=
 /--
 Completely serializes an expression tree. Json not used due to compactness
 -/
-def serialize_expression_ast (expr: Expr): MetaM String := do
-  match expr with
-  | .bvar deBruijnIndex =>
-    -- This is very common so the index alone is shown. Literals are handled below.
-    -- The raw de Bruijn index should never appear in an unbound setting. In
-    -- Lean these are handled using a `#` prefix.
-    return s!"{deBruijnIndex}"
-  | .fvar fvarId =>
-    let name := (← fvarId.getDecl).userName
-    return s!"(:fv {name})"
-  | .mvar mvarId =>
-    let name := name_to_ast mvarId.name
-    return s!"(:mv {name})"
-  | .sort level =>
-    let level := serialize_sort_level_ast level
-    return s!"(:sort {level})"
-  | .const declName _ =>
-    -- The universe level of the const expression is elided since it should be
-    -- inferrable from surrounding expression
-    return s!"(:c {declName})"
-  | .app fn arg =>
-    let fn' ← serialize_expression_ast fn
-    let arg' ← serialize_expression_ast arg
-    return s!"({fn'} {arg'})"
-  | .lam binderName binderType body binderInfo =>
-    let binderName' := name_to_ast binderName
-    let binderType' ← serialize_expression_ast binderType
-    let body' ← serialize_expression_ast body
-    let binderInfo' := binder_info_to_ast binderInfo
-    return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
-  | .forallE binderName binderType body binderInfo =>
-    let binderName' := name_to_ast binderName
-    let binderType' ← serialize_expression_ast binderType
-    let body' ← serialize_expression_ast body
-    let binderInfo' := binder_info_to_ast binderInfo
-    return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
-  | .letE name type value body _ =>
-    -- Dependent boolean flag diacarded
-    let name' := name_to_ast name
-    let type' ← serialize_expression_ast type
-    let value' ← serialize_expression_ast value
-    let body' ← serialize_expression_ast body
-    return s!"(:let {name'} {type'} {value'} {body'})"
-  | .lit v =>
-    -- To not burden the downstream parser who needs to handle this, the literal
-    -- is wrapped in a :lit sexp.
-    let v' := match v with
-      | .natVal val => toString val
-      | .strVal val => s!"\"{val}\""
-    return s!"(:lit {v'})"
-  | .mdata _ expr =>
-    -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-    -- It may become necessary to incorporate the metadata.
-    return (← serialize_expression_ast expr)
-  | .proj typeName idx struct =>
-    let struct' ← serialize_expression_ast struct
-    return s!"(:proj {typeName} {idx} {struct'})"
-
+def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
+  self expr
  where
+  self (e: Expr): String :=
+    match e with
+    | .bvar deBruijnIndex =>
+      -- This is very common so the index alone is shown. Literals are handled below.
+      -- The raw de Bruijn index should never appear in an unbound setting. In
+      -- Lean these are handled using a `#` prefix.
+      s!"{deBruijnIndex}"
+    | .fvar fvarId =>
+      let name := of_name fvarId.name
+      s!"(:fv {name})"
+    | .mvar mvarId =>
+      let name := of_name mvarId.name
+      s!"(:mv {name})"
+    | .sort level =>
+      let level := serialize_sort_level_ast level
+      s!"(:sort {level})"
+    | .const declName _ =>
+      -- The universe level of the const expression is elided since it should be
+      -- inferrable from surrounding expression
+      s!"(:c {declName})"
+    | .app fn arg =>
+      let fn' := self fn
+      let arg' := self arg
+      s!"({fn'} {arg'})"
+    | .lam binderName binderType body binderInfo =>
+      let binderName' := of_name binderName
+      let binderType' := self binderType
+      let body' := self body
+      let binderInfo' := binder_info_to_ast binderInfo
+      s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .forallE binderName binderType body binderInfo =>
+      let binderName' := of_name binderName
+      let binderType' := self binderType
+      let body' := self body
+      let binderInfo' := binder_info_to_ast binderInfo
+      s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+    | .letE name type value body _ =>
+      -- Dependent boolean flag diacarded
+      let name' := name_to_ast name
+      let type' := self type
+      let value' := self value
+      let body' := self body
+      s!"(:let {name'} {type'} {value'} {body'})"
+    | .lit v =>
+      -- To not burden the downstream parser who needs to handle this, the literal
+      -- is wrapped in a :lit sexp.
+      let v' := match v with
+        | .natVal val => toString val
+        | .strVal val => s!"\"{val}\""
+      s!"(:lit {v'})"
+    | .mdata _ inner =>
+      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
+      -- It may become necessary to incorporate the metadata.
+      self inner
+    | .proj typeName idx struct =>
+      let struct' := self struct
+      s!"(:proj {typeName} {idx} {struct'})"
  -- Elides all unhygenic names
  binder_info_to_ast : Lean.BinderInfo → String
    | .default => ""
    | .implicit => " :implicit"
    | .strictImplicit => " :strictImplicit"
    | .instImplicit => " :instImplicit"
+  of_name (name: Name) := name_to_ast name sanitize

-def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do
+def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
  let pp := toString (← Meta.ppExpr e)
  let pp?: Option String := match options.printExprPretty with
-      | true => .some pp
-      | false => .none
-  let sexp: String := (← serialize_expression_ast e)
+    | true => .some pp
+    | false => .none
+  let sexp: String := serialize_expression_ast e
  let sexp?: Option String := match options.printExprAST with
-      | true => .some sexp
-      | false => .none
+    | true => .some sexp
+    | false => .none
  return {
    pp?,
    sexp?
  }

 /-- Adapted from ppGoal -/
-def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
-      : MetaM Commands.Goal := do
+def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+      : MetaM Protocol.Goal := do
  -- Options for printing; See Meta.ppGoal for details
  let showLetValues  := true
  let ppAuxDecls     := options.printAuxDecls
@ -198,29 +195,32 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
  let lctx           := mvarDecl.lctx
  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
  Meta.withLCtx lctx mvarDecl.localInstances do
-    let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
      match localDecl with
-      | .cdecl _ _ varName _ _ _ =>
-        let varName := varName.simpMacroScopes
+      | .cdecl _ fvarId userName _ _ _ =>
+        let userName := userName.simpMacroScopes
        return {
-          name := toString varName,
+          name := of_name fvarId.name,
+          userName:= of_name userName.simpMacroScopes,
        }
-      | .ldecl _ _ varName _ _ _ _ => do
+      | .ldecl _ fvarId userName _ _ _ _ => do
        return {
-          name := toString varName,
+          name := of_name fvarId.name,
+          userName := toString userName.simpMacroScopes,
        }
-    let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
+    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
      match localDecl with
-      | .cdecl _ _ varName type _ _ =>
-        let varName := varName.simpMacroScopes
+      | .cdecl _ fvarId userName type _ _ =>
+        let userName := userName.simpMacroScopes
        let type ← instantiateMVars type
        return {
-          name := toString varName,
-          isInaccessible? := .some varName.isInaccessibleUserName
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
          type? := .some (← serialize_expression options type)
        }
-      | .ldecl _ _ varName type val _ _ => do
-        let varName := varName.simpMacroScopes
+      | .ldecl _ fvarId userName type val _ _ => do
+        let userName := userName.simpMacroScopes
        let type ← instantiateMVars type
        let value? ← if showLetValues then
          let val ← instantiateMVars val
@ -228,8 +228,9 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
        else
          pure $ .none
        return {
-          name := toString varName,
-          isInaccessible? := .some varName.isInaccessibleUserName
+          name := of_name fvarId.name,
+          userName:= of_name userName,
+          isInaccessible? := .some userName.isInaccessibleUserName
          type? := .some (← serialize_expression options type)
          value? := value?
        }
@ -239,21 +240,79 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
      if skip then
        return acc
      else
-        let nameOnly := options.proofVariableDelta && (parentDecl?.map
+        let nameOnly := options.noRepeat && (parentDecl?.map
          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
        let var ← match nameOnly with
          | true => ppVarNameOnly localDecl
          | false => ppVar localDecl
        return var::acc
    return {
-      caseName? := match mvarDecl.userName with
-        | Name.anonymous => .none
-        | name => .some <| toString name,
-      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
+      caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
+      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
      vars := vars.reverse.toArray
    }
+  where
+  of_name (n: Name) := name_to_ast n (sanitize := false)

+protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
+  let goals := state.goals.toArray
+  state.savedState.term.meta.restore
+  let parentDecl? := parent.bind (λ parentState =>
+    let parentGoal := parentState.goals.get! state.parentGoalId
+    parentState.mctx.findDecl? parentGoal)
+  goals.mapM fun goal => do
+    match state.mctx.findDecl? goal with
+    | .some mvarDecl =>
+      let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
+      pure serializedGoal
+    | .none => throwError s!"Metavariable does not exist in context {goal.name}"

+/-- Print the metavariables in a readable format -/
+protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
+  let savedState := goalState.savedState
+  savedState.term.meta.restore
+  let goals := savedState.tactic.goals
+  let mctx ← getMCtx
+  let root := goalState.root
+  -- Print the root
+  match mctx.decls.find? root with
+  | .some decl => printMVar ">" root decl
+  | .none => IO.println s!">{root.name}: ??"
+  goals.forM (fun mvarId => do
+    if mvarId != root then
+      match mctx.decls.find? mvarId with
+      | .some decl => printMVar "⊢" mvarId decl
+      | .none => IO.println s!"⊢{mvarId.name}: ??"
+  )
+  let goals := goals.toSSet
+  mctx.decls.forM (fun mvarId decl => do
+    if goals.contains mvarId || mvarId == root then
+      pure ()
+    -- Always print the root goal
+    else if mvarId == goalState.root then
+      printMVar (pref := ">") mvarId decl
+    -- Print the remainig ones that users don't see in Lean
+    else if options.printAll then
+      let pref := if goalState.newMVars.contains mvarId then "~" else " "
+      printMVar pref mvarId decl
+    else
+      pure ()
+      --IO.println s!" {mvarId.name}{userNameToString decl.userName}"
+  )
+  where
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
+      if options.printContext then
+        decl.lctx.fvarIdToDecl.forM printFVar
+      let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
+      IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
+      if options.printValue then
+        if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
+          IO.println s!"  = {← Meta.ppExpr value}"
+    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
+      IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
+    userNameToString : Name → String
+      | .anonymous => ""
+      | other => s!"[{other}]"

 end Pantograph
--- a/Pantograph/Symbols.lean
+++ b/Pantograph/Symbols.lean
@ -1,10 +1,8 @@
-/-
- - Manages the visibility status of symbols
- -/
 import Lean.Declaration

 namespace Pantograph

+/-- Converts a symbol of the form `aa.bb.cc` to a name -/
 def str_to_name (s: String): Lean.Name :=
  (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous

--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@ -1,102 +0,0 @@
-import Lean
-
-import Pantograph.Symbols
-import Pantograph.Serial
-
-/-
-The proof state manipulation system
-
-A proof state is launched by providing
-1. Environment: `Environment`
-2. Expression: `Expr`
-The expression becomes the first meta variable in the saved tactic state
-`Elab.Tactic.SavedState`.
-From this point on, any proof which extends
-`Elab.Term.Context` and
-/
-
-def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
-  {
-    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
-  }
-
-
-namespace Pantograph
-open Lean
-
-structure GoalState where
-  mvarId: MVarId
-  savedState : Elab.Tactic.SavedState
-
-abbrev M := Elab.TermElabM
-
-def GoalState.create (expr: Expr): M GoalState := do
-  let expr ← instantiateMVars expr
-  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
-  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
-  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
-  return {
-    savedState := savedState,
-    mvarId := goal.mvarId!
-  }
-
-def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
-    M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
-  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
-    state.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      Elab.Tactic.evalTactic stx
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
-        return .error errors
-      else
-        return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
-    catch exception =>
-      return .error #[← exception.toMessageData.toString]
-  match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
-    (input := tactic)
-    (fileName := "<stdin>") with
-  | Except.error err => return .error #[err]
-  | Except.ok stx    => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
-
-/-- Response for executing a tactic -/
-inductive TacticResult where
-  -- Goes to next state
-  | success (goals: Array (GoalState × Commands.Goal))
-  -- Fails with messages
-  | failure (messages: Array String)
-
-namespace TacticResult
-
-def is_success: TacticResult → Bool
-  | .success _ => true
-  | .failure _ => false
-
-end TacticResult
-
-/-- Execute tactic on given state -/
-def GoalState.execute (goal: GoalState) (tactic: String):
-    Commands.OptionsT M TacticResult := do
-  let options ← read
-  match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with
-  | .error errors =>
-    return .failure errors
-  | .ok (nextState, nextGoals) =>
-    if nextGoals.isEmpty then
-      return .success #[]
-    else
-      let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState }
-      let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId
-      let goals ← nextGoals.mapM fun nextGoal => do
-        match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with
-        | .some mvarDecl =>
-          let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
-          return (nextGoal, serializedGoal)
-        | .none => throwError nextGoal.mvarId
-      return .success goals.toArray
-
-end Pantograph
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,5 +1,5 @@
 namespace Pantograph

-def version := "0.2.5"
+def version := "0.2.6"

 end Pantograph
--- a/README.md
+++ b/README.md
@ -76,8 +76,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
  have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
 - `options.print`: Display the current set of options
 - `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
+- `goal.print {"stateId": <id>}"`: Print a goal state
 - `stat`: Display resource usage

 ## Errors
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -0,0 +1,19 @@
+import Pantograph.Protocol
+
+namespace Pantograph
+
+namespace Protocol
+/-- Set internal names to "" -/
+def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal with
+    vars := goal.vars.map removeInternalAux,
+  }
+  where removeInternalAux (v: Variable): Variable :=
+    {
+      v with
+      name := ""
+    }
+end Protocol
+
+end Pantograph
--- a/Test/Holes.lean
+++ b/Test/Holes.lean
@ -0,0 +1,101 @@
+import LSpec
+import Pantograph.Goal
+import Pantograph.Serial
+
+namespace Pantograph.Test.Holes
+open Pantograph
+open Lean
+
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
+
+deriving instance DecidableEq, Repr for Commands.Expression
+deriving instance DecidableEq, Repr for Commands.Variable
+deriving instance DecidableEq, Repr for Commands.Goal
+
+def add_test (test: LSpec.TestSeq): TestM Unit := do
+  set $ (← get) ++ test
+
+def start_goal (hole: String): TestM (Option GoalState) := do
+  let env ← Lean.MonadEnv.getEnv
+  let syn? := syntax_from_str env hole
+  add_test $ LSpec.check s!"Parsing {hole}" (syn?.isOk)
+  match syn? with
+  | .error error =>
+    IO.println error
+    return Option.none
+  | .ok syn =>
+    let expr? ← syntax_to_expr syn
+    add_test $ LSpec.check s!"Elaborating" expr?.isOk
+    match expr? with
+    | .error error =>
+      IO.println error
+      return Option.none
+    | .ok expr =>
+      let goal ← GoalState.create (expr := expr)
+      return Option.some goal
+
+def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
+
+def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      name := x.fst,
+      type? := .some { pp? := .some x.snd },
+      isInaccessible? := .some false
+    })).toArray
+  }
+-- Like `build_goal` but allow certain variables to be elided.
+def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      name := x.fst,
+      type? := x.snd.map (λ type => { pp? := type }),
+      isInaccessible? := x.snd.map (λ _ => false)
+    })).toArray
+  }
+
+def construct_sigma: TestM Unit := do
+  let goal? ← start_goal "∀ (n m: Nat), n + m = m + n"
+  add_test $ LSpec.check "Start goal" goal?.isSome
+  if let .some goal := goal? then
+    return ()
+
+
+def proof_runner (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 := {
+    currNamespace := str_to_name "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  let coreM := metaM.run'
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok (_, a) =>
+    return a
+
+def suite: IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  let tests := [
+    ("Σ'", construct_sigma)
+  ]
+  let tests ← tests.foldlM (fun acc tests => do
+    let (name, tests) := tests
+    let tests ← proof_runner env tests
+    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
+
+  return LSpec.group "Holes" tests
+
+end Pantograph.Test.Holes
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -2,7 +2,7 @@
 -/
 import LSpec
 import Pantograph
-namespace Pantograph.Test
+namespace Pantograph.Test.Integration
 open Pantograph

 def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
@ -47,26 +47,26 @@ def test_option_modify : IO LSpec.TestSeq :=
  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
  let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"
  let module? := Option.some "Init.Data.Nat.Basic"
-  let options: Commands.Options := {}
+  let options: Protocol.Options := {}
  subroutine_runner [
    subroutine_step "lib.inspect"
      [("name", .str "Nat.add_one")]
     (Lean.toJson ({
       type := { pp? }, module? }:
-      Commands.LibInspectResult)),
+      Protocol.LibInspectResult)),
    subroutine_step "options.set"
      [("printExprAST", .bool true)]
     (Lean.toJson ({ }:
-      Commands.OptionsSetResult)),
+      Protocol.OptionsSetResult)),
    subroutine_step "lib.inspect"
      [("name", .str "Nat.add_one")]
     (Lean.toJson ({
       type := { pp?, sexp? }, module? }:
-      Commands.LibInspectResult)),
+      Protocol.LibInspectResult)),
    subroutine_step "options.print"
      []
     (Lean.toJson ({ options with printExprAST := true }:
-      Commands.OptionsPrintResult))
+      Protocol.OptionsPrintResult))
  ]
 def test_malformed_command : IO LSpec.TestSeq :=
  let invalid := "invalid"
@ -75,19 +75,38 @@ def test_malformed_command : IO LSpec.TestSeq :=
      [("name", .str "Nat.add_one")]
     (Lean.toJson ({
       error := "command", desc := s!"Unknown command {invalid}"}:
-      Commands.InteractionError)),
+      Protocol.InteractionError)),
    subroutine_named_step "JSON Deserialization" "expr.echo"
      [(invalid, .str "Random garbage data")]
     (Lean.toJson ({
-       error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
-      Commands.InteractionError))
+       error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
+      Protocol.InteractionError))
+  ]
+def test_tactic : IO LSpec.TestSeq :=
+  let goal: Protocol.Goal := {
+    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
+    vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+  }
+  subroutine_runner [
+    subroutine_step "goal.start"
+      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     (Lean.toJson ({stateId := 0}:
+      Protocol.GoalStartResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+     (Lean.toJson ({
+       nextStateId? := .some 1,
+       goals? := #[goal],
+     }:
+      Protocol.GoalTacticResult))
  ]

-def test_integration: IO LSpec.TestSeq := do
+def suite: IO LSpec.TestSeq := do

  return LSpec.group "Integration" $
    (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command))
+    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Tactic" (← test_tactic))


-end Pantograph.Test
+end Pantograph.Test.Integration
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -1,4 +1,5 @@
 import LSpec
+--import Test.Holes
 import Test.Integration
 import Test.Proofs
 import Test.Serial
@ -10,9 +11,10 @@ unsafe def main := do
  Lean.initSearchPath (← Lean.findSysroot)

  let suites := [
-    test_integration,
-    test_proofs,
-    test_serial
+    --Holes.suite,
+    Integration.suite,
+    Proofs.suite,
+    Serial.suite
  ]
  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
  LSpec.lspecIO $ all
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -1,8 +1,23 @@
+/-
+Tests pertaining to goals with no interdependencies
+-/
 import LSpec
-import Pantograph.Tactic
+import Pantograph.Goal
 import Pantograph.Serial
+import Test.Common

-namespace Pantograph.Test
+namespace Pantograph
+
+def TacticResult.toString : TacticResult → String
+  | .success state => s!".success ({state.goals.length} goals)"
+  | .failure messages =>
+    let messages := "\n".intercalate messages.toList
+    s!".failure {messages}"
+  | .parseError error => s!".parseError {error}"
+  | .indexError index => s!".indexError {index}"
+end Pantograph
+
+namespace Pantograph.Test.Proofs
 open Pantograph
 open Lean

@ -10,21 +25,21 @@ inductive Start where
  | copy (name: String) -- Start from some name in the environment
  | expr (expr: String) -- Start from some expression

-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)

-deriving instance DecidableEq, Repr for Commands.Expression
-deriving instance DecidableEq, Repr for Commands.Variable
-deriving instance DecidableEq, Repr for Commands.Goal
+deriving instance DecidableEq, Repr for Protocol.Expression
+deriving instance DecidableEq, Repr for Protocol.Variable
+deriving instance DecidableEq, Repr for Protocol.Goal

-def add_test (test: LSpec.TestSeq): TestM Unit := do
+def addTest (test: LSpec.TestSeq): TestM Unit := do
  set $ (← get) ++ test

-def start_proof (start: Start): TestM (Option GoalState) := do
+def startProof (start: Start): TestM (Option GoalState) := do
  let env ← Lean.MonadEnv.getEnv
  match start with
  | .copy name =>
    let cInfo? := str_to_name name |> env.find?
-    add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
+    addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
    match cInfo? with
    | .some cInfo =>
      let goal ← GoalState.create (expr := cInfo.type)
@ -33,14 +48,14 @@ def start_proof (start: Start): TestM (Option GoalState) := do
      return Option.none
  | .expr expr =>
    let syn? := syntax_from_str env expr
-    add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
    match syn? with
    | .error error =>
      IO.println error
      return Option.none
    | .ok syn =>
-      let expr? ← syntax_to_expr syn
-      add_test $ LSpec.check s!"Elaborating" expr?.isOk
+      let expr? ← syntax_to_expr_type syn
+      addTest $ LSpec.check s!"Elaborating" expr?.isOk
      match expr? with
      | .error error =>
        IO.println error
@ -49,72 +64,146 @@ def start_proof (start: Start): TestM (Option GoalState) := do
        let goal ← GoalState.create (expr := expr)
        return Option.some goal

-def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
+def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false

-def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
+def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal :=
  {
+    caseName?,
    target := { pp? := .some target},
    vars := (nameType.map fun x => ({
-      name := x.fst,
+      userName := x.fst,
      type? := .some { pp? := .some x.snd },
      isInaccessible? := .some false
    })).toArray
  }
-- Like `build_goal` but allow certain variables to be elided.
-def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
-  {
-    target := { pp? := .some target},
-    vars := (nameType.map fun x => ({
-      name := x.fst,
-      type? := x.snd.map (λ type => { pp? := type }),
-      isInaccessible? := x.snd.map (λ _ => false)
-    })).toArray
-  }
+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 := {
+    currNamespace := Name.append .anonymous "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  let coreM := metaM.run'
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok (_, a) =>
+    return a

 -- Individual test cases
 example: ∀ (a b: Nat), a + b = b + a := by
  intro n m
  rw [Nat.add_comm]
-def proof_nat_add_comm: TestM Unit := do
-  let goal? ← start_proof (.copy "Nat.add_comm")
-  add_test $ LSpec.check "Start goal" goal?.isSome
-  if let .some goal := goal? then
-    if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
-      let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-      add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
+def proof_nat_add_comm (manual: Bool): TestM Unit := do
+  let state? ← startProof <| match manual with
+    | false => .copy "Nat.add_comm"
+    | true => .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 ()

-      if let .failure #[message] ← goal.execute "assumption" then
-        add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
-      else
-        add_test $ assert_unreachable "assumption"
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])

-      if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
-        return ()
-      else
-        add_test $ assert_unreachable "rw [Nat.add_comm]"
-    else
-      add_test $ assert_unreachable "intro n m"
-def proof_nat_add_comm_manual: TestM Unit := do
-  let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
-  add_test $ LSpec.check "Start goal" goal?.isSome
-  if let .some goal := goal? then
-    if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
-      let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-      add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
+  match ← state1.execute (goalId := 0) (tactic := "assumption") with
+  | .failure #[message] =>
+    addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
+  | other => do
+    addTest $ assertUnreachable $ other.toString

-      if let .failure #[message] ← goal.execute "assumption" then
-        add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
-      else
-        add_test $ assert_unreachable "assumption"
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty

-      if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
-        return ()
-      else
-        add_test $ assert_unreachable "rw [Nat.add_comm]"
-    else
-      add_test $ assert_unreachable "intro n m"
+  return ()
+def proof_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.execute (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.execute (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 }),
+        isInaccessible? := x.snd.map (λ _ => false)
+      })).toArray
+    }
+
+example (w x y z : Nat) (p : Nat → Prop)
+        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
+  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
+  assumption
+def proof_arith: TestM Unit := do
+  let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intros" (state1.goals.length = 1)
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  let state2 ← match ← state1.execute (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
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
+  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+  let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "assumption" state3.goals.isEmpty
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+  return ()

 -- Two ways to write the same theorem
 example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
@ -132,121 +221,180 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
  . apply Or.inl
    assumption
 def proof_or_comm: TestM Unit := do
-  let typeProp: Commands.Expression := { pp? := .some "Prop" }
-  let branchGoal (caseName name: String): Commands.Goal := {
-    caseName? := .some caseName,
-    target := { pp? := .some "q ∨ p" },
-    vars := #[
-      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
-    ]
-  }
-  let goal? ← start_proof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
-  add_test $ LSpec.check "Start goal" goal?.isSome
-  if let .some goal := goal? then
-    if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then
-      let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"
-      add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e)
+  let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()

-      if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then
-        add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p")
-        if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then
-          if let .success #[] ← goal.execute "assumption" then
-            return ()
-          else
-            add_test $ assert_unreachable "assumption"
-        else
-          add_test $ assert_unreachable "apply Or.inr"
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
+  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[branchGoal "inl" "p", branchGoal "inr" "q"])

+  let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
+    | .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.execute (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
+  let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
+    | .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.execute (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
+  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
+  -- Ensure the proof can continue from `state4_2`.
+  let state2b ← match state2.continue state4_2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
+  let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
+    | .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.execute (goalId := 0) (tactic := "assumption") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome

-        add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q")
-        if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then
-          if let .success #[] ← goal.execute "assumption" then
-            return ()
-          else
-            add_test $ assert_unreachable "assumption"
-        else
-          add_test $ assert_unreachable "apply Or.inl"
+  return ()
+  where
+    typeProp: Protocol.Expression := { pp? := .some "Prop" }
+    branchGoal (caseName name: String): Protocol.Goal := {
+      caseName? := .some caseName,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
+        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
+        { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
+      ]
+    }

-      else
-        add_test $ assert_unreachable "cases h"
-    else
-      add_test $ assert_unreachable "intro p q h"
+/-- M-coupled goals -/
+def proof_m_couple: TestM Unit := do
+  let state? ← startProof (.expr "(2: Nat) ≤ 5")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()

-example (w x y z : Nat) (p : Nat → Prop)
-        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
-  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
-  assumption
-def proof_arith_1: TestM Unit := do
-  let goal? ← start_proof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
-  add_test $ LSpec.check "Start goal" goal?.isSome
-  if let .some goal := goal? then
-    if let .success #[(goal, _)] ← goal.execute "intros" then
-      if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then
-        if let .success #[] ← goal.execute "assumption" then
-          return ()
-        else
-          add_test $ assert_unreachable "assumption"
-      else
-        add_test $ assert_unreachable "simp ..."
-    else
-      add_test $ assert_unreachable "intros"
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+    | .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"])
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  -- Set m to 3
+  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  let state1b ← match state1.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "2 ≤ 3", .some "3 ≤ 5"])
+  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  return ()

-def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do
-  let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
-  add_test $ LSpec.check "Start goal" goal?.isSome
-  if let .some goal := goal? then
-    if let .success #[(goal, sGoal)] ← goal.execute "intro n" then
-      let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
-      add_test $ LSpec.check "intro n" (sGoal = sGoal1e)
+def proof_proposition_generation: TestM Unit := do
+  let state? ← startProof (.expr "Σ' p:Prop, p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()

-      if let .success #[(_, sGoal)] ← goal.execute "intro m" then
-        let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
-        add_test $ LSpec.check "intro m" (sGoal = sGoal2e)
-      else
-        add_test $ assert_unreachable "intro m"
-    else
-      add_test $ assert_unreachable "intro n"
+  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      buildGoal [] "?fst" (caseName? := .some "snd"),
+      buildGoal [] "Prop" (caseName? := .some "fst")
+      ])
+  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone

-def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
-  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
+  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone

-  let coreContext: Lean.Core.Context := {
-    currNamespace := str_to_name "Aniva",
-    openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
-    fileMap := { source := "", positions := #[0], lines := #[1] }
-  }
-  let metaM := termElabM.run' (ctx := {
-    declName? := some "_pantograph",
-    errToSorry := false
-  })
-  let coreM := metaM.run'
-  match ← (coreM.run' coreContext { env := env }).toBaseIO with
-  | .error exception =>
-    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
-  | .ok (_, a) =>
-    return a
+  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
+    #[])
+  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
+  return ()

-def test_proofs : IO LSpec.TestSeq := do
+def suite: IO LSpec.TestSeq := do
  let env: Lean.Environment ← Lean.importModules
-    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
    (opts := {})
    (trustLevel := 1)
  let tests := [
-    ("Nat.add_comm", proof_nat_add_comm),
-    ("nat.add_comm manual", proof_nat_add_comm_manual),
+    ("Nat.add_comm", proof_nat_add_comm false),
+    ("Nat.add_comm manual", proof_nat_add_comm true),
+    ("Nat.add_comm delta", proof_delta_variable),
+    ("arithmetic", proof_arith),
    ("Or.comm", proof_or_comm),
-    ("arithmetic 1", proof_arith_1),
-    ("delta variable", proof_delta_variable)
+    ("2 < 5", proof_m_couple),
+    ("Proposition Generation", proof_proposition_generation)
  ]
  let tests ← tests.foldlM (fun acc tests => do
    let (name, tests) := tests
-    let tests ← proof_runner env tests
+    let tests ← proofRunner env tests
    return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done

  return LSpec.group "Proofs" tests

-end Pantograph.Test
-
+end Pantograph.Test.Proofs
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -1,19 +1,19 @@
 import LSpec
 import Pantograph.Serial
-import Pantograph.Symbols
+import Pantograph.Symbol

-namespace Pantograph.Test
+namespace Pantograph.Test.Serial

 open Pantograph
 open Lean

-deriving instance Repr, DecidableEq for Commands.BoundExpression
+deriving instance Repr, DecidableEq for Protocol.BoundExpression

 def test_str_to_name: LSpec.TestSeq :=
    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")

 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (String × Commands.BoundExpression) := [
+  let entries: List (String × Protocol.BoundExpression) := [
    ("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
    ("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
  ]
@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
  let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
    let env ← MonadEnv.getEnv
    let expr := str_to_name symbol |> env.find? |>.get! |>.type
-    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
-    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+    let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
  let coreM := metaM.run'
  let coreContext: Core.Context := {
    currNamespace := Lean.Name.str .anonymous "Aniva"
@ -62,15 +62,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
  | .ok a            => return a


-def test_serial: IO LSpec.TestSeq := do
+def suite: IO LSpec.TestSeq := do
  let env: Environment ← importModules
    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)

-  return LSpec.group "Serialisation" $
+  return LSpec.group "Serialization" $
    (LSpec.group "str_to_name" test_str_to_name) ++
    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))

-end Pantograph.Test
+end Pantograph.Test.Serial