Experimental: Stored Traces

Iterating on a trace postprocessor with postprocess_traces re-runs the traced command on every edit, which is impractical if the command is slow. store_traces_as t in cmd runs cmd once and stores its trace messages under the name t; #trace_roots t and #postprocess_traces t post then inspect the stored trace without re-running cmd.

Stored traces are kept in an in-memory environment extension and are only available in the file that stored them; they are not exported to .olean files. store_traces_as declares t : CoreM StoredTrace, which merely references the stored data, so that metaprograms can inspect the trace as well.

def Lean.PostprocessTraces.storeTracesAsCmd : ParserDescr

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

store_traces_as t in cmd runs cmd, reports its output unchanged, and additionally stores the trace messages it produced under the name t. The stored trace can then be inspected without re-running cmd using #trace_roots t and #postprocess_traces t post, which is useful when cmd is slow and the right trace postprocessor is found iteratively.

store_traces_as also adds a declaration t : CoreM Lean.PostprocessTraces.StoredTrace to the environment, so the trace can be inspected by arbitrary metaprograms, e.g. #eval do return (← t).roots.size. The declaration only references the trace data, which is kept in memory for the current file only; it is not exported to .olean files.

Equations

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

def Lean.PostprocessTraces.postprocessStoredTracesCmd : ParserDescr

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

#postprocess_traces t post applies the trace postprocessor post : TracePostprocessor to the trace stored as t by store_traces_as t in cmd and then renders the resulting trace tree. See postprocess_traces for the available operations and patterns.

Equations

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

structure Lean.PostprocessTraces.StoredTrace : Type

A trace stored by store_traces_as t in cmd, for inspection in metaprograms.

store_traces_as declares t : CoreM StoredTrace, so the stored trace can be retrieved in any metaprogram that can run CoreM, e.g. #eval do return (← t).roots.size. The trace data itself is kept in an in-memory environment extension and is only available in the file that stored it; in particular, it is not exported to .olean files. The declaration only holds a reference, so declaring it is cheap even for very large traces.

• messages : Array Message

  The stored trace messages: one message per source range inside the traced command, see addTraceAsMessages.

@[instance_reducible]

instance Lean.PostprocessTraces.instInhabitedStoredTrace : Inhabited StoredTrace

Equations

• Lean.PostprocessTraces.instInhabitedStoredTrace = { default := Lean.PostprocessTraces.instInhabitedStoredTrace.default }

def Lean.PostprocessTraces.findStoredTrace? (env : Environment) (declName : Name) : Option StoredTrace

Returns the trace stored under the declaration declName, if any.

Equations

• Lean.PostprocessTraces.findStoredTrace? env declName = (Lean.PostprocessTraces.storedTracesExt✝.getState env).find? declName

def Lean.PostprocessTraces.allStoredTraces (env : Environment) : List (Name × StoredTrace)

The names of all traces stored in the current file, with their stored traces.

Equations

• Lean.PostprocessTraces.allStoredTraces env = Std.TreeMap.toList (Lean.PostprocessTraces.storedTracesExt✝.getState env)

def Lean.PostprocessTraces.findStoredTrace (declName : Name) : CoreM StoredTrace

Returns the trace stored under the declaration declName. This is the implementation of the declarations created by store_traces_as; the trace data is only available in the file that stored it.

Equations

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

def Lean.PostprocessTraces.storeTraces (declName : Name) (t : StoredTrace) : CoreM Unit

Stores t under the declaration declName, overwriting any previously stored trace.

Equations

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

def Lean.PostprocessTraces.StoredTrace.trees (t : StoredTrace) : Array TraceTree

All trace trees of the stored trace, across all of its messages.

Equations

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

def Lean.PostprocessTraces.StoredTrace.postprocess (t : StoredTrace) (post : TracePostprocessor) : CoreM StoredTrace

Applies a postprocessor to every trace message of the stored trace, dropping messages whose roots were all removed.

Equations

• t.postprocess post = do let __do_lift ← Array.filterMapM (fun (x : Lean.Message) => Lean.Elab.PostprocessTraces.postprocessMessage post x) t.messages pure { messages := __do_lift }

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

Equations

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

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

Equations

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