Experimental: the postprocess_traces command

postprocess_traces post in cmd runs cmd and transforms its trace messages with the trace postprocessor post before they are reported. See Lean.PostprocessTraces.Basic for the postprocessor library.

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.

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

Equations

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