feat(Util/CountHeartbeats): Add guard_min_heartbeats command (#18392)

Mathlib/Util/CountHeartbeats.lean

@@ -117,6 +117,31 @@ elab "count_heartbeats " "in" ppLine cmd:command : command => do
         Lean.Meta.Tactic.TryThis.addSuggestion (← getRef)
           (← set_option hygiene false in `(command| set_option maxHeartbeats $m in $cmd))
 
+/--
+Guard the minimal number of heartbeats used in the enclosed command.
+
+This is most useful in the context of debugging and minimizing an example of a slow declaration.
+By guarding the number of heartbeats used in the slow declaration,
+an error message will be generated if a minimization step makes the slow behaviour go away.
+
+The default number of minimal heartbeats is the value of `maxHeartbeats` (typically 200000).
+Alternatively, you can specify a number of heartbeats to guard against,
+using the syntax `guard_min_heartbeats n in cmd`.
+-/
+elab "guard_min_heartbeats " n:(num)? "in" ppLine cmd:command : command => do
+  let max := (← Command.liftCoreM getMaxHeartbeats) / 1000
+  let n := match n with
+           | some j => j.getNat
+           | none => max
+  let start ← IO.getNumHeartbeats
+  try
+    elabCommand (← `(command| set_option maxHeartbeats 0 in $cmd))
+  finally
+    let finish ← IO.getNumHeartbeats
+    let elapsed := (finish - start) / 1000
+    if elapsed < n then
+      logInfo m!"Used {elapsed} heartbeats, which is less than the minimum of {n}."
+
 /--
 Run a command, optionally restoring the original state, and report just the number of heartbeats.
 -/

test/CountHeartbeats.lean

@@ -0,0 +1,21 @@
+import Mathlib.Tactic.Ring
+
+set_option linter.style.header false
+
+/-- info: Used 7 heartbeats, which is less than the current maximum of 200000. -/
+#guard_msgs in
+count_heartbeats in
+example (a : Nat) : a = a := rfl
+
+/-- info: Used 7 heartbeats, which is less than the minimum of 200000. -/
+#guard_msgs in
+guard_min_heartbeats in
+example (a : Nat) : a = a := rfl
+
+/-- info: Used 7 heartbeats, which is less than the minimum of 2000. -/
+#guard_msgs in
+guard_min_heartbeats 2000 in
+example (a : Nat) : a = a := rfl
+
+guard_min_heartbeats 1 in
+example (a : Nat) : a = a := rfl