From 05b5d113b350bc7daec58a22694e85f2528fec48 Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 30 Jan 2025 23:30:56 +0000 Subject: [PATCH] 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 | 40 ++++++++++++++++++++++++++----- MathlibTest/CountHeartbeats.lean | 26 ++++++++++++-------- 2 files changed, 50 insertions(+), 16 deletions(-) diff --git a/Mathlib/Util/CountHeartbeats.lean b/Mathlib/Util/CountHeartbeats.lean index 209f07273d42b..c2cae69c01c47 100644 --- a/Mathlib/Util/CountHeartbeats.lean +++ b/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 diff --git a/MathlibTest/CountHeartbeats.lean b/MathlibTest/CountHeartbeats.lean index d476ef76e955a..07fdf8f2515dc 100644 --- a/MathlibTest/CountHeartbeats.lean +++ b/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