chore: remove Grind.Config.failures options (#8423)

Option is not very useful.

Author: leodemoura

src/Init/Grind/Tactics.lean

@@ -67,8 +67,6 @@ structure Config where
   if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
   -/
   splitImp : Bool := false
-  /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/
-  failures : Nat := 1
   /-- Maximum number of heartbeats (in thousands) the canonicalizer can spend per definitional equality test. -/
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems that have been marked with `[grind ext]`. -/

src/Lean/Elab/Tactic/Grind.lean

@@ -141,7 +141,7 @@ def grind
     let type ← mvarId.getType
     let mvar' ← mkFreshExprSyntheticOpaqueMVar type
     let result ← Grind.main mvar'.mvarId! params fallback
-    if result.hasFailures then
+    if result.hasFailed then
       throwError "`grind` failed\n{← result.toMessageData}"
     -- `grind` proofs are often big
     let e ← if (← isProp type) then

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

@@ -105,7 +105,7 @@ private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) :=
   return goals.filter fun goal => !goal.inconsistent
 
 structure Result where
-  failures : List Goal
+  failure? : Option Goal
   skipped  : List Goal
   issues   : List MessageData
   config   : Grind.Config
@@ -140,11 +140,11 @@ private def mkGlobalDiag (cs : Counters) (simp : Simp.Stats) : MetaM (Option Mes
   else
     return some <| .trace { cls := `grind } "Diagnostics" msgs
 
-def Result.hasFailures (r : Result) : Bool :=
-  !r.failures.isEmpty
+def Result.hasFailed (r : Result) : Bool :=
+  r.failure?.isSome
 
 def Result.toMessageData (result : Result) : MetaM MessageData := do
-  let mut msgs ← result.failures.mapM (goalToMessageData · result.config)
+  let mut msgs ← result.failure?.toList.mapM (goalToMessageData · result.config)
   if result.config.verbose then
     let mut issues := result.issues
     -- We did not find the following very useful in practice.
@@ -163,23 +163,23 @@ def main (mvarId : MVarId) (params : Params) (fallback : Fallback) : MetaM Resul
   if debug.terminalTacticsAsSorry.get (← getOptions) then
     mvarId.admit
     return {
-        failures := [], skipped := [], issues := [], config := params.config, trace := {}, counters := {}, simp := {}
+        failure? := none, skipped := [], issues := [], config := params.config, trace := {}, counters := {}, simp := {}
     }
   else
     let go : GrindM Result := withReducible do
       let goals ← initCore mvarId params
-      let (failures, skipped) ← solve goals fallback
+      let (failure?, skipped) ← solve goals fallback
       trace[grind.debug.final] "{← ppGoals goals}"
       let issues   := (← get).issues
       let trace    := (← get).trace
       let counters := (← get).counters
       let simp     := (← get).simpStats
-      if failures.isEmpty then
+      if failure?.isNone then
         -- If there are no failures and diagnostics are enabled, we still report the performance counters.
         if (← isDiagnosticsEnabled) then
           if let some msg ← mkGlobalDiag counters simp then
             logInfo msg
-      return { failures, skipped, issues, config := params.config, trace, counters, simp }
+      return { failure?, skipped, issues, config := params.config, trace, counters, simp }
     go.run params fallback
 
 end Lean.Meta.Grind

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

@@ -16,8 +16,7 @@ namespace Solve
 
 structure State where
   todo     : List Goal
-  failures : List Goal := []
-  stop     : Bool := false
+  failure? : Option Goal := none
 
 private abbrev M := StateRefT State GrindM
 
@@ -32,18 +31,16 @@ def pushGoal (goal : Goal) : M Unit :=
 def pushGoals (goals : List Goal) : M Unit :=
   modify fun s => { s with todo := goals ++ s.todo }
 
-def pushFailure (goal : Goal) : M Unit := do
-  modify fun s => { s with failures := goal :: s.failures }
-  if (← get).failures.length ≥ (← getConfig).failures then
-    modify fun s => { s with stop := true }
+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
-      pushFailure goal
+      setFailure goal
       return true
     else
       throw ex
@@ -67,12 +64,9 @@ def tryLookahead : Goal → M Bool := applyTac lookahead
 
 def tryMBTC : Goal → M Bool := applyTac Arith.Cutsat.mbtcTac
 
-def maxNumFailuresReached : M Bool := do
-  return (← get).failures.length ≥ (← getConfig).failures
-
 partial def main (fallback : Fallback) : M Unit := do
   repeat do
-    if (← get).stop then
+    if (← get).failure?.isSome then
       return ()
     let some goal ← getNext? |
       return ()
@@ -93,15 +87,15 @@ partial def main (fallback : Fallback) : M Unit := do
     let goal ← GoalM.run' goal fallback
     if goal.inconsistent || (← goal.mvarId.isAssigned) then
       continue
-    pushFailure goal
+    setFailure goal
 
 end Solve
 
 /--
 Try to solve/close the given goals, and returns the ones that could not be solved.
 -/
-def solve (goals : List Goal) (fallback : Fallback) : GrindM (List Goal × List Goal) := do
+def solve (goals : List Goal) (fallback : Fallback) : GrindM (Option Goal × List Goal) := do
   let (_, s) ← Solve.main fallback |>.run { todo := goals }
-  return (s.failures.reverse, s.todo)
+  return (s.failure?, s.todo)
 
 end Lean.Meta.Grind