Additional functions using CoreM state.

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

Count 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 getMaxHeartbeats : Lean.CoreM Nat

Return the current maxHeartbeats.

Equations

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

def getInitHeartbeats : Lean.CoreM Nat

Return the current initHeartbeats.

Equations

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

def getRemainingHeartbeats : Lean.CoreM Nat

Return the remaining heartbeats available in this computation.

Equations

• getRemainingHeartbeats = do let __do_lift ← getMaxHeartbeats let __do_lift_1 ← liftM IO.getNumHeartbeats let __do_lift_2 ← getInitHeartbeats pure (__do_lift - (__do_lift_1 - __do_lift_2))

def heartbeatsPercent : Lean.CoreM Nat

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

Equations

• heartbeatsPercent = do let __do_lift ← liftM IO.getNumHeartbeats let __do_lift_1 ← getInitHeartbeats let __do_lift_2 ← getMaxHeartbeats pure ((__do_lift - __do_lift_1) * 100 / __do_lift_2)

def reportOutOfHeartbeats (tac : Lean.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.