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.

Equations
    Instances For
      source
      def Lean.getMaxHeartbeats :
      CoreM Nat

      Returns the current maxHeartbeats.

      Equations
        Instances For
          source
          def Lean.getInitHeartbeats :
          CoreM Nat

          Returns the current initHeartbeats.

          Equations
            Instances For
              source
              def Lean.getRemainingHeartbeats :
              CoreM Nat

              Returns the remaining heartbeats available in this computation.

              Equations
                Instances For
                  source
                  def Lean.heartbeatsPercent :
                  CoreM Nat

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

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

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

                      Equations
                        Instances For