Experimental: Trace Postprocessors and the postprocess_traces Command

Trace messages of complex elaboration tasks can be very large, and finding the relevant part in the editor requires a lot of clicking and searching. This module provides trace postprocessors: functions that transform the trace of a command before it is reported, e.g. by filtering out irrelevant subtrees, hoisting the interesting ones, or pre-expanding the paths to matches.

A trace postprocessor (Lean.PostprocessTraces.TracePostprocessor) receives the array of trace roots of one trace message and returns the transformed roots. The Lean.PostprocessTraces namespace provides a small set of operations (filterSubtrees, hoist, exposeSubtrees, countNodes, selfTime) that compose left-to-right with >=>. The selecting operations take a pattern (Lean.PostprocessTraces.TracePattern), a predicate on trace subtrees; built-in patterns select by trace class (ofClass), text (containsString), result (succeeded, failed, errored, unsuccessful), and time (minTimeMs, minSelfTimeMs). Users can define their own postprocessors and patterns as ordinary functions.

Syntax: postprocess_traces post in cmd transforms the trace messages produced by cmd with post.

Traces are stored as MessageData (see MessageData.trace); TraceTree is a structured view of such messages that takes care of the context wrappers (MessageData.withContext etc.) around trace nodes.

def Lean.PostprocessTraces.postprocessTracesCmd : ParserDescr

Experimental. postprocess_traces and the library around it are expected to change in the future.

postprocess_traces post in cmd runs cmd and transforms every trace message it produces with the trace postprocessor post : Lean.PostprocessTraces.TracePostprocessor before it is reported.

The postprocessor receives the array of trace roots of each trace message and returns the transformed roots; returning an empty array drops the message entirely. The Lean.PostprocessTraces namespace (automatically opened in post) provides operations such as filterSubtrees, hoist, exposeSubtrees, and selfTime, which take patterns such as ofClass, containsString, and minTimeMs and compose left-to-right with >=>. User-defined postprocessors and patterns are ordinary functions.

For example, the following only shows the instance-synthesis steps that mention tryResolve, together with their ancestors:

set_option trace.Meta.synthInstance true in
postprocess_traces filter (containsString "tryResolve") in
example : Inhabited (List Nat) := inferInstance

Equations

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

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 }

def Lean.Elab.PostprocessTraces.elabPostprocessTraces : Command.CommandElab

Equations

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

@[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.PostprocessTraces.ofClass (cls : Name) : TracePattern

Matches the trace nodes with the exact trace class cls.

Equations

• Lean.PostprocessTraces.ofClass cls t = pure (t.cls? == some cls)

def Lean.PostprocessTraces.containsString (pat : String) : TracePattern

Matches the subtrees whose trace class or head message contains pat as a substring. For large traces, this is an expensive pattern because all head messages need to be pretty-printed; to select nodes by their exact trace class, prefer the much cheaper ofClass.

Equations

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

def Lean.PostprocessTraces.succeeded : TracePattern

Matches the trace nodes whose action succeeded (✅️, TraceResult.success). Nodes without a recorded result (e.g. from addTrace) do not match.

Equations

• Lean.PostprocessTraces.succeeded t = pure (t.result? == some Lean.TraceResult.success)

def Lean.PostprocessTraces.failed : TracePattern

Matches the trace nodes whose action failed (❌️, TraceResult.failure).

Equations

• Lean.PostprocessTraces.failed t = pure (t.result? == some Lean.TraceResult.failure)

def Lean.PostprocessTraces.errored : TracePattern

Matches the trace nodes whose action threw an exception (💥️, TraceResult.error).

Equations

• Lean.PostprocessTraces.errored t = pure (t.result? == some Lean.TraceResult.error)

def Lean.PostprocessTraces.unsuccessful : TracePattern

Matches the trace nodes whose action did not succeed, i.e. failed (❌️) or threw an exception (💥️). Nodes without a recorded result (e.g. from addTrace) do not match.

Equations

• Lean.PostprocessTraces.unsuccessful t = pure (t.result? == some Lean.TraceResult.failure || t.result? == some Lean.TraceResult.error)

def Lean.PostprocessTraces.minTimeMs (ms : Float) : TracePattern

Matches the subtrees whose action took at least ms milliseconds. Timing information is only available with set_option trace.profiler true.

Equations

• Lean.PostprocessTraces.minTimeMs ms t = pure (decide (t.elapsed * 1000 ≥ ms))

def Lean.PostprocessTraces.minSelfTimeMs (ms : Float) : TracePattern

Matches the subtrees whose action took at least ms milliseconds outside of their child nodes. Timing information is only available with set_option trace.profiler true.

Equations

• Lean.PostprocessTraces.minSelfTimeMs ms t = pure (decide (t.selfElapsed * 1000 ≥ ms))

def Lean.PostprocessTraces.filterSubtrees (p : TracePattern) : TracePostprocessor

Keeps only the subtrees matching p, together with their ancestors for context; all other nodes are removed. Matching subtrees are kept in their entirety and not searched for nested matches (see TraceTree.filterSubtrees).

Equations

• Lean.PostprocessTraces.filterSubtrees p roots = Array.filterMapM (fun (x : Lean.PostprocessTraces.TraceTree) => Lean.PostprocessTraces.TraceTree.filterSubtrees p x) roots

def Lean.PostprocessTraces.hoist (p : TracePattern) : TracePostprocessor

Hoists the subtrees matching p to the top level, so that every new trace root is a match; ancestors and unrelated subtrees are discarded. Matches nested inside other matches are not searched for.

Equations

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

def Lean.PostprocessTraces.exposeSubtrees (p : TracePattern) : TracePostprocessor

Expands all transitive ancestors of the subtrees matching p in the editor, so that the trace opens already showing all matches. No nodes are removed, and all other nodes, including the matches themselves, keep their expansion state. Matching subtrees are not searched for nested matches.

Equations

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

def Lean.PostprocessTraces.countNodes : TracePostprocessor

Appends the number of nodes inside each subtree to the subtree's head message.

Equations

• Lean.PostprocessTraces.countNodes roots = pure (Array.map (fun (root : Lean.PostprocessTraces.TraceTree) => (Lean.PostprocessTraces.countNodes.go✝ root).fst) roots)

def Lean.PostprocessTraces.selfTime : TracePostprocessor

Appends the number of milliseconds spent inside each subtree but outside of its child nodes to the subtree's head message. Timing information is only available with set_option trace.profiler true; nodes without it are not annotated.

Equations

• Lean.PostprocessTraces.selfTime roots = pure (Array.map Lean.PostprocessTraces.selfTime.go✝ roots)