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.

source
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.

Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
def Mathlib.CountHeartbeats.«tactic#count_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.

Instances For

source
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.

Equations

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

Instances For

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

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

Equations

- Mathlib.CountHeartbeats.roundDownIf n approx = if approx = true then toString "approximately " ++ toString (n / 1000 * 1000) else toString n

Instances For

source
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_heartbeats 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 the internal heartbeat counter accessible via `IO.getNumHeartbeats` has granularity 1000 times finer than 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`.

Equations

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

Instances For

source
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`.

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
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%`.

Equations

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

Instances For

# The "countHeartbeats" linter #

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

source
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.

source
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.

source
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.

Equations

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

Instances For

source
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.

Equations

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

Instances For