The Lean Language Reference

15.8. Timing🔗

🔗def
IO.sleep (ms : UInt32) : BaseIO Unit

Pauses execution for the specified number of milliseconds.

🔗opaque
IO.monoNanosNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in nanoseconds. There is no relation to wall clock time.

🔗opaque
IO.monoMsNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in milliseconds. There is no relation to wall clock time.

🔗opaque
IO.getNumHeartbeats : BaseIO Nat

Returns the number of heartbeats that have occurred during the current thread's execution. The heartbeat count is the number of “small” memory allocations performed in a thread.

Heartbeats used to implement timeouts that are more deterministic across different hardware.

🔗def
IO.addHeartbeats (count : Nat) : BaseIO Unit

Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give allocation-avoiding code additional “weight” and is also used to adjust the counter after resuming from a snapshot.

Heartbeats are a means of implementing “deterministic” timeouts. The heartbeat counter is the number of “small” memory allocations performed on the current execution thread.