Documentation

Std.Lean.CoreM

Additional functions using CoreM state. #

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

Instances For
    source
    def getMaxHeartbeats :
    Lean.CoreM Nat

    Return the current maxHeartbeats.

    Instances For
      source
      def getInitHeartbeats :
      Lean.CoreM Nat

      Return the current initHeartbeats.

      Instances For
        source
        def getRemainingHeartbeats :
        Lean.CoreM Nat

        Return the remaining heartbeats available in this computation.

        Instances For
          source
          def heartbeatsPercent :
          Lean.CoreM Nat

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

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

            Instances For