opaque Lean.profiler : Lean.Option Bool

opaque Lean.profiler.threshold : Lean.Option Nat

@[export lean_get_profiler_threshold]

def Lean.profiler.threshold.getSecs (o : Options) : Float

@[extern lean_profileit]

def Lean.profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) (decl : Name := Name.anonymous) : α

Print and accumulate run time of act when option profiler is set to true.

unsafe def Lean.profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) (decl : Name := Name.anonymous) : EIO ε α

@[implemented_by Lean.profileitIOUnsafe]

def Lean.profileitIO {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) (decl : Name := Name.anonymous) : EIO ε α

def Lean.profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (act : m α) (decl : Name := Name.anonymous) : m α

@[extern lean_display_cumulative_profiling_times]

opaque Lean.displayCumulativeProfilingTimes : BaseIO Unit

Print all profiling times (if any) to standard error.