Utilities for analyzing MessageData

Utility functions for working with trace messages.

withTraceNode (in Lean.Util.Trace) stores a TraceResult in TraceData.result? and prepends emoji to the rendered header:

• ✅️ (checkEmoji) for success
• ❌️ (crossEmoji) for failure
• 💥️ (bombEmoji) for exceptions

The traceResultOf function provides backward-compatible parsing of rendered headers.

@[deprecated Lean.TraceData.result? (since := "2026-03-23")]

def Lean.MessageData.traceResultOf (headerStr : String) : Option TraceResult

Determine the status of a trace node from its rendered header string.

withTraceNode prepends checkEmoji/crossEmoji/bombEmoji (defined in Lean.Util.Trace) to trace headers to indicate outcomes.

The TraceResult will be recorded in trace messages directly in lean4#12698. Once that PR is available, callers should prefer td.result? over calling this function.

Equations

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

@[deprecated Lean.TraceData (since := "2026-03-23")]

def Lean.MessageData.stripTraceResultPrefix (s : String) : String

Strip the leading status emoji and space from a trace header string, leaving just the semantic content for comparison across trace runs.

Trace headers from withTraceNode have the form "{emoji}[{VS16}] {content}". This strips everything through the first space. Returns the string unchanged if no recognized status prefix is present.

Equations

• Lean.MessageData.stripTraceResultPrefix s = if (Lean.MessageData.traceResultOf s).isNone = true then s else ((s.toSlice.dropPrefix fun (x : Char) => !x.isWhitespace).dropPrefix ' ').copy

def Lean.MessageData.extractInstName (s : String) : String

Extract the instance name from a rendered apply @Foo to Goal trace header. Returns the string between "apply " and " to ".

Note: this is fragile string matching against Lean's Meta.synthInstance trace format. If the trace format changes, this function will silently return the original string. Once lean4#12699 is available, these nodes will have trace class Meta.synthInstance.apply and can be identified structurally via td.cls instead of string-matching on the header.

Equations

• Lean.MessageData.extractInstName s = match s.splitOn "apply " with | [head, rest] => match rest.splitOn " to " with | name :: tail => name.trimAscii.toString | x => s | x => s

def Lean.MessageData.dedupByString (msgs : Array MessageData) : BaseIO (Array MessageData)

Deduplicate an array of MessageData by their rendered string representations.

Equations

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