Main.lean

@@ -8,7 +8,7 @@ import Pantograph
 open Pantograph
 
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
-def parseCommand (s: String): Except String Protocol.Command := do
+def parse_command (s: String): Except String Commands.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 parseCommand command with
+  match parse_command command with
   | .error error =>
-    let error  := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
+    let error  := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
     IO.println error.compress
   | .ok command =>

Makefile

@@ -6,7 +6,7 @@ TEST_EXE := build/bin/test
 TEST_SOURCE := $(wildcard Test/*.lean)
 
 $(LIB) $(EXE): $(SOURCE)
-	lake build pantograph
+	lake build
 
 $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 	lake build test
@@ -14,7 +14,4 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
 test: $(TEST_EXE)
 	lake env $(TEST_EXE)
 
-clean:
-	lake clean
-
-.PHONY: test clean
+.PHONY: test

Pantograph.lean

@@ -1,8 +1,8 @@
-import Pantograph.Goal
-import Pantograph.Protocol
-import Pantograph.SemihashMap
+import Pantograph.Commands
 import Pantograph.Serial
-import Pantograph.Symbol
+import Pantograph.Symbols
+import Pantograph.Tactic
+import Pantograph.SemihashMap
 
 namespace Pantograph
 
@@ -11,16 +11,16 @@ structure Context where
 
 /-- Stores state of the REPL -/
 structure State where
-  options: Protocol.Options := {}
+  options: Commands.Options := {}
   goalStates: SemihashMap GoalState := SemihashMap.empty
 
-/-- Main state monad for executing commands -/
+-- State monad
 abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
--- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
--- certain monadic features in `MainM`
-abbrev CR α := Except Protocol.InteractionError α
+-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
+-- monadic features in `MainM`
+abbrev CR α := Except Commands.InteractionError α
 
-def execute (command: Protocol.Command): MainM Lean.Json := do
+def execute (command: Commands.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
@@ -40,31 +40,31 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   | "goal.tactic"    => run goal_tactic
   | "goal.delete"    => run goal_delete
   | cmd =>
-    let error: Protocol.InteractionError :=
+    let error: Commands.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
-  errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
+  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   -- Command Functions
-  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
+  reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with goalStates := SemihashMap.empty }
     return .ok { nGoals }
-  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
+  stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
     return .ok { nGoals }
-  lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
+  lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.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: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
+  lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let name := str_to_name args.name
@@ -84,7 +84,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         value? := ← value?.mapM (λ v => serialize_expression state.options v),
         module? := module?
       }
-  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
+  expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     match syntax_from_str env args.expr with
@@ -101,7 +101,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           }
         catch exception =>
           return .error $ errorI "typing" (← exception.toMessageData.toString)
-  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
+  options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
     let state ← get
     let options := state.options
     set { state with
@@ -116,9 +116,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       }
     }
     return .ok {  }
-  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
+  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
     return .ok (← get).options
-  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
+  goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@@ -140,32 +140,34 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | .error error => return .error error
     | .ok expr =>
       let goalState ← GoalState.create expr
-      let (goalStates, stateId) := state.goalStates.insert goalState
+      let (goalStates, goalId) := state.goalStates.insert goalState
       set { state with goalStates }
-      return .ok { stateId }
-  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
+      return .ok { goalId }
+  goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
     let state ← get
-    match state.goalStates.get? args.stateId with
-    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
+    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.goalId args.tactic |>.run state.options
+      let result ← GoalState.execute goalState args.tactic |>.run state.options
       match result with
-      | .success nextGoalState goals =>
-        let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
-        set { state with goalStates }
-        return .ok {
-          nextStateId? := .some nextStateId,
-          goals? := .some goals
-        }
-      | .parseError message =>
-        return .ok { parseError? := .some message }
-      | .indexError goalId =>
-        return .error $ errorIndex s!"Invalid goal id index {goalId}"
+      | .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 =>
         return .ok { tacticErrors? := .some messages }
-  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
+  goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
     let state ← get
-    let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
+    let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
     set { state with goalStates }
     return .ok {}
 

Pantograph/Commands.lean

@@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
 
-namespace Pantograph.Protocol
+namespace Pantograph.Commands
 
 
 /-- Main Option structure, placed here to avoid name collision -/
@@ -132,42 +132,32 @@ abbrev OptionsPrintResult := Options
 
 structure GoalStart where
   -- Only one of the fields below may be populated.
-  expr: Option String     -- Directly parse in an expression
-  copyFrom: Option String -- Copy the type from a theorem in the environment
+  expr: Option String     -- Proof expression
+  copyFrom: Option String -- Theorem name
   deriving Lean.FromJson
 structure GoalStartResult where
-  stateId: Nat := 0
+  goalId: Nat := 0 -- Proof tree id
   deriving Lean.ToJson
 structure GoalTactic where
   -- Identifiers for tree, state, and goal
-  stateId: Nat
-  goalId: Nat := 0
+  goalId: Nat
   tactic: String
   deriving Lean.FromJson
 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.
+  -- Existence of this field shows success
   goals?: Option (Array Goal)          := .none
-
-  -- Existence of this field shows tactic execution failure
+  -- Next proof state id, if successful
+  goalIds?: Option (Array Nat)          := .none
+  -- Existence of this field shows failure
   tacticErrors?: Option (Array String) := .none
-
-  -- Existence of this field shows the tactic parsing has failed
-  parseError?: Option String := .none
   deriving Lean.ToJson
 
--- Remove goal states
+-- Remove a bunch of goals.
 structure GoalDelete where
-  stateIds: List Nat
+  goalIds: List Nat
   deriving Lean.FromJson
 structure GoalDeleteResult where
   deriving Lean.ToJson
 
-structure GoalPrint where
-  printContext: Bool := true
-  printValue: Bool := true
-  printNonVisible: Bool := true
 
-
-end Pantograph.Protocol
+end Pantograph.Commands

Pantograph/Goal.lean

@@ -1,159 +0,0 @@
-import Lean
-
-import Pantograph.Symbol
-import Pantograph.Serial
-import Pantograph.Protocol
-
-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
-
-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 savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
-  return {
-    savedState,
-    root := goal.mvarId!,
-    newMVars := SSet.empty,
-  }
-protected def GoalState.goals (goalState: GoalState): List MVarId := goalState.savedState.tactic.goals
-
-def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    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
-        let unsolved ← Elab.Tactic.getUnsolvedGoals
-        -- The order of evaluation is important here, since `getUnsolvedGoals` prunes the goals set
-        return .ok (← MonadBacktrack.saveState, unsolved)
-    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) (goals: Array Protocol.Goal)
-  -- 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):
-    Protocol.OptionsT 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
-  let options ← read
-  match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
-  | .error errors =>
-    return .failure errors
-  | .ok (nextSavedState, nextGoals) =>
-    assert! nextSavedState.tactic.goals.length == nextGoals.length
-    -- 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 mvarId :: acc
-      ) []).toSSet
-    let nextState: GoalState := {
-      savedState := nextSavedState
-      root := state.root,
-      newMVars,
-    }
-    nextSavedState.term.restore
-    let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal
-    let goals ← nextGoals.mapM fun nextGoal => do
-      match (← MonadMCtx.getMCtx).findDecl? nextGoal with
-      | .some mvarDecl =>
-        let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
-        return serializedGoal
-      | .none => throwError s!"Parent mvar id does not exist {nextGoal.name}"
-    return .success nextState goals.toArray
-
--- Diagnostics functions
-
-/-- Print the metavariables in a readable format -/
-protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrint := {}): Elab.TermElabM Unit := do
-  let savedState := goalState.savedState
-  savedState.term.restore
-  let goals := savedState.tactic.goals
-  let mctx ← getMCtx
-  goals.forM (fun mvarId => do
-    let pref := "⊢"
-    match mctx.decls.find? mvarId with
-    | .some decl => printMVar pref mvarId decl
-    | .none => IO.println s!"{pref}{mvarId.name}: ??"
-  )
-  let goals := goals.toSSet
-  mctx.decls.forM (fun mvarId decl => do
-    if goals.contains mvarId then
-      pure ()
-    else if mvarId == goalState.root then
-      printMVar (pref := ">") mvarId decl
-    else if ¬(goalState.newMVars.contains mvarId) then
-      printMVar (pref := " ") mvarId decl
-    else if options.printNonVisible then
-      printMVar (pref := "~") mvarId decl
-    else
-      IO.println s!" {mvarId.name}{userNameToString decl.userName}"
-  )
-  where
-    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do
-      if options.printContext then
-        decl.lctx.fvarIdToDecl.forM printFVar
-      IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {← serialize_expression_ast decl.type}"
-      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): Elab.TermElabM Unit := do
-      IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
-    userNameToString : Name → String
-      | .anonymous => ""
-      | other => s!"[{other}]"
-
-end Pantograph

Pantograph/Serial.lean

@@ -3,7 +3,7 @@ All serialisation functions
 -/
 import Lean
 
-import Pantograph.Protocol
+import Pantograph.Commands
 
 namespace Pantograph
 open Lean
@@ -28,18 +28,26 @@ 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 Protocol.BoundExpression := do
+def type_expr_to_bound (expr: Expr): MetaM Commands.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)))
@@ -108,7 +116,7 @@ def serialize_expression_ast (expr: Expr): MetaM String := do
     -- Lean these are handled using a `#` prefix.
     return s!"{deBruijnIndex}"
   | .fvar fvarId =>
-    let name := name_to_ast fvarId.name
+    let name := (← fvarId.getDecl).userName
     return s!"(:fv {name})"
   | .mvar mvarId =>
     let name := name_to_ast mvarId.name
@@ -166,7 +174,7 @@ def serialize_expression_ast (expr: Expr): MetaM String := do
     | .strictImplicit => " :strictImplicit"
     | .instImplicit => " :instImplicit"
 
-def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do
   let pp := toString (← Meta.ppExpr e)
   let pp?: Option String := match options.printExprPretty with
       | true => .some pp
@@ -181,8 +189,8 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
-      : MetaM Protocol.Goal := do
+def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+      : MetaM Commands.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
   let ppAuxDecls     := options.printAuxDecls
@@ -190,7 +198,7 @@ def serialize_goal (options: Protocol.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 Protocol.Variable := do
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
       match localDecl with
       | .cdecl _ _ varName _ _ _ =>
         let varName := varName.simpMacroScopes
@@ -201,7 +209,7 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
         return {
           name := toString varName,
         }
-    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
+    let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
       match localDecl with
       | .cdecl _ _ varName type _ _ =>
         let varName := varName.simpMacroScopes
@@ -241,7 +249,7 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
       caseName? := match mvarDecl.userName with
         | Name.anonymous => .none
         | name => .some <| toString name,
-      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
+      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
       target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }

Pantograph/Symbols.lean

@@ -1,8 +1,10 @@
+/-
+ - 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
 

Pantograph/Tactic.lean

@@ -0,0 +1,102 @@
+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

Pantograph/Version.lean

@@ -1,5 +1,5 @@
 namespace Pantograph
 
-def version := "0.2.6"
+def version := "0.2.5"
 
 end Pantograph

Test/Holes.lean

@@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Goal
+import Pantograph.Tactic
 import Pantograph.Serial
 
 namespace Pantograph.Test.Holes

Test/Integration.lean

@@ -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: Protocol.Options := {}
+  let options: Commands.Options := {}
   subroutine_runner [
     subroutine_step "lib.inspect"
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        type := { pp? }, module? }:
-      Protocol.LibInspectResult)),
+      Commands.LibInspectResult)),
     subroutine_step "options.set"
       [("printExprAST", .bool true)]
      (Lean.toJson ({ }:
-      Protocol.OptionsSetResult)),
+      Commands.OptionsSetResult)),
     subroutine_step "lib.inspect"
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        type := { pp?, sexp? }, module? }:
-      Protocol.LibInspectResult)),
+      Commands.LibInspectResult)),
     subroutine_step "options.print"
       []
      (Lean.toJson ({ options with printExprAST := true }:
-      Protocol.OptionsPrintResult))
+      Commands.OptionsPrintResult))
   ]
 def test_malformed_command : IO LSpec.TestSeq :=
   let invalid := "invalid"
@@ -75,12 +75,12 @@ def test_malformed_command : IO LSpec.TestSeq :=
       [("name", .str "Nat.add_one")]
      (Lean.toJson ({
        error := "command", desc := s!"Unknown command {invalid}"}:
-      Protocol.InteractionError)),
+      Commands.InteractionError)),
     subroutine_named_step "JSON Deserialization" "expr.echo"
       [(invalid, .str "Random garbage data")]
      (Lean.toJson ({
-       error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
-      Protocol.InteractionError))
+       error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
+      Commands.InteractionError))
   ]
 
 def suite: IO LSpec.TestSeq := do

Test/Main.lean

@@ -1,5 +1,5 @@
 import LSpec
---import Test.Holes
+import Test.Holes
 import Test.Integration
 import Test.Proofs
 import Test.Serial
@@ -11,7 +11,7 @@ unsafe def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    --Holes.suite,
+    Holes.suite,
     Integration.suite,
     Proofs.suite,
     Serial.suite

Test/Proofs.lean

@@ -1,21 +1,7 @@
-/-
-Tests pertaining to goals with no interdependencies
--/
 import LSpec
-import Pantograph.Goal
+import Pantograph.Tactic
 import Pantograph.Serial
 
-namespace Pantograph
-
-def TacticResult.toString : TacticResult → String
-  | .success _ goals => s!".success ({goals.size} 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
@@ -24,21 +10,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 Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
 
-deriving instance DecidableEq, Repr for Protocol.Expression
-deriving instance DecidableEq, Repr for Protocol.Variable
-deriving instance DecidableEq, Repr for Protocol.Goal
+deriving instance DecidableEq, Repr for Commands.Expression
+deriving instance DecidableEq, Repr for Commands.Variable
+deriving instance DecidableEq, Repr for Commands.Goal
 
-def addTest (test: LSpec.TestSeq): TestM Unit := do
+def add_test (test: LSpec.TestSeq): TestM Unit := do
   set $ (← get) ++ test
 
-def startProof (start: Start): TestM (Option GoalState) := do
+def start_proof (start: Start): TestM (Option GoalState) := do
   let env ← Lean.MonadEnv.getEnv
   match start with
   | .copy name =>
     let cInfo? := str_to_name name |> env.find?
-    addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
+    add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
     match cInfo? with
     | .some cInfo =>
       let goal ← GoalState.create (expr := cInfo.type)
@@ -47,14 +33,14 @@ def startProof (start: Start): TestM (Option GoalState) := do
       return Option.none
   | .expr expr =>
     let syn? := syntax_from_str env expr
-    addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    add_test $ 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_type syn
-      addTest $ LSpec.check s!"Elaborating" expr?.isOk
+      let expr? ← syntax_to_expr syn
+      add_test $ LSpec.check s!"Elaborating" expr?.isOk
       match expr? with
       | .error error =>
         IO.println error
@@ -63,9 +49,9 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some goal
 
-def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
+def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goal :=
+def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
   {
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
@@ -74,8 +60,8 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa
       isInaccessible? := .some false
     })).toArray
   }
--- Like `buildGoal` but allow certain variables to be elided.
-def buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
+-- 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 => ({
@@ -84,62 +70,50 @@ def buildGoalSelective (nameType: List (String × Option String)) (target: Strin
       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 (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 ()
+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)
 
-  let (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
-    | .success state #[goal] => pure (state, goal)
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n")
+      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"
 
-  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 .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)
 
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
-    | .success state #[] => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      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"
 
-  return ()
+      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"
 
 
 -- Two ways to write the same theorem
@@ -158,122 +132,119 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
   . apply Or.inl
     assumption
 def proof_or_comm: TestM Unit := do
-  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 ()
+  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 (state1, goal1) ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
-    | .success state #[goal] => pure (state, goal)
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p")
-  let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
-    | .success state #[goal1, goal2] => pure (state, goal1, goal2)
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p")
-  addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q")
+      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 (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state #[goal] => pure (state, goal)
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
-    | .success state #[] => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  IO.println "=====  1  ====="
-  state1.print
-  IO.println "=====  2  ====="
-  state2.print
-  IO.println "===== 4_1 ====="
-  state4_1.print
-  let (state3_2, _goal) ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
-    | .success state #[goal] => pure (state, goal)
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  IO.println "===== 3_2 ====="
-  state3_2.print
-  let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
-    | .success state #[] => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  IO.println "===== 4_2 ====="
-  state4_2.print
 
-  return ()
-  where
-    typeProp: Protocol.Expression := { pp? := .some "Prop" }
-    branchGoal (caseName name: String): Protocol.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 }
-      ]
-    }
+        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"
 
---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? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
---  addTest $ 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
---          addTest $ assertUnreachable "assumption"
---      else
---        addTest $ assertUnreachable "simp ..."
---    else
---      addTest $ assertUnreachable "intros"
---
---def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do
---  let goal? ← startProof (.expr "∀ (a b: Nat), a + b = b + a")
---  addTest $ LSpec.check "Start goal" goal?.isSome
---  if let .some goal := goal? then
---    if let .success #[(goal, sGoal)] ← goal.execute "intro n" then
---      let sGoal1e: Protocol.Goal :=buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
---      addTest $ LSpec.check "intro n" (sGoal = sGoal1e)
---
---      if let .success #[(_, sGoal)] ← goal.execute "intro m" then
---        let sGoal2e: Protocol.Goal :=buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
---        addTest $ LSpec.check "intro m" (sGoal = sGoal2e)
---      else
---        addTest $ assertUnreachable "intro m"
---    else
---      addTest $ assertUnreachable "intro n"
+      else
+        add_test $ assert_unreachable "cases h"
+    else
+      add_test $ assert_unreachable "intro p q h"
+
+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"
+
+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)
+
+      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"
+
+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
 
 /-- Tests the most basic form of proofs whose goals do not relate to each other -/
 def suite: IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
-    (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
+    (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   let tests := [
-    ("Nat.add_comm", proof_nat_add_comm false),
-    ("Nat.add_comm manual", proof_nat_add_comm true),
-    ("Or.comm", proof_or_comm)
-    --("arithmetic 1", proof_arith_1),
-    --("delta variable", proof_delta_variable)
+    ("Nat.add_comm", proof_nat_add_comm),
+    ("nat.add_comm manual", proof_nat_add_comm_manual),
+    ("Or.comm", proof_or_comm),
+    ("arithmetic 1", proof_arith_1),
+    ("delta variable", proof_delta_variable)
   ]
   let tests ← tests.foldlM (fun acc tests => do
     let (name, tests) := tests
-    let tests ← proofRunner env tests
+    let tests ← proof_runner env tests
     return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
 
   return LSpec.group "Proofs" tests

Test/Serial.lean

@@ -1,19 +1,19 @@
 import LSpec
 import Pantograph.Serial
-import Pantograph.Symbol
+import Pantograph.Symbols
 
 namespace Pantograph.Test.Serial
 
 open Pantograph
 open Lean
 
-deriving instance Repr, DecidableEq for Protocol.BoundExpression
+deriving instance Repr, DecidableEq for Commands.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 × Protocol.BoundExpression) := [
+  let entries: List (String × Commands.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" })
   ]