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)