Defines a command wrapper that prints the number of heartbeats used in the enclosed command.

For example

#count_heartbeats in
theorem foo : 42 = 6 * 7 := rfl

will produce an info message containing a number around 51. If this number is above the current maxHeartbeats, we also print a Try this: suggestion.

def Mathlib.CountHeartbeats.runTacForHeartbeats (tac : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (revert : Bool := true) : Lean.Elab.Tactic.TacticM Nat

Run a tactic, optionally restoring the original state, and report just the number of heartbeats.

def Mathlib.CountHeartbeats.variation (counts : List Nat) : List Nat

Given a List Nat, return the minimum, maximum, and standard deviation.

def Mathlib.CountHeartbeats.logVariation {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (counts : List Nat) : m Unit

Given a List Nat, log an info message with the minimum, maximum, and standard deviation.

def Mathlib.CountHeartbeats.«tactic#count_heartbeats_» : Lean.ParserDescr

Count the heartbeats used by a tactic, e.g.: #count_heartbeats simp.

def Mathlib.CountHeartbeats.«tactic#count_heartbeats!_In__» : Lean.ParserDescr

#count_heartbeats! in tac runs a tactic 10 times, counting the heartbeats used, and logs the range and standard deviation. The tactic #count_heartbeats! n in tac runs it n times instead.

def Mathlib.CountHeartbeats.roundDownIf (n : Nat) (approx : Bool) : String

Round down the number n to the nearest thousand, if approx is true.

def Mathlib.CountHeartbeats.«command#count_heartbeatsApproximatelyIn__» : Lean.ParserDescr

#count_heartbeats in cmd counts the heartbeats used in the enclosed command cmd. Use #count_heartbeats to count the heartbeats in all the following declarations.

This is most useful for setting sufficient but reasonable limits via set_option maxHeartbeats for long running declarations.

If you do so, please resist the temptation to set the limit as low as possible. As the simp set and other features of the library evolve, other contributors will find that their (likely unrelated) changes have pushed the declaration over the limit. count_heartbearts in will automatically suggest a set_option maxHeartbeats via "Try this:" 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 helps make the tests more stable to small changes in heartbeats. To use this functionality, use #count_heartbeats approximately in cmd.

def Mathlib.CountHeartbeats.tacticCount_heartbeats : Lean.ParserDescr

count_heartbeats is deprecated in favour of #count_heartbeats since "2025-01-12"

def Mathlib.CountHeartbeats.commandCount_heartbeats : Lean.ParserDescr

count_heartbeats is deprecated in favour of #count_heartbeats since "2025-01-12"

def Mathlib.CountHeartbeats.commandGuard_min_heartbeatsApproximately_In__ : Lean.ParserDescr

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.

The optional approximately keyword rounds down the heartbeats to the nearest thousand. This helps make the tests more stable to small changes in heartbeats. To use this functionality, use guard_min_heartbeats approximately (n)? in cmd.

def Mathlib.CountHeartbeats.elabForHeartbeats (cmd : Lean.TSyntax `command) (revert : Bool := true) : Lean.Elab.Command.CommandElabM Nat

Run a command, optionally restoring the original state, and report just the number of heartbeats.

def Mathlib.CountHeartbeats.«command#count_heartbeats!_In__» : Lean.ParserDescr

#count_heartbeats! in cmd runs a command 10 times, reporting the range in heartbeats, and the standard deviation. The command #count_heartbeats! n in cmd runs it n times instead.

Example usage:

#count_heartbeats! in
def f := 37

displays the info message Min: 7 Max: 8 StdDev: 14%.

The "countHeartbeats" linter

The "countHeartbeats" linter counts the heartbeats of every declaration.

opaque Mathlib.Linter.linter.countHeartbeats : Lean.Option Bool

The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to #count_heartbeats in xxx, except that it applies to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations: it looks inside set_option ... in, but not, for instance, inside mutual blocks.

There is a convenience notation #count_heartbeats that simply sets the linter option to true.

opaque Mathlib.Linter.linter.countHeartbeatsApprox : Lean.Option Bool

An option used by the countHeartbeats linter: if set to true, then the countHeartbeats linter rounds down to the nearest 1000 the heartbeat count.

def Mathlib.Linter.CountHeartbeats.countHeartbeatsLinter : Lean.Linter

The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to #count_heartbeats in xxx, except that it applies to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations: it looks inside set_option ... in, but not, for instance, inside mutual blocks.

There is a convenience notation #count_heartbeats that simply sets the linter option to true.

def Mathlib.Linter.CountHeartbeats.«command#count_heartbeatsApproximately» : Lean.ParserDescr

The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to #count_heartbeats in xxx, except that it applies to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations: it looks inside set_option ... in, but not, for instance, inside mutual blocks.

There is a convenience notation #count_heartbeats that simply sets the linter option to true.