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 : α) :
                @[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
                              @[inline]
                              def getElem! {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem cont idx elem dom] [Inhabited elem] (xs : cont) (i : idx) [Decidable (dom xs i)] :
                              elem
                              Equations
                              • xs[i]! = if h : dom xs i then xs[i] else outOfBounds
                              Instances For
                                @[inline]
                                def getElem? {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : contidxProp} [GetElem cont idx elem dom] (xs : cont) (i : idx) [Decidable (dom xs i)] :
                                Option elem
                                Equations
                                • xs[i]? = if h : dom xs i then some xs[i] else none
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    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