Main.lean

@@ -43,7 +43,7 @@ partial def loop : MainM Unit := do repeat do
         | false => ret.compress
       IO.println str
     catch e =>
-      let message := e.toString
+      let message ← e.toMessageData.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
       IO.println error.compress
 
@@ -60,10 +60,11 @@ unsafe def main (args: List String): IO Unit := do
   let (options, imports) := args.partition (·.startsWith "--")
   let coreContext ← options.map (·.drop 2) |>.toArray |> Pantograph.createCoreContext
   let coreState ← Pantograph.createCoreState imports.toArray
+  let context: Context := {}
   try
-    let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
+    let coreM := loop.run context |>.run' {}
     IO.println "ready."
-    mainM
+    discard <| coreM.toIO coreContext coreState
   catch ex =>
     let message := ex.toString
     let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)

Pantograph/Goal.lean

@@ -85,19 +85,12 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
 
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
--- Restore the name generator and macro scopes of the core state
+protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
-protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
-  let savedCore := state.coreState
-  modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
-protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
-  state.restoreCoreMExtra
   state.savedState.term.meta.restore
-protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
-  state.restoreCoreMExtra
   state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
-  state.restoreElabM
+  state.savedState.restore
   Elab.Tactic.setGoals [goal]
 
 @[export pantograph_goal_state_focus]
@@ -222,7 +215,7 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
   goal.checkNotAssigned `GoalState.step
   let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
-  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+  Elab.Term.synthesizeSyntheticMVarsNoPostponing
 
   let goals ← if guardMVarErrors then
       pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
@@ -287,7 +280,6 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  assert! ¬ (← goal.isAssigned)
   state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):

Pantograph/Protocol.lean

@@ -103,7 +103,7 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String := .none
+  type?: Option String
   -- universe levels
   levels: Option (Array String) := .none
   deriving Lean.FromJson
@@ -217,14 +217,14 @@ structure EnvSaveLoadResult where
 
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
-  printJsonPretty?: Option Bool := .none
+  printJsonPretty?: Option Bool
-  printExprPretty?: Option Bool := .none
+  printExprPretty?: Option Bool
-  printExprAST?: Option Bool := .none
+  printExprAST?: Option Bool
-  printDependentMVars?: Option Bool := .none
+  printDependentMVars?: Option Bool
-  noRepeat?: Option Bool := .none
+  noRepeat?: Option Bool
-  printAuxDecls?: Option Bool := .none
+  printAuxDecls?: Option Bool
-  printImplementationDetailHyps?: Option Bool := .none
+  printImplementationDetailHyps?: Option Bool
-  automaticMode?: Option Bool := .none
+  automaticMode?: Option Bool
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -236,7 +236,7 @@ structure GoalStart where
   expr: Option String     -- Directly parse in an expression
   -- universe levels
   levels: Option (Array String) := .none
-  copyFrom: Option String := .none -- Copy the type from a theorem in the environment
+  copyFrom: Option String -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0

Repl.lean

@@ -6,28 +6,18 @@ namespace Pantograph.Repl
 open Lean
 
 structure Context where
-  coreContext : Core.Context
 
 /-- Stores state of the REPL -/
 structure State where
-  options : Protocol.Options := {}
+  options: Protocol.Options := {}
-  nextId : Nat := 0
+  nextId: Nat := 0
-  goalStates : Std.HashMap Nat GoalState := Std.HashMap.empty
+  goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
-
-  env : Environment
-  -- Parser state
-  scope : Elab.Command.Scope := { header := "" }
 
 /-- Main state monad for executing commands -/
-abbrev MainM := ReaderT Context $ StateRefT State IO
+abbrev MainM := ReaderT Context $ StateRefT State CoreM
-def getMainState : MainM State := get
 /-- Fallible subroutine return type -/
 abbrev CR α := Except Protocol.InteractionError α
 
-instance : MonadEnv MainM where
-  getEnv := return (← get).env
-  modifyEnv f := modify fun s => { s with env := f s.env  }
-
 def newGoalState (goalState: GoalState) : MainM Nat := do
   let state ← get
   let stateId := state.nextId
@@ -37,25 +27,11 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
   }
   return stateId
 
-def runCoreM { α } (coreM : CoreM α) : MainM α := do
-  let scope := (← get).scope
-  let coreCtx : Core.Context := {
-    (← read).coreContext with
-    currNamespace      := scope.currNamespace
-    openDecls          := scope.openDecls
-    options            := scope.opts
-  }
-  let coreState : Core.State := {
-    env := (← get).env
-  }
-  let (result, state') ← coreM.toIO coreCtx coreState
-  modifyEnv λ _ => state'.env
-  return result
 
-def liftMetaM { α } (metaM : MetaM α): MainM α :=
+def runMetaInMainM { α } (metaM: MetaM α): MainM α :=
-  runCoreM metaM.run'
+  metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) : MainM α :=
+def runTermElabInMainM { α } (termElabM: Elab.TermElabM α) : MainM α :=
-  runCoreM $ termElabM.run' (ctx := defaultElabContext) |>.run'
+  termElabM.run' (ctx := defaultElabContext) |>.run'
 
 section Frontend
 
@@ -69,7 +45,7 @@ structure CompilationUnit where
   newConstants : List Name
 
 def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-  let options := (← getMainState).options
+  let options := (← get).options
   let (fileName, file) ← match args.fileName?, args.file? with
     | .some fileName, .none => do
       let file ← IO.FS.readFile fileName
@@ -109,9 +85,6 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
   let (li, state') ← frontendM.run context |>.run state
   if args.inheritEnv then
     setEnv state'.commandState.env
-    if let .some scope := state'.commandState.scopes.head? then
-      -- modify the scope
-      set { ← getMainState with scope }
   let units ← li.mapM λ step => withEnv step.env do
     let newConstants? := if args.newConstants then
         .some $ step.newConstants.toArray.map λ name => name.toString
@@ -120,11 +93,9 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
     let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
         pure (.none, .none, .none)
       else do
-        let ({ state, srcBoundaries }, goals) ← liftMetaM do
+        let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState step.sorrys
-          let result@{state, .. } ← Frontend.sorrysToGoalState step.sorrys
-          let goals ← goalSerialize state options
-          pure (result, goals)
         let stateId ← newGoalState state
+        let goals ← goalSerialize state options
         let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
         pure (.some stateId, .some goals, .some srcBoundaries)
     let invocations? := if args.invocations then .some step.invocations else .none
@@ -150,58 +121,63 @@ def execute (command: Protocol.Command): MainM Json := do
       | .ok result =>  return toJson result
       | .error ierror => return toJson ierror
     | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
-  match command.cmd with
+  try
-  | "reset"         => run reset
+    match command.cmd with
-  | "stat"          => run stat
+    | "reset"         => run reset
-  | "expr.echo"     => run expr_echo
+    | "stat"          => run stat
-  | "env.describe"  => run env_describe
+    | "expr.echo"     => run expr_echo
-  | "env.module_read" => run env_module_read
+    | "env.describe"  => run env_describe
-  | "env.catalog"   => run env_catalog
+    | "env.module_read" => run env_module_read
-  | "env.inspect"   => run env_inspect
+    | "env.catalog"   => run env_catalog
-  | "env.add"       => run env_add
+    | "env.inspect"   => run env_inspect
-  | "env.save"      => run env_save
+    | "env.add"       => run env_add
-  | "env.load"      => run env_load
+    | "env.save"      => run env_save
-  | "options.set"   => run options_set
+    | "env.load"      => run env_load
-  | "options.print" => run options_print
+    | "options.set"   => run options_set
-  | "goal.start"    => run goal_start
+    | "options.print" => run options_print
-  | "goal.tactic"   => run goal_tactic
+    | "goal.start"    => run goal_start
-  | "goal.continue" => run goal_continue
+    | "goal.tactic"   => run goal_tactic
-  | "goal.delete"   => run goal_delete
+    | "goal.continue" => run goal_continue
-  | "goal.print"    => run goal_print
+    | "goal.delete"   => run goal_delete
-  | "goal.save"     => run goal_save
+    | "goal.print"    => run goal_print
-  | "goal.load"     => run goal_load
+    | "goal.save"     => run goal_save
-  | "frontend.process" => run frontend_process
+    | "goal.load"     => run goal_load
-  | cmd =>
+    | "frontend.process" => run frontend_process
-    let error: Protocol.InteractionError :=
+    | cmd =>
-      errorCommand s!"Unknown command {cmd}"
+      let error: Protocol.InteractionError :=
-    return toJson error
+        errorCommand s!"Unknown command {cmd}"
+      return toJson error
+  catch ex => do
+    let error ← ex.toMessageData.toString
+    return toJson $ errorIO error
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
   errorIO := errorI "io"
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
-    let state ← getMainState
+    let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
+    Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
-    let state ← getMainState
+    let state ← get
     let nGoals := state.goalStates.size
     return .ok { nGoals }
   env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
-    let result ← runCoreM $ Environment.describe args
+    let result ← Environment.describe args
     return .ok result
   env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
-    runCoreM $ Environment.moduleRead args
+    Environment.moduleRead args
   env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
-    let result ← runCoreM $ Environment.catalog args
+    let result ← Environment.catalog args
     return .ok result
   env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
-    let state ← getMainState
+    let state ← get
-    runCoreM $ Environment.inspect args state.options
+    Environment.inspect args state.options
   env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
-    runCoreM $ Environment.addDecl args
+    Environment.addDecl args
   env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
     let env ← MonadEnv.getEnv
     environmentPickle env args.path
@@ -211,10 +187,10 @@ def execute (command: Protocol.Command): MainM Json := do
     setEnv env
     return .ok {}
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
-    let state ← getMainState
+    let state ← get
-    runCoreM $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
+    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
-    let state ← getMainState
+    let state ← get
     let options := state.options
     set { state with
       options := {
@@ -231,12 +207,13 @@ def execute (command: Protocol.Command): MainM Json := do
     }
     return .ok {  }
   options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
-    return .ok (← getMainState).options
+    return .ok (← get).options
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
-    let expr?: Except _ GoalState ← liftTermElabM (match args.expr, args.copyFrom with
+    let env ← MonadEnv.getEnv
+    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
       | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
-      | .none, .some copyFrom => do
+      | .none, .some copyFrom =>
-        (match (← getEnv).find? <| copyFrom.toName with
+        (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
@@ -247,12 +224,12 @@ def execute (command: Protocol.Command): MainM Json := do
       let stateId ← newGoalState goalState
       return .ok { stateId, root := goalState.root.name.toString }
   goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
     let .some goal := goalState.goals.get? args.goalId |
       return .error $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
+    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
       -- NOTE: Should probably use a macro to handle this...
       match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
       | .some tactic, .none, .none, .none, .none, .none, .none => do
@@ -274,26 +251,26 @@ def execute (command: Protocol.Command): MainM Json := do
       | .none, .none, .none, .none, .none, .none, .some draft => do
         pure <| Except.ok <| ← goalState.tryDraft goal draft
       | _, _, _, _, _, _, _ =>
-        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
+        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
-        pure $ .error error
+        pure $ Except.error $ error
     match nextGoalState? with
     | .error error => return .error error
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
-            return .error $ errorIO "Resuming known goals"
+            throwError "Resuming known goals"
           pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |
-            return .error $ errorIO "If conv exit succeeded this should not fail"
+            throwError "If conv exit succeeded this should not fail"
           let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            return .error $ errorIO "Resuming known goals"
+            throwError "Resuming known goals"
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
-      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
+      let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return .ok {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
@@ -305,7 +282,7 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok (.failure messages) =>
       return .ok { tacticErrors? := .some messages }
   goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
-    let state ← getMainState
+    let state ← get
     let .some target := state.goalStates[args.target]? |
       return .error $ errorIndex s!"Invalid state index {args.target}"
     let nextState? ← match args.branch?, args.goals? with
@@ -320,21 +297,21 @@ def execute (command: Protocol.Command): MainM Json := do
     | .error error => return .error <| errorI "structure" error
     | .ok nextGoalState =>
       let nextStateId ← newGoalState nextGoalState
-      let goals ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
+      let goals ← goalSerialize nextGoalState (options := state.options)
       return .ok {
         nextStateId,
         goals,
       }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
-    let state ← getMainState
+    let state ← get
     let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
     set { state with goalStates }
     return .ok {}
   goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.stateId]? |
       return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← liftMetaM <| goalPrint
+    let result ← runMetaInMainM <| goalPrint
         goalState
         (rootExpr := args.rootExpr?.getD False)
         (parentExpr := args.parentExpr?.getD False)
@@ -343,7 +320,7 @@ def execute (command: Protocol.Command): MainM Json := do
         (options := state.options)
     return .ok result
   goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
-    let state ← getMainState
+    let state ← get
     let .some goalState := state.goalStates[args.id]? |
       return .error $ errorIndex s!"Invalid state index {args.id}"
     goalStatePickle goalState args.path
@@ -356,6 +333,6 @@ def execute (command: Protocol.Command): MainM Json := do
     try
       frontend_process_inner args
     catch e =>
-      return .error $ errorI "frontend" e.toString
+      return .error $ errorI "frontend" (← e.toMessageData.toString)
 
 end Pantograph.Repl

Test/Integration.lean

@@ -8,33 +8,23 @@ import Test.Common
 namespace Pantograph.Test.Integration
 open Pantograph.Repl
 
-deriving instance Lean.ToJson for Protocol.EnvInspect
+def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
-deriving instance Lean.ToJson for Protocol.EnvAdd
+    (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
-deriving instance Lean.ToJson for Protocol.ExprEcho
+  let payload := Lean.Json.mkObj payload
-deriving instance Lean.ToJson for Protocol.OptionsSet
-deriving instance Lean.ToJson for Protocol.OptionsPrint
-deriving instance Lean.ToJson for Protocol.GoalStart
-deriving instance Lean.ToJson for Protocol.GoalPrint
-deriving instance Lean.ToJson for Protocol.GoalTactic
-deriving instance Lean.ToJson for Protocol.FrontendProcess
-
-def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
-    (expected: β) (name? : Option String := .none): MainM LSpec.TestSeq := do
-  let payload := Lean.toJson payload
   let name := name?.getD s!"{cmd} {payload.compress}"
   let result ← Repl.execute { cmd, payload }
-  return LSpec.test name (result.pretty = (Lean.toJson expected).pretty)
+  return LSpec.test name (toString result = toString (Lean.toJson expected))
 
 abbrev Test := List (MainM LSpec.TestSeq)
 
-def test_expr_echo : Test :=
+def test_elab : Test :=
   [
     step "expr.echo"
-     ({ expr := "λ {α : Sort (u + 1)} => List α", levels := .some #["u"]}: Protocol.ExprEcho)
+      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
-     ({
+     (Lean.toJson ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult),
+     }: Protocol.ExprEchoResult)),
   ]
 
 def test_option_modify : Test :=
@@ -43,53 +33,49 @@ def test_option_modify : Test :=
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   [
-    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str "Nat.add_one")]
      ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
-    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
+    step "options.set" [("printExprAST", .bool true)]
      ({ }: Protocol.OptionsSetResult),
-    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str "Nat.add_one")]
      ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
-    step "options.print" ({} : Protocol.OptionsPrint)
+    step "options.print" []
      ({ options with printExprAST := true }: Protocol.Options),
   ]
 def test_malformed_command : Test :=
   let invalid := "invalid"
   [
-    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
+    step invalid [("name", .str "Nat.add_one")]
      ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
      (name? := .some "Invalid Command"),
-    step "expr.echo" (Lean.Json.mkObj [(invalid, .str "Random garbage data")])
+    step "expr.echo" [(invalid, .str "Random garbage data")]
      ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
       Protocol.InteractionError)
     (name? := .some "JSON Deserialization")
   ]
 def test_tactic : Test :=
-  let varX := { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}
   let goal1: Protocol.Goal := {
     name := "_uniq.11",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[varX],
+    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.14",
+    name := "_uniq.17",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      varX,
+      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.13", userName := "y", type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
     ],
   }
   [
-    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
+    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
      ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
-    step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
-    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
-     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
-      Protocol.GoalTacticResult)
   ]
 def test_automatic_mode (automatic: Bool): Test :=
   let varsPQ := #[
@@ -128,16 +114,16 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   [
-    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
+    step "options.set" [("automaticMode", .bool automatic)]
      ({}: Protocol.OptionsSetResult),
-    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
      ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
     let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
-    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
+    step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
      ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
   ]
 
@@ -146,28 +132,28 @@ def test_env_add_inspect : Test :=
   let name2 := "Pantograph.mystery2"
   [
     step "env.add"
-      ({
+      [
-        name := name1,
+        ("name", .str name1),
-        type := "Prop → Prop → Prop",
+        ("type", .str "Prop → Prop → Prop"),
-        value := "λ (a b: Prop) => Or a b",
+        ("value", .str "λ (a b: Prop) => Or a b"),
-        isTheorem := false
+        ("isTheorem", .bool false)
-      }: Protocol.EnvAdd)
+      ]
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str name1)]
      ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
       Protocol.EnvInspectResult),
     step "env.add"
-      ({
+      [
-        name := name2,
+        ("name", .str name2),
-        type := "Nat → Int",
+        ("type", .str "Nat → Int"),
-        value := "λ (a: Nat) => a + 1",
+        ("value", .str "λ (a: Nat) => a + 1"),
-        isTheorem := false
+        ("isTheorem", .bool false)
-      }: Protocol.EnvAdd)
+      ]
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
+    step "env.inspect" [("name", .str name2)]
      ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
@@ -180,14 +166,19 @@ example : ∀ (p: Prop), p → p := by
   exact h
 
 def test_frontend_process : Test :=
-  let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
-  let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
   [
+    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
-      ({
+      [
-        file? := .some file,
+        ("file",              .str file),
-        invocations := true,
+        ("invocations",       .bool true),
-      }: Protocol.FrontendProcess)
+        ("readHeader",        .bool false),
+        ("inheritEnv",        .bool false),
+        ("sorrys",            .bool false),
+        ("typeErrorsAsGoals", .bool false),
+        ("newConstants",      .bool false),
+      ]
      ({
        units := [{
          boundary := (0, file.utf8ByteSize),
@@ -223,10 +214,15 @@ def test_frontend_process_sorry : Test :=
       vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
-      ({
+      [
-        file? := .some file,
+        ("file", .str file),
-        sorrys := true,
+        ("readHeader",        .bool false),
-      }: Protocol.FrontendProcess)
+        ("inheritEnv",        .bool false),
+        ("invocations", .bool false),
+        ("sorrys", .bool true),
+        ("typeErrorsAsGoals", .bool false),
+        ("newConstants", .bool false),
+      ]
      ({
        units := [{
          boundary := (0, solved.utf8ByteSize),
@@ -237,46 +233,23 @@ def test_frontend_process_sorry : Test :=
          goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
-     }: Protocol.FrontendProcessResult),
+    }: Protocol.FrontendProcessResult),
   ]
 
-def test_import_open : Test :=
-  let header := "import Init\nopen Nat"
-  let goal1: Protocol.Goal := {
-    name := "_uniq.67",
-    target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
-  }
-  [
-    step "frontend.process"
-      ({
-        file? := .some header,
-        readHeader := true,
-        inheritEnv := true,
-      }: Protocol.FrontendProcess)
-     ({
-       units := [{
-         boundary := (12, header.utf8ByteSize),
-       }],
-     }: Protocol.FrontendProcessResult),
-    step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
-    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
-     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
-     ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
-  ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
-  let coreContext ← createCoreContext #[]
+  let context: Context := {}
-  let mainM : MainM LSpec.TestSeq :=
+  let commands: MainM LSpec.TestSeq :=
-    steps.foldlM (λ suite step => do return suite ++ (← step)) LSpec.TestSeq.done
+    steps.foldlM (λ suite step => do
-  mainM.run { coreContext } |>.run' { env }
+      let result ← step
+      return suite ++ result) LSpec.TestSeq.done
+  runCoreMSeq env <| commands.run context |>.run' {}
+
 
 def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("expr.echo", test_expr_echo),
+    ("expr.echo", test_elab),
     ("options.set options.print", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
@@ -285,7 +258,6 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
-    ("frontend.process import", test_import_open),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

Test/Tactic/Prograde.lean

@@ -87,7 +87,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
         { userName := "q", type? := .some { pp? := .some "Prop" } },
         { userName := "h", type? := .some { pp? := .some "p" } },
         { userName := "y",
-          type? := .some { pp? := .some "p ∨ ?m.19" },
+          type? := .some { pp? := .some "p ∨ ?m.25" },
           value? := .some { pp? := .some "Or.inl h" },
         }
       ]