Lean.Heartbeats

This provides some utilities is the first file in the Lean import hierarchy. It is responsible for setting up basic definitions, most of which Lean already has "built in knowledge" about, so it is important that they be set up in exactly this way. (For example, Lean will use PUnit in the desugaring of do notation, or in the pattern match compiler.)

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.