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 α) : m (α × Nat)

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)

def Lean.getMaxHeartbeats : Lean.CoreM Nat

Returns the current maxHeartbeats.

Equations

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

def Lean.getInitHeartbeats : Lean.CoreM Nat

Returns the current initHeartbeats.

Equations

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

def Lean.getRemainingHeartbeats : Lean.CoreM Nat

Returns the remaining heartbeats available in this computation.

Equations

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

def Lean.heartbeatsPercent : Lean.CoreM Nat

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.

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

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.