Trace messages

Trace messages explain to the user what problem Lean solved and what steps it took. Think of trace messages like a figure in a paper.

They are shown in the editor as a collapsible tree, usually as [class.name] message ▸. Every trace node has a class name, a message, and an array of children. This module provides the API to produce trace messages, the key entry points are:

• registerTraceClass `class.name registers a trace class
• ``withTraceNode class.name (fun result => return msg) do body produces a trace message containing the trace messages in `body` as children
• trace[class.name] msg produces a trace message without children

Users can enable trace options for a class using set_option trace.class.name true. This only enables trace messages for the class.name trace class as well as child classes that are explicitly marked as inherited (see registerTraceClass).

Internally, trace messages are stored as MessageData: .trace cls msg #[.trace .., .trace ..]

When writing trace messages, try to follow these guidelines:

1. Expansion progressively increases detail. Each level of expansion (of the trace node in the editor) should reveal more details. For example, the unexpanded node should show the top-level goal. Expanding it should show a list of steps. Expanding one of the steps then shows what happens during that step.
2. One trace message per step. The [trace.class] marker functions as a visual bullet point, making it easy to identify the different steps at a glance.
3. Outcome first. The top-level trace message should already show whether the action failed or succeeded, as opposed to a "success" trace message that comes pages later.
4. Be concise. Keep messages short. Avoid repetitive text. (This is also why the editor plugins abbreviate the common prefixes.)
5. Emoji are concisest. Several helper functions in this module help with a consistent emoji language.
6. Good defaults. Setting set_option trace.Meta.synthInstance true (etc.) should produce great trace messages out-of-the-box, without needing extra options to tweak it.

structure Lean.TraceElem : Type

• ref : Lean.Syntax
• msg : Lean.MessageData

instance Lean.instInhabitedTraceElem : Inhabited Lean.TraceElem

Equations

• Lean.instInhabitedTraceElem = { default := { ref := default, msg := default } }

structure Lean.TraceState : Type

• traces : Lean.PersistentArray Lean.TraceElem

instance Lean.instInhabitedTraceState : Inhabited Lean.TraceState

Equations

• Lean.instInhabitedTraceState = { default := { traces := default } }

opaque Lean.inheritedTraceOptions : IO.Ref (Lean.HashSet Lake.Name)

class Lean.MonadTrace (m : Type → Type) : Type

• modifyTraceState : (Lean.TraceState → Lean.TraceState) → m Unit
• getTraceState : m Lean.TraceState

instance Lean.instMonadTrace (m : Type → Type) (n : Type → Type) [MonadLift m n] [Lean.MonadTrace m] : Lean.MonadTrace n

Equations

• Lean.instMonadTrace m n = { modifyTraceState := fun (f : Lean.TraceState → Lean.TraceState) => liftM (Lean.modifyTraceState f), getTraceState := liftM Lean.getTraceState }

def Lean.printTraces {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.resetTraceState {m : Type → Type} [Lean.MonadTrace m] : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.isTracingEnabledFor {m : Type → Type} [Monad m] [Lean.MonadOptions m] [MonadLiftT IO m] (cls : Lake.Name) : m Bool

Equations

• Lean.isTracingEnabledFor cls = do let inherited ← liftM (ST.Ref.get Lean.inheritedTraceOptions) let __do_lift ← Lean.getOptions pure (Lean.checkTraceOption inherited __do_lift cls)

@[inline]

def Lean.getTraces {m : Type → Type} [Monad m] [Lean.MonadTrace m] : m (Lean.PersistentArray Lean.TraceElem)

Equations

• Lean.getTraces = do let s ← Lean.getTraceState pure s.traces

@[inline]

def Lean.modifyTraces {m : Type → Type} [Lean.MonadTrace m] (f : Lean.PersistentArray Lean.TraceElem → Lean.PersistentArray Lean.TraceElem) : m Unit

Equations

• Lean.modifyTraces f = Lean.modifyTraceState fun (s : Lean.TraceState) => { traces := f s.traces }

@[inline]

def Lean.setTraceState {m : Type → Type} [Lean.MonadTrace m] (s : Lean.TraceState) : m Unit

Equations

• Lean.setTraceState s = Lean.modifyTraceState fun (x : Lean.TraceState) => s

def Lean.addRawTrace {m : Type → Type} [Monad m] [Lean.MonadTrace m] [Lean.MonadRef m] [Lean.AddMessageContext m] (msg : Lean.MessageData) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.addTrace {m : Type → Type} [Monad m] [Lean.MonadTrace m] [Lean.MonadRef m] [Lean.AddMessageContext m] (cls : Lake.Name) (msg : Lean.MessageData) : m Unit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.trace {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (cls : Lake.Name) (msg : Unit → Lean.MessageData) : m Unit

Equations

• Lean.trace cls msg = do let __do_lift ← Lean.isTracingEnabledFor cls if __do_lift = true then Lean.addTrace cls (msg ()) else pure PUnit.unit

@[inline]

def Lean.traceM {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (cls : Lake.Name) (mkMsg : m Lean.MessageData) : m Unit

Equations

• Lean.traceM cls mkMsg = do let __do_lift ← Lean.isTracingEnabledFor cls if __do_lift = true then do let msg ← mkMsg Lean.addTrace cls msg else pure PUnit.unit

def Lean.withSeconds {α : Type} {m : Type → Type} [Monad m] [MonadLiftT BaseIO m] (act : m α) : m (α × Float)

Equations

• Lean.withSeconds act = do let start ← liftM IO.monoNanosNow let a ← act let stop ← liftM IO.monoNanosNow pure (a, Nat.toFloat (stop - start) / 1000000000)

opaque Lean.trace.profiler : Lean.Option Bool

opaque Lean.trace.profiler.threshold : Lean.Option Nat

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

Equations

• Lean.trace.profiler.threshold.getSecs o = Nat.toFloat (Lean.Option.get o Lean.trace.profiler.threshold) / 1000

@[inline]

def Lean.shouldProfile {m : Type → Type} [Monad m] [Lean.MonadOptions m] : m Bool

Equations

• Lean.shouldProfile = do let opts ← Lean.getOptions pure (Lean.Option.get opts Lean.profiler || Lean.Option.get opts Lean.trace.profiler)

@[inline]

def Lean.shouldEnableNestedTrace {m : Type → Type} [Monad m] [MonadLiftT IO m] [Lean.MonadOptions m] (cls : Lake.Name) (secs : Float) : m Bool

Equations

• One or more equations did not get rendered due to their size.

class Lean.MonadAlwaysExcept (ε : outParam (Type u)) (m : Type u → Type v) : Type (max (u + 1) v)

MonadExcept variant that is expected to catch all exceptions of the given type in case the standard instance doesn't.

In most circumstances, we want to let runtime exceptions during term elaboration bubble up to the command elaborator (see Core.tryCatch). However, in a few cases like building the trace tree, we really need to handle (and then re-throw) every exception lest we end up with a broken tree.

• except : MonadExceptOf ε m

instance Lean.instMonadAlwaysExceptEIO (ε : Type) : Lean.MonadAlwaysExcept ε (EIO ε)

Equations

• Lean.instMonadAlwaysExceptEIO ε = { except := inferInstance }

instance Lean.instMonadAlwaysExceptStateT {m : Type → Type} [Monad m] {σ : Type} (ε : Type) [always : Lean.MonadAlwaysExcept ε m] : Lean.MonadAlwaysExcept ε (StateT σ m)

Equations

• Lean.instMonadAlwaysExceptStateT ε = { except := let x := Lean.MonadAlwaysExcept.except; inferInstance }

instance Lean.instMonadAlwaysExceptStateRefT' {m : Type → Type} {ω : Type} {σ : Type} (ε : Type) [always : Lean.MonadAlwaysExcept ε m] : Lean.MonadAlwaysExcept ε (StateRefT' ω σ m)

Equations

• Lean.instMonadAlwaysExceptStateRefT' ε = { except := let x := Lean.MonadAlwaysExcept.except; inferInstance }

instance Lean.instMonadAlwaysExceptReaderT {m : Type → Type} {ρ : Type} (ε : Type) [always : Lean.MonadAlwaysExcept ε m] : Lean.MonadAlwaysExcept ε (ReaderT ρ m)

Equations

• Lean.instMonadAlwaysExceptReaderT ε = { except := let x := Lean.MonadAlwaysExcept.except; inferInstance }

def Lean.withTraceNode {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] {ε : Type} [always : Lean.MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Lake.Name) (msg : Except ε α → m Lean.MessageData) (k : m α) (collapsed : optParam Bool true) : m α

Equations

• One or more equations did not get rendered due to their size.

def Lean.withTraceNode' {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [Lean.MonadAlwaysExcept Lean.Exception m] [MonadLiftT BaseIO m] (cls : Lake.Name) (k : m (α × Lean.MessageData)) (collapsed : optParam Bool true) : m α

Equations

• One or more equations did not get rendered due to their size.

def Lean.registerTraceClass (traceClassName : Lake.Name) (inherited : optParam Bool false) (ref : autoParam Lake.Name _auto✝) : IO Unit

Registers a trace class.

By default, trace classes are not inherited; that is, set_option trace.foo true does not imply set_option trace.foo.bar true. Calling registerTraceClass `foo.bar (inherited := true) enables this inheritance on an opt-in basis.

Equations

• One or more equations did not get rendered due to their size.

def Lean.«doElemTrace[_]__» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.bombEmoji : String

Equations

• Lean.bombEmoji = "💥"

def Lean.checkEmoji : String

Equations

• Lean.checkEmoji = "✅"

def Lean.crossEmoji : String

Equations

• Lean.crossEmoji = "❌"

def Lean.exceptBoolEmoji {ε : Type u_1} : Except ε Bool → String

Equations

• Lean.exceptBoolEmoji x = match x with | Except.error a => Lean.bombEmoji | Except.ok true => Lean.checkEmoji | Except.ok false => Lean.crossEmoji

def Lean.exceptOptionEmoji {α : Type} {ε : Type u_1} : Except ε (Option α) → String

Equations

• Lean.exceptOptionEmoji x = match x with | Except.error a => Lean.bombEmoji | Except.ok (some val) => Lean.checkEmoji | Except.ok none => Lean.crossEmoji

def Lean.exceptEmoji {α : Type} {ε : Type u_1} : Except ε α → String

Visualize an Except using a checkmark or a cross.

Equations

• Lean.exceptEmoji x = match x with | Except.error a => Lean.crossEmoji | Except.ok a => Lean.checkEmoji

class Lean.ExceptToEmoji (ε : Type) (α : Type) : Type

• toEmoji : Except ε α → String

instance Lean.instExceptToEmojiBool {ε : Type} : Lean.ExceptToEmoji ε Bool

Equations

• Lean.instExceptToEmojiBool = { toEmoji := Lean.exceptBoolEmoji }

instance Lean.instExceptToEmojiOption {α : Type} {ε : Type} : Lean.ExceptToEmoji ε (Option α)

Equations

• Lean.instExceptToEmojiOption = { toEmoji := Lean.exceptOptionEmoji }

def Lean.withTraceNodeBefore {α : Type} {m : Type → Type} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] {ε : Type} [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [always : Lean.MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [Lean.ExceptToEmoji ε α] (cls : Lake.Name) (msg : m Lean.MessageData) (k : m α) (collapsed : optParam Bool true) : m α

Similar to withTraceNode, but msg is constructed before executing k. This is important when debugging methods such as isDefEq, and we want to generate the message before k updates the metavariable assignment. The class ExceptToEmoji is used to convert the result produced by k into an emoji (e.g., 💥, ✅, ❌).

TODO: find better name for this function.

Equations

• One or more equations did not get rendered due to their size.