# Heartbeats #

Functions for interacting with the deterministic timeout heartbeat mechanism.

def
Lean.withHeartbeats
{m : Type → Type u_1}
{α : Type}
[Monad m]
[MonadLiftT BaseIO m]
(x : m α)
:

Counts the number of heartbeats used during a monadic function.

Remember that user facing heartbeats (e.g. as used in `set_option maxHeartbeats`

)
differ from the internally tracked heartbeats by a factor of 1000,
so you need to divide the results here by 1000 before comparing with user facing numbers.

## Equations

- Lean.withHeartbeats x = do let start ← liftM IO.getNumHeartbeats let r ← x let finish ← liftM IO.getNumHeartbeats pure (r, finish - start)

## Instances For

Returns the current `maxHeartbeats`

.

## Equations

- Lean.getMaxHeartbeats = do let __do_lift ← read pure __do_lift.maxHeartbeats

## Instances For

Returns the current `initHeartbeats`

.

## Equations

- Lean.getInitHeartbeats = do let __do_lift ← read pure __do_lift.initHeartbeats

## Instances For

Returns the remaining heartbeats available in this computation.

## Equations

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

## Instances For

Returns the percentage of the max heartbeats allowed that have been consumed so far in this computation.

## Equations

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

## Instances For

def
Lean.reportOutOfHeartbeats
(tac : Lake.Name)
(stx : Lean.Syntax)
(threshold : optParam Nat 90)
:

Log a message if it looks like we ran out of time.

## Equations

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