fix: grind diagnostics at maxHeartbeats (#8438)

This PR ensures that `grind` diagnostics are obtained even when
`maxHeartbeats` is reached.
This PR also removes some dead code.

Author: leodemoura

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

@@ -15,27 +15,6 @@ TODO: a proper tactic language for `grind`.
 
 def GrindTactic := Goal → GrindM (Option (List Goal))
 
-def GrindTactic.try (x : GrindTactic) : GrindTactic := fun g => do
-  let some gs ← x g | return some [g]
-  return some gs
-
-def applyToAll (x : GrindTactic)  (goals : List Goal) : GrindM (List Goal) := do
-  go goals []
-where
-  go (goals : List Goal) (acc : List Goal) : GrindM (List Goal) := do
-    match goals with
-    | [] => return acc.reverse
-    | goal :: goals => match (← x goal) with
-      | none => go goals (goal :: acc)
-      | some goals' => go goals (goals' ++ acc)
-
-partial def GrindTactic.andThen (x y : GrindTactic) : GrindTactic := fun goal => do
-  let some goals ← x goal | return none
-  applyToAll y goals
-
-instance : AndThen GrindTactic where
-  andThen a b := GrindTactic.andThen a (b ())
-
 partial def GrindTactic.iterate (x : GrindTactic) : GrindTactic := fun goal => do
   go [goal] []
 where
@@ -48,13 +27,6 @@ where
       else
         go todo (goal :: result)
 
-partial def GrindTactic.orElse (x y : GrindTactic) : GrindTactic := fun goal => do
-  let some goals ← x goal | y goal
-  return goals
-
-instance : OrElse GrindTactic where
-  orElse a b := GrindTactic.andThen a (b ())
-
 def toGrindTactic (f : GoalM Unit) : GrindTactic := fun goal => do
   let goal ← GoalM.run' goal f
   if goal.inconsistent then

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

@@ -474,7 +474,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-def ematch : GoalM Unit := do
+private def ematchCore : GoalM Unit := do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms
@@ -489,12 +489,13 @@ def ematch : GoalM Unit := do
       ematch.num       := s.ematch.num + 1
     }
 
-/-- Performs one round of E-matching, and assert new instances. -/
-def ematchAndAssert : GrindTactic := fun goal => do
+/-- Performs one round of E-matching. -/
+def ematch : GrindTactic := fun goal => do
   let numInstances := goal.ematch.numInstances
-  let goal ← GoalM.run' goal ematch
+  let goal ← GoalM.run' goal ematchCore
   if goal.ematch.numInstances == numInstances then
     return none
-  assertAll goal
+  else
+    return [goal]
 
 end Lean.Meta.Grind

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

@@ -263,7 +263,10 @@ def assertNext : GrindTactic := fun goal => do
   assertAt fact.proof fact.prop fact.generation { goal with newRawFacts }
 
 /-- Asserts all facts in the `goal` fact queue. -/
-partial def assertAll : GrindTactic :=
-  assertNext.iterate
+partial def assertAll : GrindTactic := fun goal =>
+  if goal.newRawFacts.isEmpty then
+    return none
+  else
+    assertNext.iterate goal
 
 end Lean.Meta.Grind

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

@@ -24,13 +24,13 @@ where
   loop (goal : Goal) : GrindM Bool := withIncRecDepth do
     if goal.inconsistent then
       return true
-    else if let some goals ← assertNext goal then
+    else if let some goals ← assertAll goal then
       cont goals
     else if let some goals ← Arith.check goal then
       cont goals
     else if let some goals ← splitNext goal then
       cont goals
-    else if let some goals ← ematchAndAssert goal then
+    else if let some goals ← ematch goal then
       cont goals
     else
       return false

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,18 +52,18 @@ def applyTac (x : GrindTactic) (goal : Goal) : M Bool := do
     return true
   stepGuard go goal
 
-def tryAssertNext : Goal → M Bool := applyTac assertNext
+def tryAssertAll : Goal → M Bool := applyTac assertAll
 
-def tryEmatch : Goal → M Bool := applyTac ematchAndAssert
-
-def trySplit : Goal → M Bool := applyTac splitNext
+def tryEmatch : Goal → M Bool := applyTac ematch
 
 def tryArith : Goal → M Bool := applyTac Arith.check
 
 def tryLookahead : Goal → M Bool := applyTac lookahead
 
 def tryMBTC : Goal → M Bool := applyTac Arith.Cutsat.mbtcTac
 
+def trySplit : Goal → M Bool := applyTac splitNext
+
 partial def main (fallback : Fallback) : M Unit := do
   repeat do
     if (← get).failure?.isSome then
@@ -72,7 +72,7 @@ partial def main (fallback : Fallback) : M Unit := do
       return ()
     if goal.inconsistent then
       continue
-    if (← tryAssertNext goal) then
+    if (← tryAssertAll goal) then
       continue
     if (← tryArith goal) then
       continue

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)