feat: catch syntax errors

REPL/Main.lean

@@ -160,14 +160,16 @@ def runCommand (s : Command) : M m (CommandResponse ⊕ Error) := do
 /--
 Run a single tactic, returning the id of the new proof statement, and the new goals.
 -/
--- TODO return messages?
 -- TODO detect sorries?
-def runProofStep (s : ProofStep) : M m (ProofStepResponse ⊕ Error) := do
+def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do
   match (← get).proofStates[s.proofState]? with
   | none => return .inr ⟨"Unknown proof state."⟩
   | some proofState =>
-    let proofState' ← proofState.runString s.tactic
-    return .inl (← createProofStepReponse proofState' proofState)
+    try
+      let proofState' ← proofState.runString s.tactic
+      return .inl (← createProofStepReponse proofState' proofState)
+    catch ex =>
+      return .inr ⟨ex.toString⟩
 
 end REPL
 

test/invalid_tactic.expected.out

@@ -0,0 +1,20 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 43},
+   "goal": "x : Nat ⊢ x = x",
+   "endPos": {"line": 1, "column": 48}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 18},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofState": 1,
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "unknown identifier 'my_fake_premise'"}],
+ "goals": []}
+

test/invalid_tactic.in

@@ -0,0 +1,3 @@
+{"cmd": "theorem my_theorem (x : Nat) : x = x := by sorry"}
+
+{"tactic": "exact my_fake_premise", "proofState": 0}

test/unknown_tactic.expected.out

@@ -10,4 +10,5 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-uncaught exception: <input>:1:1: unknown tactic
+{"message": "<input>:1:1: unknown tactic"}
+