fix(#count_heartbeats): add approximately flag to stabilise tests (#…

…21251)

Writing `#count_hearts approximately in cmd` will report the heartbeat count, rounded down to the nearest 1000.

This can be used by the `#count_heartbeats` command: writing `#count_heartbeats approximately` only reports heartbeat counts that are rounded down to the nearest 1000.

This functionality is mostly intended to stabilise tests, so that small variations in heartbeat counts will still pass the tests.

Reported on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/341532-lean4-dev/topic/mathlib.20test.20build.20fails.20.288.20instead.20of.207.20heartbeats.29)

Mathlib/Util/CountHeartbeats.lean

@@ -95,22 +95,30 @@ using the least number of the form `2^k * 200000` that suffices.
 Note that that internal heartbeat counter accessible via `IO.getNumHeartbeats`
 has granularity 1000 times finer that the limits set by `set_option maxHeartbeats`.
 As this is intended as a user command, we divide by 1000.
+
+The optional `approximately` keyword rounds down the heartbeats to the nearest thousand.
+This is helps make the tests more stable to small changes in heartbeats.
+To use this functionality, use `#count_heartbeats approximately in cmd`.
 -/
-elab "#count_heartbeats " "in" ppLine cmd:command : command => do
+elab "#count_heartbeats " approx:(&"approximately ")? "in" ppLine cmd:command : command => do
   let start ← IO.getNumHeartbeats
   try
     elabCommand (← `(command| set_option maxHeartbeats 0 in $cmd))
   finally
     let finish ← IO.getNumHeartbeats
     let elapsed := (finish - start) / 1000
+    let roundElapsed :=
+      if approx.isSome then s!"approximately {(elapsed / 1000) * 1000}" else s!"{elapsed}"
     let max := (← Command.liftCoreM getMaxHeartbeats) / 1000
     if elapsed < max then
-      logInfo m!"Used {elapsed} heartbeats, which is less than the current maximum of {max}."
+      logInfo
+        m!"Used {roundElapsed} heartbeats, which is less than the current maximum of {max}."
     else
       let mut max' := max
       while max' < elapsed do
         max' := 2 * max'
-      logInfo m!"Used {elapsed} heartbeats, which is greater than the current maximum of {max}."
+      logInfo
+        m!"Used {roundElapsed} heartbeats, which is greater than the current maximum of {max}."
       let m : TSyntax `num := quote max'
       Command.liftCoreM <| MetaM.run' do
         Lean.Meta.Tactic.TryThis.addSuggestion (← getRef)
@@ -210,6 +218,16 @@ register_option linter.countHeartbeats : Bool := {
   descr := "enable the countHeartbeats linter"
 }
 
+/--
+An option used by the `countHeartbeats` linter: if set to `true`, then the countHeartbeats linter
+rounds down to the nearest 1000 the heartbeat count.
+-/
+register_option linter.countHeartbeatsApprox : Bool := {
+  defValue := false
+  descr := "if set to `true`, then the countHeartbeats linter rounds down \
+            to the nearest 1000 the heartbeat count"
+}
+
 namespace CountHeartbeats
 
 @[inherit_doc Mathlib.Linter.linter.countHeartbeats]
@@ -221,7 +239,10 @@ def countHeartbeatsLinter : Linter where run := withSetOptionIn fun stx ↦ do
   let mut msgs := #[]
   if [``Lean.Parser.Command.declaration, `lemma].contains stx.getKind then
     let s ← get
-    elabCommand (← `(command| #count_heartbeats in $(⟨stx⟩)))
+    if Linter.getLinterValue linter.countHeartbeatsApprox (← getOptions) then
+      elabCommand (← `(command| #count_heartbeats approximately in $(⟨stx⟩)))
+    else
+      elabCommand (← `(command| #count_heartbeats in $(⟨stx⟩)))
     msgs := (← get).messages.unreported.toArray.filter (·.severity != .error)
     set s
   match stx.find? (·.isOfKind ``Parser.Command.declId) with
@@ -233,8 +254,15 @@ def countHeartbeatsLinter : Linter where run := withSetOptionIn fun stx ↦ do
 initialize addLinter countHeartbeatsLinter
 
 @[inherit_doc Mathlib.Linter.linter.countHeartbeats]
-macro "#count_heartbeats" : command =>
-  `(command| set_option linter.countHeartbeats true)
+macro "#count_heartbeats" approx:(&" approximately")? : command => do
+  let approx ←
+    if approx.isSome then
+      `(set_option linter.countHeartbeatsApprox true) else
+      `(set_option linter.countHeartbeatsApprox false)
+  return ⟨mkNullNode
+    #[← `(command| set_option linter.countHeartbeats true),
+      approx]⟩
+
 
 end CountHeartbeats
 

MathlibTest/CountHeartbeats.lean

@@ -1,4 +1,5 @@
-import Mathlib.Tactic.Ring
+import Mathlib.Util.CountHeartbeats
+import Mathlib.Util.SleepHeartbeats
 
 set_option linter.style.header false
 
@@ -26,25 +27,27 @@ example (a : Nat) : a = a := rfl
 
 section using_count_heartbeats
 
--- sets the `countHeartbeats` linter option to `true`
-#count_heartbeats
+-- sets the `countHeartbeats` both linter option and the `approximate` option to `true`
+#count_heartbeats approximately
 
 mutual -- mutual declarations get ignored
 theorem XY : True := trivial
 end
 
-/-- info: Used 4 heartbeats, which is less than the current maximum of 200000. -/
+/-- info: Used approximately 1000 heartbeats, which is less than the current maximum of 200000. -/
 #guard_msgs in
 -- we use two nested `set_option ... in` to test that the `heartBeats` linter enters both.
 set_option linter.unusedTactic false in
 set_option linter.unusedTactic false in
-example : True := trivial
+example : True := by
+  sleep_heartbeats 1000 -- on top of these heartbeats, a few more are used by the rest of the proof
+  trivial
 
-/-- info: Used 4 heartbeats, which is less than the current maximum of 200000. -/
+/-- info: Used approximately 0 heartbeats, which is less than the current maximum of 200000. -/
 #guard_msgs in
 example : True := trivial
 
-/-- info: 'YX' used 2 heartbeats, which is less than the current maximum of 200000. -/
+/-- info: 'YX' used approximately 0 heartbeats, which is less than the current maximum of 200000. -/
 #guard_msgs in
 set_option linter.unusedTactic false in
 set_option linter.unusedTactic false in
@@ -55,23 +58,26 @@ end using_count_heartbeats
 section using_linter_option
 
 set_option linter.countHeartbeats true
+set_option linter.countHeartbeatsApprox true
 
 mutual -- mutual declarations get ignored
 theorem XY' : True := trivial
 end
 
-/-- info: Used 4 heartbeats, which is less than the current maximum of 200000. -/
+/-- info: Used approximately 0 heartbeats, which is less than the current maximum of 200000. -/
 #guard_msgs in
 -- we use two nested `set_option ... in` to test that the `heartBeats` linter enters both.
 set_option linter.unusedTactic false in
 set_option linter.unusedTactic false in
 example : True := trivial
 
-/-- info: Used 4 heartbeats, which is less than the current maximum of 200000. -/
+/-- info: Used approximately 0 heartbeats, which is less than the current maximum of 200000. -/
 #guard_msgs in
 example : True := trivial
 
-/-- info: 'YX'' used 2 heartbeats, which is less than the current maximum of 200000. -/
+/--
+info: 'YX'' used approximately 0 heartbeats, which is less than the current maximum of 200000.
+-/
 #guard_msgs in
 set_option linter.unusedTactic false in
 set_option linter.unusedTactic false in