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

Equations

• Lean.PostprocessTraces.instInhabitedTraceTree = { default := Lean.PostprocessTraces.TraceTree.leaf Lean.MessageData.nil }

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

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

Equations

• Lean.PostprocessTraces.TraceTree.ofMessageData msg = Lean.PostprocessTraces.TraceTree.ofMessageData.go✝ id msg

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 >=>.

Equations

• Lean.PostprocessTraces.TracePostprocessor = (Array Lean.PostprocessTraces.TraceTree → Lean.CoreM (Array Lean.PostprocessTraces.TraceTree))

@[instance_reducible]

instance Lean.PostprocessTraces.instInhabitedTracePostprocessor : Inhabited TracePostprocessor

Equations

• Lean.PostprocessTraces.instInhabitedTracePostprocessor = { default := fun (roots : Array Lean.PostprocessTraces.TraceTree) => pure roots }

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

Equations

• Lean.PostprocessTraces.TracePattern = (Lean.PostprocessTraces.TraceTree → Lean.CoreM Bool)

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

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

Equations

• (Lean.PostprocessTraces.TraceTree.node data msg children wrap).data? = some data
• (Lean.PostprocessTraces.TraceTree.leaf msg).data? = none

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

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

Equations

• t.cls? = Option.map (fun (x : Lean.TraceData) => x.cls) t.data?

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

The children of this tree.

Equations

• (Lean.PostprocessTraces.TraceTree.node data msg children wrap).children = children
• (Lean.PostprocessTraces.TraceTree.leaf msg).children = #[]

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

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

Equations

• (Lean.PostprocessTraces.TraceTree.node data msg children_1 wrap).withChildren children = Lean.PostprocessTraces.TraceTree.node data msg children wrap
• (Lean.PostprocessTraces.TraceTree.leaf msg).withChildren children = Lean.PostprocessTraces.TraceTree.leaf msg

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

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

Equations

• (Lean.PostprocessTraces.TraceTree.node data msg children wrap).modifyData f = Lean.PostprocessTraces.TraceTree.node (f data) msg children wrap
• (Lean.PostprocessTraces.TraceTree.leaf msg).modifyData f = Lean.PostprocessTraces.TraceTree.leaf msg

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

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

Equations

• t.elapsed = match t.data? with | some data => data.stopTime - data.startTime | none => 0

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.

Equations

• t.selfElapsed = max 0 (t.elapsed - Array.foldl (fun (s : Float) (c : Lean.PostprocessTraces.TraceTree) => s + c.elapsed) 0 t.children)

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.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.PostprocessTraces.TraceTree.leaf msg).headText = msg.toString

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

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

Equations

• t.result? = t.data?.bind fun (x : Lean.TraceData) => x.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.

Equations

• Lean.Elab.PostprocessTraces.traceContainer? data = Lean.Elab.PostprocessTraces.traceContainer?.go✝ id data

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.

Equations

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

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.

Equations

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

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.

Equations

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