Debugging helper functions

@[never_extract, extern lean_dbg_trace]

def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α

Equations

• dbgTrace s f = f ()

def dbgTraceVal {α : Type u} [ToString α] (a : α) : α

Equations

• dbgTraceVal a = dbgTrace (toString a) fun (x : Unit) => a

@[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

• dbgTraceIfShared s a = a

@[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

• dbgStackTrace f = f ()

@[extern lean_dbg_sleep]

def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α

Equations

• dbgSleep ms f = f ()

@[never_extract, inline]

def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line : Nat) (col : Nat) (msg : String) : α

Equations

• panicWithPos modName line col msg = panic (mkPanicMessage modName line col msg)

@[never_extract, inline]

def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line : Nat) (col : Nat) (msg : String) : α

Equations

• panicWithPosWithDecl modName declName line col msg = panic (mkPanicMessageWithDecl modName declName line col msg)

@[extern lean_ptr_addr]

unsafe opaque ptrAddrUnsafe {α : Type u} (a : α) : USize

@[extern lean_is_exclusive_obj]

unsafe opaque isExclusiveUnsafe {α : Type u} (a : α) : Bool

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₂) : β

@[inline]

unsafe def ptrEq {α : Type u_1} (a : α) (b : α) : Bool

unsafe def ptrEqList {α : Type u_1} (as : List α) (bs : List α) : Bool

@[inline]

unsafe def withPtrEqUnsafe {α : Type u} (a : α) (b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool

@[implemented_by withPtrEqUnsafe]

def withPtrEq {α : Type u} (a : α) (b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool

Equations

• withPtrEq a b k h = k ()

@[inline]

def withPtrEqDecEq {α : Type u} (a : α) (b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b)

withPtrEq for DecidableEq

Equations

• withPtrEqDecEq a b k = match h : withPtrEq a b (fun (x : Unit) => toBoolUsing (k ())) ⋯ with | true => isTrue ⋯ | false => isFalse ⋯

@[implemented_by withPtrAddrUnsafe]

def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ (u₁ u₂ : USize), k u₁ = k u₂) : β

Equations

• withPtrAddr a k h = k 0

@[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

• Runtime.markMultiThreaded a = a

@[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

• Runtime.markPersistent a = a