Documentation

Init.Util

Debugging helper functions #

@[never_extract, extern lean_dbg_trace]
def dbgTrace {α : Type u} (s : String) (f : Unitα) :
α
Equations
Instances For
    def dbgTraceVal {α : Type u} [ToString α] (a : α) :
    α
    Equations
    Instances For
      @[never_extract, extern lean_dbg_trace_if_shared]
      def dbgTraceIfShared {α : Type u} (s : String) (a : α) :
      α

      Display the given message if a is shared, that is, RC(a) > 1

      Equations
      Instances For
        @[never_extract, extern lean_dbg_stack_trace]
        def dbgStackTrace {α : Type u} (f : Unitα) :
        α

        Print stack trace to stderr before evaluating given closure. Currently supported on Linux only.

        Equations
        Instances For
          @[extern lean_dbg_sleep]
          def dbgSleep {α : Type u} (ms : UInt32) (f : Unitα) :
          α
          Equations
          Instances For
            @[never_extract, inline]
            def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line : Nat) (col : Nat) (msg : String) :
            α
            Equations
            Instances For
              @[never_extract, inline]
              def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) :
              α
              Equations
              Instances For
                @[extern lean_ptr_addr]
                unsafe opaque ptrAddrUnsafe {α : Type u} (a : α) :
                @[extern lean_is_exclusive_obj]
                unsafe opaque isExclusiveUnsafe {α : Type u} (a : α) :

                Returns true if a is an exclusive object. We say an object is exclusive if it is single-threaded and its reference counter is 1.

                @[inline]
                unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
                β
                Equations
                Instances For
                  @[inline]
                  unsafe def ptrEq {α : Type u_1} (a : α) (b : α) :
                  Equations
                  Instances For
                    unsafe def ptrEqList {α : Type u_1} (as : List α) (bs : List α) :
                    Equations
                    Instances For
                      @[inline]
                      unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
                      Equations
                      Instances For
                        @[implemented_by withPtrEqUnsafe]
                        def withPtrEq {α : Type u} (a : α) (b : α) (k : UnitBool) (h : a = bk () = true) :
                        Equations
                        Instances For
                          @[inline]
                          def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : UnitDecidable (a = b)) :
                          Decidable (a = b)

                          withPtrEq for DecidableEq

                          Equations
                          Instances For
                            @[implemented_by withPtrAddrUnsafe]
                            def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USizeβ) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) :
                            β
                            Equations
                            Instances For
                              @[extern lean_runtime_mark_multi_threaded]
                              def Runtime.markMultiThreaded {α : Sort u_1} (a : α) :
                              α

                              Marks given value and its object graph closure as multi-threaded if currently marked single-threaded. This will make reference counter updates atomic and thus more costly. It can still be useful to do eagerly when the value will be shared between threads later anyway and there is available time budget to mark it now.

                              Equations
                              Instances For
                                @[extern lean_runtime_mark_persistent]
                                def Runtime.markPersistent {α : Sort u_1} (a : α) :
                                α

                                Marks given value and its object graph closure as persistent. This will remove reference counter updates but prevent the closure from being deallocated until the end of the process! It can still be useful to do eagerly when the value will be marked persistent later anyway and there is available time budget to mark it now or it would be unnecessarily marked multi-threaded in between.

                                Equations
                                Instances For