See Lean.PostprocessTraces.

inductive Lean.PostprocessTraces.TraceTree : Type

A structured view of a trace message (MessageData.trace), used by trace postprocessors (see TracePostprocessor).

• node (data : TraceData) (msg : MessageData) (children : Array TraceTree) (wrap : MessageData → MessageData) : TraceTree

  A trace node [data.cls] msg with the given children.

  wrap restores the context wrappers (MessageData.withContext etc.) that were peeled off the original MessageData while decomposing it; it is re-applied around the node by toMessageData.

• leaf (msg : MessageData) : TraceTree

  A child message that is not itself a trace node (e.g. produced by addRawTrace).

@[instance_reducible]

instance Lean.PostprocessTraces.instInhabitedTraceTree : Inhabited TraceTree

def Lean.PostprocessTraces.TraceTree.ofMessageData (msg : MessageData) : TraceTree

Decomposes trace MessageData into a TraceTree. The MessageData can be reconstructed using TraceTree.toMessageData.

partial def Lean.PostprocessTraces.TraceTree.toMessageData : TraceTree → MessageData

Reassembles the MessageData of a trace tree.

@[reducible, inline]

abbrev Lean.PostprocessTraces.TracePostprocessor : Type

A trace postprocessor transforms the trace roots of a trace message before it is reported, e.g. by filtering out irrelevant subtrees or pre-expanding interesting nodes. Returning an empty array drops the trace message entirely.

Traces are reported as one message per source range inside a command, and a postprocessor is applied to each of these messages separately; it therefore cannot move trace roots from one source range to another.

Postprocessors are applied by the postprocess_traces post in cmd command and can be composed left-to-right with >=>.

@[instance_reducible]

instance Lean.PostprocessTraces.instInhabitedTracePostprocessor : Inhabited TracePostprocessor

@[reducible, inline]

abbrev Lean.PostprocessTraces.TracePattern : Type

A pattern selects the trace subtrees that an operation acts on (see filter, hoist, and expand). Patterns are ordinary predicates: the built-in ones (such as containsString, unsuccessful, or minTimeMs) can be combined with custom conditions in a fun.

def Lean.PostprocessTraces.TraceTree.data? : TraceTree → Option TraceData

The TraceData of a trace node; none for leaf messages.

def Lean.PostprocessTraces.TraceTree.cls? (t : TraceTree) : Option Name

The trace class of a trace node; none for leaf messages.

def Lean.PostprocessTraces.TraceTree.children : TraceTree → Array TraceTree

The children of this tree.

def Lean.PostprocessTraces.TraceTree.withChildren (t : TraceTree) (children : Array TraceTree) : TraceTree

Replaces the children of a trace node. Leaf messages are returned unchanged.

def Lean.PostprocessTraces.TraceTree.modifyData (t : TraceTree) (f : TraceData → TraceData) : TraceTree

Transforms the TraceData of a trace node. Leaf messages are returned unchanged.

def Lean.PostprocessTraces.TraceTree.elapsed (t : TraceTree) : Float

Elapsed time of this node in seconds; 0 if no profiling data is available.

def Lean.PostprocessTraces.TraceTree.selfElapsed (t : TraceTree) : Float

Elapsed time of this node that is not accounted for by its children, in seconds; 0 if no profiling data is available.

def Lean.PostprocessTraces.TraceTree.headText : TraceTree → BaseIO String

The message of this node (without its children), formatted as a string. Useful for text-based filters but expensive.

def Lean.PostprocessTraces.TraceTree.result? (t : TraceTree) : Option TraceResult

The TraceResult of a trace node; none for leaf messages and nodes without a result.

partial def Lean.PostprocessTraces.TraceTree.collectSubtrees (p : TracePattern) (t : TraceTree) (acc : Array TraceTree := #[]) : CoreM (Array TraceTree)

Collects all maximal subtrees satisfying p in acc: adds t itself if p t holds, and otherwise recurses into the children. Matching subtrees are not searched for nested matches.

partial def Lean.PostprocessTraces.TraceTree.filterSubtrees (p : TracePattern) (t : TraceTree) : CoreM (Option TraceTree)

Prunes the tree to the subtrees satisfying p, keeping their ancestors for context; none if there is no match. The resulting tree consists of those nodes that either have a matching ancestor or transitive child. Matching subtrees are not searched for nested matches.

def Lean.Elab.PostprocessTraces.traceContainer? (data : MessageData) : Option ((Array MessageData → MessageData) × Array MessageData)

Decomposes the synthetic container message produced by addTraceAsMessages (.tagged `trace <| .trace _ _ roots, possibly inside context wrappers) into its trace roots, together with a function that reassembles the container from transformed roots.

def Lean.Elab.PostprocessTraces.postprocessMessage (post : PostprocessTraces.TracePostprocessor) (msg : Message) : CoreM (Option Message)

Applies post to a trace message (see addTraceAsMessages), returning none if the postprocessor dropped all roots of the message. Non-trace messages are returned unchanged.

def Lean.Elab.PostprocessTraces.runAndCollectMessages (cmd : Syntax) : Command.CommandElabM (Array Message)

Runs a command and returns all messages (sync and async) it produces, clearing the snapshot tasks after collection so that async messages are not reported twice. The surrounding message log is unaffected; it is restored even if the command is interrupted.

def Lean.Elab.PostprocessTraces.evalPostprocessorTopLevel (post : Term) : Command.CommandElabM PostprocessTraces.TracePostprocessor

Evaluates the postprocessor without leaking the traces produced by elaborating the postprocessor term itself into the (typically trace-enabled) surrounding context.