From be505b80504b34f1298c734a97ecfc3af2d06a68 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 28 Mar 2025 19:06:43 -0700
Subject: [PATCH 1/3] feat: Run cancel token with timeout
---
Pantograph/Library.lean | 11 +++++++++++
1 file changed, 11 insertions(+)
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index b060275..aa7c42d 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -3,7 +3,10 @@ import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.Delate
import Pantograph.Version
+
import Lean
+import Std.Time
+import Std.Internal.Async
namespace Lean
@@ -212,4 +215,12 @@ def goalConvExit (state: GoalState): CoreM TacticResult :=
def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
runTermElabM <| state.tryCalc goal pred
+-- 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
+ let _ ← EIO.asTask do
+ let () ← (← Std.Internal.IO.Async.sleep timeout).block
+ cancelToken.set
+ return ()
+
end Pantograph
From 4610348fed595b6f4d04a5260c622de45091d647 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 28 Mar 2025 20:42:10 -0700
Subject: [PATCH 2/3] feat: `CoreM` timeout
---
Pantograph/Environment.lean | 51 ++++++-----
Pantograph/Library.lean | 58 +++++-------
Pantograph/Protocol.lean | 11 ++-
Repl.lean | 177 ++++++++++++++++++++----------------
Test/Environment.lean | 4 +-
Test/Integration.lean | 19 ++++
doc/repl.md | 3 +
7 files changed, 186 insertions(+), 137 deletions(-)
diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index 8e552a3..e18da61 100644
--- 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
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index aa7c42d..3c147b0 100644
--- 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 ()
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 0742986..41a6ccd 100644
--- 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
diff --git a/Repl.lean b/Repl.lean
index 310b9bf..0518296 100644
--- 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
diff --git a/Test/Environment.lean b/Test/Environment.lean
index e954bc3..be4bd0a 100644
--- 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"
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9263fbe..2c59e3b 100644
--- 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),
diff --git a/doc/repl.md b/doc/repl.md
index 93eb6ab..b0fe972 100644
--- 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
From 0528a1592ec8541025687383910869bf6de6356f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 28 Mar 2025 21:31:30 -0700
Subject: [PATCH 3/3] fix: Print internal exceptions nicely
---
Repl.lean | 13 +++++++++----
Test/Integration.lean | 2 +-
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/Repl.lean b/Repl.lean
index 0518296..3c87429 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -18,8 +18,9 @@ structure State where
-- Parser state
scope : Elab.Command.Scope := { header := "" }
-/-- Main state monad for executing commands -/
+/-- Main monad for executing commands -/
abbrev MainM := ReaderT Context $ StateRefT State IO
+/-- Main with possible exception -/
abbrev EMainM := Protocol.FallibleT $ ReaderT Context $ StateRefT State IO
def getMainState : MainM State := get
@@ -54,13 +55,17 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
}
-- Remap the coreM to capture every exception
let coreM' : CoreM _ :=
- Core.tryCatchRuntimeEx (Except.ok <$> coreM) λ ex => do
+ try
+ Except.ok <$> coreM
+ catch ex =>
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
+ let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
+ | Except.error (Exception.error _ msg) => Protocol.throw $ { error := "core", desc := ← msg.toString }
+ | Except.error (Exception.internal id _) => Protocol.throw $ { error := "internal", desc := (← id.getName).toString }
+ | Except.ok a => pure a
if result matches .ok _ then
modifyEnv λ _ => state'.env
liftExcept result
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 2c59e3b..013554b 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -101,7 +101,7 @@ def test_tactic_timeout : Test :=
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),
+ ({ error := "internal", desc := "interrupt" }: Protocol.InteractionError),
-- ensure graceful recovery
step "options.set" ({ timeout? := .some 0 } : Protocol.OptionsSet)
({ }: Protocol.OptionsSetResult),