Documentation

Lean.Util.Heartbeats

Heartbeats #

Functions for interacting with the deterministic timeout heartbeat mechanism.

source
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.

Instances For
    source
    def Lean.getMaxHeartbeats :
    Lean.CoreM Nat

    Returns the current maxHeartbeats.

    Instances For
      source
      def Lean.getInitHeartbeats :
      Lean.CoreM Nat

      Returns the current initHeartbeats.

      Equations
      Instances For
        source
        def Lean.getRemainingHeartbeats :
        Lean.CoreM Nat

        Returns the remaining heartbeats available in this computation.

        Instances For
          source
          def Lean.heartbeatsPercent :
          Lean.CoreM Nat

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

          Instances For
            source
            def Lean.reportOutOfHeartbeats (tac : Lean.Name) (stx : Lean.Syntax) (threshold : Nat := 90) :
            Lean.CoreM Unit

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

            Instances For