more robust error handling

leanprover-community · Oct 25, 2023 · 474db93 · 474db93
1 parent 3d336e8
commit 474db93
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 12 deletions.
diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -161,7 +161,7 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO ProofStepResponse := d
 /--
 Run a command, returning the id of the new environment, and any messages and sorries.
 -/
-def runCommand (s : Command) : M m (CommandResponse ⊕ Error) := do
+def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let (cmdSnapshot?, notFound) ← do match s.env with
   | none => pure (none, false)
   | some i => do match (← get).cmdStates[i]? with
@@ -170,7 +170,10 @@ def runCommand (s : Command) : M m (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let cmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (cmdState, messages, trees) ← IO.processInput s.cmd cmdState?
+  let (cmdState, messages, trees) ← try
+    IO.processInput s.cmd cmdState?
+  catch ex =>
+    return .inr ⟨ex.toString⟩
   let messages ← messages.mapM fun m => Message.of m
   let sorries ← sorries trees
   let tactics ← match s.allTactics with

diff --git a/test/Mathlib/ReplMathlibTests/20231025.lean b/test/Mathlib/ReplMathlibTests/20231025.lean