feat: `CoreM` timeout

2025-03-28 20:42:10 -07:00 · 2025-03-28 20:42:10 -07:00 · 4610348fed
parent be505b8050
commit 4610348fed
7 changed files with 186 additions and 137 deletions
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -52,12 +52,12 @@ def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do
    imports := env.header.imports.map toString,
    modules := env.header.moduleNames.map (·.toString),
  }
-def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do
+def moduleRead (args: Protocol.EnvModuleRead): CoreM Protocol.EnvModuleReadResult := do
  let env ← Lean.MonadEnv.getEnv
  let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) |
-    return .error $ Protocol.errorIndex s!"Module not found {args.module}"
+    throwError s!"Module not found {args.module}"
  let data := env.header.moduleData[i]!
-  return .ok {
+  return {
    imports := data.imports.map toString,
    constNames := data.constNames.map (·.toString),
    extraConstNames := data.extraConstNames.map (·.toString),
@ -69,13 +69,11 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
    | .some x => acc.push x
    | .none => acc)
  return { symbols := names }
-def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
+def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.FallibleT CoreM Protocol.EnvInspectResult := do
  let env ← Lean.MonadEnv.getEnv
  let name :=  args.name.toName
  let info? := env.find? name
-  let info ← match info? with
-    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
-    | some info => pure info
+  let .some info := info? | Protocol.throw $ Protocol.errorIndex s!"Symbol not found {args.name}"
  let module? := env.getModuleIdxFor? name >>=
    (λ idx => env.allImportedModuleNames.get? idx.toNat)
  let value? := match args.value?, info with
@ -145,17 +143,19 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
      }
    else
      .pure result
-  return .ok result
-def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
+  return result
+@[export pantograph_env_add_m]
+def addDecl (name: String) (levels: Array String := #[]) (type: String) (value: String) (isTheorem: Bool)
+    : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
  let env ← Lean.MonadEnv.getEnv
  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match parseTerm env args.type with
+    let type ← match parseTerm env type with
      | .ok syn => do
        match ← elabTerm syn with
        | .error e => return .error e
        | .ok expr => pure expr
      | .error e => return .error e
-    let value ← match parseTerm env args.value with
+    let value ← match parseTerm env value with
      | .ok syn => do
        try
          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
@ -167,16 +167,25 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
    pure $ .ok (type, value)
  let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
    | .ok t => pure t
-    | .error e => return .error $ Protocol.errorExpr e
-  let decl := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
-    (name := args.name.toName)
-    (levelParams := [])
-    (type := type)
-    (value := value)
-    (hints := Lean.mkReducibilityHintsRegularEx 1)
-    (safety := Lean.DefinitionSafety.safe)
-    (all := [])
+    | .error e => Protocol.throw $ Protocol.errorExpr e
+  let levelParams := levels.toList.map (·.toName)
+  let decl := if isTheorem then
+    Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
+      (name := name.toName)
+      (levelParams := levelParams)
+      (type := type )
+      (value := value)
+      (all := [])
+  else
+    Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
+      (name := name.toName)
+      (levelParams := levelParams)
+      (type := type)
+      (value := value)
+      (hints := Lean.mkReducibilityHintsRegularEx 1)
+      (safety := Lean.DefinitionSafety.safe)
+      (all := [])
  Lean.addDecl decl
-  return .ok {}
+  return {}

 end Pantograph.Environment
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -5,8 +5,6 @@ import Pantograph.Delate
 import Pantograph.Version

 import Lean
-import Std.Time
-import Std.Internal.Async

 namespace Lean

@ -78,59 +76,53 @@ def createCoreState (imports: Array String): IO Core.State := do
    (trustLevel := 1)
  return { env := env }

-@[export pantograph_env_add_m]
-def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
-    CoreM (Protocol.CR Protocol.EnvAddResult) :=
-  Environment.addDecl { name, type, value, isTheorem }
-
@[export pantograph_parse_elab_type_m]
-def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
+def parseElabType (type: String): Protocol.FallibleT Elab.TermElabM Expr := do
  let env ← MonadEnv.getEnv
  let syn ← match parseTerm env type with
-    | .error str => return .error $ errorI "parsing" str
+    | .error str => Protocol.throw $ errorI "parsing" str
    | .ok syn => pure syn
  match ← elabType syn with
-  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← instantiateMVars expr)
+  | .error str => Protocol.throw $ errorI "elab" str
+  | .ok expr => return (← instantiateMVars expr)

 /-- This must be a TermElabM since the parsed expr contains extra information -/
@[export pantograph_parse_elab_expr_m]
-def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Protocol.FallibleT Elab.TermElabM Expr := do
  let env ← MonadEnv.getEnv
-  let expectedType? ← match ← expectedType?.mapM parseElabType with
-    | .none => pure $ .none
-    | .some (.ok t) => pure $ .some t
-    | .some (.error e) => return .error e
+  let expectedType? ← expectedType?.mapM parseElabType
  let syn ← match parseTerm env expr with
-    | .error str => return .error $ errorI "parsing" str
+    | .error str => Protocol.throw $ errorI "parsing" str
    | .ok syn => pure syn
  match ← elabTerm syn expectedType? with
-  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← instantiateMVars expr)
+  | .error str => Protocol.throw $ errorI "elab" str
+  | .ok expr => return (← instantiateMVars expr)

@[export pantograph_expr_echo_m]
 def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
-    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabExpr expr expectedType? with
-      | .error e => return .error e
+    Protocol.FallibleT CoreM Protocol.ExprEchoResult := do
+  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+    let expr ← match ← parseElabExpr expr expectedType? |>.run with
+      | .error e => return Except.error e
      | .ok expr => pure expr
    try
      let type ← unfoldAuxLemmas (← Meta.inferType expr)
-      return .ok {
+      return .ok $ .ok ({
          type := (← serializeExpression options type),
-          expr := (← serializeExpression options expr)
-      }
+          expr := (← serializeExpression options expr),
+      }: Protocol.ExprEchoResult)
    catch exception =>
-      return .error $ errorI "typing" (← exception.toMessageData.toString)
+      return Except.error $ errorI "typing" (← exception.toMessageData.toString)
+  liftExcept e

@[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
-  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabType expr with
+def goalStartExpr (expr: String) (levels: Array String): Protocol.FallibleT CoreM GoalState := do
+  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
+    let expr ← match ← parseElabType expr |>.run with
      | .error e => return .error e
      | .ok expr => pure $ expr
-    return .ok $ ← GoalState.create expr
+    return .ok $ .ok $ ← GoalState.create expr
+  liftExcept e

@[export pantograph_goal_resume]
 def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
@ -217,9 +209,9 @@ def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResul

 -- Cancel the token after a timeout.
@[export pantograph_run_cancel_token_with_timeout_m]
-def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : Std.Time.Millisecond.Offset) : IO Unit := do
+def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : UInt32) : IO Unit := do
  let _ ← EIO.asTask do
-    let () ← (← Std.Internal.IO.Async.sleep timeout).block
+    IO.sleep timeout
    cancelToken.set
  return ()

--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -30,6 +30,8 @@ structure Options where
  printImplementationDetailHyps: Bool := false
  -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
  automaticMode: Bool := true
+  -- Timeout for tactics and operations that could potentially execute a tactic
+  timeout: Nat := 0
  deriving Lean.ToJson

 abbrev OptionsT := ReaderT Options
@ -202,9 +204,10 @@ structure EnvInspectResult where

 structure EnvAdd where
  name: String
+  levels: Array String := #[]
  type: String
  value: String
-  isTheorem: Bool
+  isTheorem: Bool := false
  deriving Lean.FromJson
 structure EnvAddResult where
  deriving Lean.ToJson
@ -225,6 +228,7 @@ structure OptionsSet where
  printAuxDecls?: Option Bool := .none
  printImplementationDetailHyps?: Option Bool := .none
  automaticMode?: Option Bool := .none
+  timeout?: Option Nat := .none
  deriving Lean.FromJson
 structure OptionsSetResult where
  deriving Lean.ToJson
@ -386,6 +390,9 @@ structure FrontendProcessResult where
  units: List CompilationUnit
  deriving Lean.ToJson

-abbrev CR α := Except InteractionError α
+abbrev FallibleT := ExceptT InteractionError
+
+abbrev throw {m : Type v → Type w} [MonadExceptOf InteractionError m] {α : Type v} (e : InteractionError) : m α :=
+  throwThe InteractionError e

 end Pantograph.Protocol
--- a/Repl.lean
+++ b/Repl.lean
@ -20,9 +20,8 @@ structure State where

 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context $ StateRefT State IO
+abbrev EMainM := Protocol.FallibleT $ ReaderT Context $ StateRefT State IO
 def getMainState : MainM State := get
-/-- Fallible subroutine return type -/
-abbrev CR α := Except Protocol.InteractionError α

 instance : MonadEnv MainM where
  getEnv := return (← get).env
@ -37,24 +36,42 @@ def newGoalState (goalState: GoalState) : MainM Nat := do
  }
  return stateId

-def runCoreM { α } (coreM : CoreM α) : MainM α := do
+def runCoreM { α } (coreM : CoreM α) : EMainM α := do
  let scope := (← get).scope
+  let options :=(← get).options
+  let cancelTk? ← match options.timeout with
+    | 0 => pure .none
+    | _ => .some <$> IO.CancelToken.new
  let coreCtx : Core.Context := {
    (← read).coreContext with
    currNamespace      := scope.currNamespace
    openDecls          := scope.openDecls
    options            := scope.opts
+    cancelTk?,
  }
  let coreState : Core.State := {
    env := (← get).env
  }
-  let (result, state') ← coreM.toIO coreCtx coreState
-  modifyEnv λ _ => state'.env
-  return result
+  -- Remap the coreM to capture every exception
+  let coreM' : CoreM _ :=
+    Core.tryCatchRuntimeEx (Except.ok <$> coreM) λ ex => do
+      let desc ← ex.toMessageData.toString
+      return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+  let io := coreM'.toIO coreCtx coreState
+  if let .some token := cancelTk? then
+    runCancelTokenWithTimeout token (timeout := .mk options.timeout)
+  let (result, state') ← io
+  if result matches .ok _ then
+    modifyEnv λ _ => state'.env
+  liftExcept result

-def liftMetaM { α } (metaM : MetaM α): MainM α :=
+def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
+  liftExcept $ ← runCoreM coreM.run
+
+
+def liftMetaM { α } (metaM : MetaM α): EMainM α :=
  runCoreM metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) : MainM α :=
+def liftTermElabM { α } (termElabM: Elab.TermElabM α) : EMainM α :=
  runCoreM $ termElabM.run' (ctx := defaultElabContext) |>.run'

 section Frontend
@ -68,7 +85,7 @@ structure CompilationUnit where
  messages : Array String
  newConstants : List Name

-def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
+def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
  let options := (← getMainState).options
  let (fileName, file) ← match args.fileName?, args.file? with
    | .some fileName, .none => do
@ -76,7 +93,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
      pure (fileName, file)
    | .none, .some file =>
      pure ("<anonymous>", file)
-    | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+    | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {fileName, file} must be supplied"
  let env?: Option Environment ← if args.readHeader then
      pure .none
    else do
@ -137,19 +154,23 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
      goalSrcBoundaries?,
      newConstants?,
    }
-  return .ok { units }
+  return { units }

 end Frontend

 /-- Main loop command of the REPL -/
 def execute (command: Protocol.Command): MainM Json := do
-  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → MainM (CR β)): MainM Json :=
-    match fromJson? command.payload with
-    | .ok args => do
-      match (← comm args) with
-      | .ok result =>  return toJson result
-      | .error ierror => return toJson ierror
-    | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
+  let run { α β: Type } [FromJson α] [ToJson β] (comm: α → EMainM β): MainM Json :=
+    try
+      match fromJson? command.payload with
+      | .ok args => do
+        match (← comm args |>.run) with
+        | .ok result =>  return toJson result
+        | .error ierror => return toJson ierror
+      | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
+    catch ex : IO.Error =>
+      let error : Protocol.InteractionError := { error := "io", desc := ex.toString }
+      return toJson error
  match command.cmd with
  | "reset"         => run reset
  | "stat"          => run stat
@ -180,40 +201,40 @@ def execute (command: Protocol.Command): MainM Json := do
  errorIndex := errorI "index"
  errorIO := errorI "io"
  -- Command Functions
-  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
+  reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
    let state ← getMainState
    let nGoals := state.goalStates.size
    set { state with nextId := 0, goalStates := .empty }
-    return .ok { nGoals }
-  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
+    return { nGoals }
+  stat (_: Protocol.Stat): EMainM Protocol.StatResult := do
    let state ← getMainState
    let nGoals := state.goalStates.size
-    return .ok { nGoals }
-  env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
+    return { nGoals }
+  env_describe (args: Protocol.EnvDescribe): EMainM Protocol.EnvDescribeResult := do
    let result ← runCoreM $ Environment.describe args
-    return .ok result
-  env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
+    return result
+  env_module_read (args: Protocol.EnvModuleRead): EMainM Protocol.EnvModuleReadResult := do
    runCoreM $ Environment.moduleRead args
-  env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
+  env_catalog (args: Protocol.EnvCatalog): EMainM Protocol.EnvCatalogResult := do
    let result ← runCoreM $ Environment.catalog args
-    return .ok result
-  env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
+    return result
+  env_inspect (args: Protocol.EnvInspect): EMainM Protocol.EnvInspectResult := do
    let state ← getMainState
-    runCoreM $ Environment.inspect args state.options
-  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
-    runCoreM $ Environment.addDecl args
-  env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
+    runCoreM' $ Environment.inspect args state.options
+  env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
+    runCoreM' $ Environment.addDecl args.name args.levels args.type args.value args.isTheorem
+  env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
    let env ← MonadEnv.getEnv
    environmentPickle env args.path
-    return .ok {}
-  env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
+    return {}
+  env_load (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
    let (env, _) ← environmentUnpickle args.path
    setEnv env
-    return .ok {}
-  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
+    return {}
+  expr_echo (args: Protocol.ExprEcho): EMainM Protocol.ExprEchoResult := do
    let state ← getMainState
-    runCoreM $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
-  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
+    runCoreM' $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
+  options_set (args: Protocol.OptionsSet): EMainM Protocol.OptionsSetResult := do
    let state ← getMainState
    let options := state.options
    set { state with
@ -227,14 +248,15 @@ def execute (command: Protocol.Command): MainM Json := do
        printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
        printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
        automaticMode := args.automaticMode?.getD options.automaticMode,
+        timeout := args.timeout?.getD options.timeout,
      }
    }
-    return .ok {  }
-  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
-    return .ok (← getMainState).options
-  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
+    return {  }
+  options_print (_: Protocol.OptionsPrint): EMainM Protocol.Options := do
+    return (← getMainState).options
+  goal_start (args: Protocol.GoalStart): EMainM Protocol.GoalStartResult := do
    let expr?: Except _ GoalState ← liftTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
+      | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) |>.run
      | .none, .some copyFrom => do
        (match (← getEnv).find? <| copyFrom.toName with
        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@ -242,16 +264,16 @@ def execute (command: Protocol.Command): MainM Json := do
      | _, _ =>
        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
    match expr? with
-    | .error error => return .error error
+    | .error error => Protocol.throw error
    | .ok goalState =>
      let stateId ← newGoalState goalState
-      return .ok { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
+      return { stateId, root := goalState.root.name.toString }
+  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.stateId]? |
-      return .error $ errorIndex s!"Invalid state index {args.stateId}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
    let .some goal := goalState.goals.get? args.goalId |
-      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
+      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
      -- NOTE: Should probably use a macro to handle this...
      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
@ -277,63 +299,63 @@ def execute (command: Protocol.Command): MainM Json := do
        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
        pure $ .error error
    match nextGoalState? with
-    | .error error => return .error error
+    | .error error => Protocol.throw 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"
+            Protocol.throw $ errorIO "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"
+            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            return .error $ errorIO "Resuming known goals"
+            Protocol.throw $ errorIO "Resuming known goals"
          pure result
        | false, _ => pure nextGoalState
      let nextStateId ← newGoalState nextGoalState
      let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
-      return .ok {
+      return {
        nextStateId? := .some nextStateId,
        goals? := .some goals,
      }
    | .ok (.parseError message) =>
-      return .ok { parseError? := .some message }
+      return { parseError? := .some message }
    | .ok (.invalidAction message) =>
-      return .error $ errorI "invalid" message
+      Protocol.throw $ errorI "invalid" message
    | .ok (.failure messages) =>
-      return .ok { tacticErrors? := .some messages }
-  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
+      return { tacticErrors? := .some messages }
+  goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
    let state ← getMainState
    let .some target := state.goalStates[args.target]? |
-      return .error $ errorIndex s!"Invalid state index {args.target}"
-    let nextState? ← match args.branch?, args.goals? with
+      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
+    let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
      | .some branchId, .none => do
        match state.goalStates[branchId]? with
-        | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
+        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
        | .some branch => pure $ target.continue branch
      | .none, .some goals =>
        pure $ goalResume target goals
-      | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
-    match nextState? with
-    | .error error => return .error <| errorI "structure" error
+      | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {branch, goals} must be supplied"
+    match nextGoalState? with
+    | .error error => Protocol.throw $ errorI "structure" error
    | .ok nextGoalState =>
      let nextStateId ← newGoalState nextGoalState
      let goals ← liftMetaM $ goalSerialize nextGoalState (options := state.options)
-      return .ok {
+      return {
        nextStateId,
        goals,
      }
-  goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
+  goal_delete (args: Protocol.GoalDelete): EMainM Protocol.GoalDeleteResult := do
    let state ← getMainState
    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
+    return {}
+  goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.stateId]? |
-      return .error $ errorIndex s!"Invalid state index {args.stateId}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
    let result ← liftMetaM <| goalPrint
        goalState
        (rootExpr := args.rootExpr?.getD False)
@ -341,21 +363,18 @@ def execute (command: Protocol.Command): MainM Json := do
        (goals := args.goals?.getD False)
        (extraMVars := args.extraMVars?.getD #[])
        (options := state.options)
-    return .ok result
-  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
+    return result
+  goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
    let state ← getMainState
    let .some goalState := state.goalStates[args.id]? |
-      return .error $ errorIndex s!"Invalid state index {args.id}"
+      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
    goalStatePickle goalState args.path
-    return .ok {}
-  goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do
+    return {}
+  goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
    let id ← newGoalState goalState
-    return .ok { id }
-  frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
-    try
-      frontend_process_inner args
-    catch e =>
-      return .error $ errorI "frontend" e.toString
+    return { id }
+  frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
+    frontend_process_inner args

 end Pantograph.Repl
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -103,14 +103,14 @@ def test_symbol_location : TestT IO Unit := do
    (opts := {})
    (trustLevel := 1)
  addTest $ ← runTestCoreM env do
-    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
+    let .ok result ← (Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {})).run | fail "Inspect failed"
    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"

    -- Extraction of source doesn't work for symbols in `Init` for some reason
    checkTrue "file" result.sourceUri?.isNone
    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
-    let .ok { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed"
+    let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
    checkTrue "constNames" $ constNames.contains "Nat.succ_add"

--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -91,6 +91,24 @@ def test_tactic : Test :=
     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
      Protocol.GoalTacticResult)
  ]
+example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
+  simp
+def test_tactic_timeout : Test :=
+  [
+    step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult),
+    -- timeout of 10 milliseconds
+    step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
+     ({ }: Protocol.OptionsSetResult),
+    step "goal.tactic" ({ stateId := 0, expr? := .some "by\nsleep 1000; simp" }: Protocol.GoalTactic)
+     ({ error := "io", desc := "internal exception #6" }: Protocol.InteractionError),
+    -- ensure graceful recovery
+    step "options.set" ({ timeout? := .some 0 } : Protocol.OptionsSet)
+     ({ }: Protocol.OptionsSetResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "simp" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := .some #[], }: Protocol.GoalTacticResult),
+  ]
+
 def test_automatic_mode (automatic: Bool): Test :=
  let varsPQ := #[
    { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
@ -280,6 +298,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
    ("options.set options.print", test_option_modify),
    ("Malformed command", test_malformed_command),
    ("Tactic", test_tactic),
+    ("Tactic Timeout", test_tactic_timeout),
    ("Manual Mode", test_automatic_mode false),
    ("Automatic Mode", test_automatic_mode true),
    ("env.add env.inspect", test_env_add_inspect),
--- a/doc/repl.md
+++ b/doc/repl.md
@ -22,6 +22,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  automatic mode (flag: `"automaticMode"`).  By default it is turned on, with
  all goals automatically resuming. This makes Pantograph act like a gym,
  with no resumption necessary to manage your goals.
+
+  Set `timeout` to a non-zero number to specify timeout (milliseconds) for all `CoreM`
+  operations.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
  Start a new proof from a given expression or symbol