From 4eccb5b4792c270ad10ac059b9672a8845961079 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 May 2025 18:14:59 -0400 Subject: [PATCH] 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. --- src/Lean/Meta/Tactic/Grind/Combinators.lean | 28 --------------------- src/Lean/Meta/Tactic/Grind/EMatch.lean | 11 ++++---- src/Lean/Meta/Tactic/Grind/Intro.lean | 7 ++++-- src/Lean/Meta/Tactic/Grind/Lookahead.lean | 4 +-- src/Lean/Meta/Tactic/Grind/Solve.lean | 28 ++++++++++----------- tests/lean/run/grind_heartbeats.lean | 24 ++++++++++++++++++ 6 files changed, 51 insertions(+), 51 deletions(-) create mode 100644 tests/lean/run/grind_heartbeats.lean diff --git a/src/Lean/Meta/Tactic/Grind/Combinators.lean b/src/Lean/Meta/Tactic/Grind/Combinators.lean index cfeb0efb2a..bdc5adf8c0 100644 --- a/src/Lean/Meta/Tactic/Grind/Combinators.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index be83a4a3ee..57724eaaed 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Intro.lean b/src/Lean/Meta/Tactic/Grind/Intro.lean index c2f413e1b0..334d412f71 100644 --- a/src/Lean/Meta/Tactic/Grind/Intro.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Lookahead.lean b/src/Lean/Meta/Tactic/Grind/Lookahead.lean index e093e2afb8..7680835f9b 100644 --- a/src/Lean/Meta/Tactic/Grind/Lookahead.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Solve.lean b/src/Lean/Meta/Tactic/Grind/Solve.lean index e7057ae133..39c2fa5799 100644 --- a/src/Lean/Meta/Tactic/Grind/Solve.lean +++ b/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,11 +52,9 @@ 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 @@ -64,6 +62,8 @@ 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 diff --git a/tests/lean/run/grind_heartbeats.lean b/tests/lean/run/grind_heartbeats.lean new file mode 100644 index 0000000000..cd8ceca193 --- /dev/null +++ b/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 ` 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)