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 : optParam Bool true) : Lean.Elab.Tactic.TacticM Nat

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.CountHeartbeats.tacticCount_heartbeats_ : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.CountHeartbeats.tacticCount_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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.CountHeartbeats.commandCount_heartbeatsIn__ : Lean.ParserDescr

Count the heartbeats used in the enclosed command.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.CountHeartbeats.commandCount_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%.

Equations

• One or more equations did not get rendered due to their size.