Catch runtime exceptions in trySimpOnly

Verbose/English/Calc.lean

@@ -333,6 +333,10 @@ example (x : ℝ) (p : ℕ) (h : x ≤ p) : x < (p + 1 : ℕ) := by
   Calc x ≤ p by assumption
     _ < p + 1 by computation
 
+-- Regression test for bug where simp reached max recursion depth
+example (a b : ℝ) (h : a = a*b) : a - a* b = 0 := by
+  Calc a - a*b = 0 since a = a*b
+
 example (u : Nat → Nat) (h : ∀ n, u n = u 0)
   : ∀ n, ∀ m, u m = u n := by
   intro m n

Verbose/English/Since.lean

@@ -399,3 +399,7 @@ example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : True := by
 
 example (a b : ℝ) (h : a ≥ b) (h' : b > 0) : |a| = a := by
   Since a ≥ b and b > 0 we get that a > 0 finally we conclude that |a| = a
+
+-- Regression tests for simpa exceeding heartbeats bug
+example (a b c : ℝ) (h : a = b) (h' : b = b * c) : b - a = b - b * c := by
+  Since a = b and b = b * c we conclude that b - a = b - b * c

Verbose/Tactics/Since.lean

@@ -314,40 +314,39 @@ def trySimpa (g : MVarId) (a b : Term) : TacticM Bool := g.withContext do
   let goals ← getGoals
   let state ← saveState
   setGoals [g]
-  try
+  -- Catching runtime exceptions, because heartbeat exceeded causes a runtime exception
+  tryCatchRuntimeEx (do
     evalTactic (← `(tactic| focus simpa only [$a:term] using $b:term))
     setGoals goals
     trace[Verbose] s!"simpa succeeded"
-    return true
-  catch
-  | e =>
-    trace[Verbose] e.toMessageData
-    state.restore
-    setGoals [g]
-    try
-      evalTactic (← `(tactic| focus simpa only [$b:term] using $a:term))
-      trace[Verbose] s!"simpa succeeded"
-      setGoals goals
-      return true
-    catch
-      | _ =>
-        trace[Verbose] e.toMessageData
-        state.restore
-        return false
+    return true)
+    (fun e => do
+      trace[Verbose] e.toMessageData
+      state.restore
+      setGoals [g]
+      tryCatchRuntimeEx (do
+        evalTactic (← `(tactic| focus simpa only [$b:term] using $a:term))
+        trace[Verbose] s!"simpa succeeded"
+        setGoals goals
+        return true)
+        (fun _ => do
+          trace[Verbose] e.toMessageData
+          state.restore
+          return false))
 
 def trySimpOnly (g : MVarId) (hyp : Term) : TacticM Bool := g.withContext do
   let goals ← getGoals
   let state ← saveState
   setGoals [g]
-  try
+  -- Catching runtime exceptions, because heartbeat exceeded causes a runtime exception
+  tryCatchRuntimeEx (do
     evalTactic (← `(tactic| focus ((simp only [$hyp:term]; try apply le_rfl); done)))
     setGoals goals
-    return true
-  catch
-  | e =>
+    return true)
+   (fun e => do
     trace[Verbose] e.toMessageData
     state.restore
-    return false
+    return false)
 
 def tryFieldSimpOnly (g : MVarId) (hyp : Term) : TacticM Bool := g.withContext do
   let goals ← getGoals