feat: ensure we see grind diagnostics at maxHeartbeats

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Solve.lean

@@ -35,15 +35,15 @@ def setFailure (goal : Goal) : M Unit := do
   modify fun s => { s with failure? := some goal }
 
 @[inline] def stepGuard (x : Goal → M Bool) (goal : Goal) : M Bool := do
-  try
-    x goal
-  catch ex =>
-    if ex.isMaxHeartbeat || ex.isMaxRecDepth then
-      reportIssue! ex.toMessageData
-      setFailure goal
-      return true
-    else
-      throw ex
+  tryCatchRuntimeEx
+    (x goal)
+    fun ex => do
+      if ex.isMaxHeartbeat || ex.isMaxRecDepth then
+        reportIssue! ex.toMessageData
+        setFailure goal
+        return true
+      else
+        throw ex
 
 def applyTac (x : GrindTactic) (goal : Goal) : M Bool := do
   let go (goal : Goal) : M Bool := do
@@ -52,22 +52,16 @@ def applyTac (x : GrindTactic) (goal : Goal) : M Bool := do
     return true
   stepGuard go goal
 
--- TODO: it should be assertAll. It may produce multiple goals because of eager splitting.
 def tryAssertAll : Goal → M Bool := applyTac assertAll
 
--- TODO: it doesn't need to invoke assertAll
 def tryEmatch : Goal → M Bool := applyTac ematch
 
--- Can only fail or produce a new updated goal
 def tryArith : Goal → M Bool := applyTac Arith.check
 
--- Can only fail or produce a new updated goal
 def tryLookahead : Goal → M Bool := applyTac lookahead
 
--- Can only fail or produce a new updated goal
 def tryMBTC : Goal → M Bool := applyTac Arith.Cutsat.mbtcTac
 
--- May fail or produce multiple new goals
 def trySplit : Goal → M Bool := applyTac splitNext
 
 partial def main (fallback : Fallback) : M Unit := do

tests/lean/run/grind_heartbeats.lean

@@ -0,0 +1,24 @@
+set_option grind.warning false
+
+opaque f : Nat → Nat
+opaque op : Nat → Nat → Nat
+@[grind] theorem op_comm : op x y = op y x := sorry
+@[grind] theorem op_assoc : op (op x y) z = op x (op y z) := sorry
+
+syntax "gen! " num : term
+
+macro_rules
+  | `(gen! 0) => `(f 0)
+  | `(gen! $n:num) => `(op (f $n) (gen! $(Lean.quote (n.getNat - 1))))
+
+/--
+trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
+    Use `set_option maxHeartbeats <num>` to set the limit.
+    ⏎
+    Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs (trace, drop error) in
+set_option trace.grind.issues true in
+set_option maxHeartbeats 5000 in
+example : gen! 10 = 0 ∧ True := by
+  grind (instances := 10000)