Utilities for analyzing MessageData

WARNING: The declarations in this module may become obsolete with upcoming core changes.

TraceData has no structured success/failure field. Instead, withTraceNodeBefore (in Lean.Util.Trace) prepends emoji to the rendered header message using ExceptToEmoji:

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

The TraceResult type and traceResultOf function provide structured access to this encoding.

Pending lean4 PRs

These lean4 PRs may render declarations in this module obsolete:

• lean4#12698 adds TraceResult to TraceData. Once available, callers can use td.result? instead of parsing the header string.
• lean4#12699 adds a Meta.synthInstance.apply trace class, so synthesis "apply" nodes can be identified via td.cls instead of string-matching.

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

inductive Lean.MessageData.TraceResult : Type

The success/failure status of a trace node, as encoded by withTraceNodeBefore via emoji prefix on the rendered header.

Intended to match TraceResult from lean4#12698. Once that PR is available, callers should prefer td.result? over parsing the header string with traceResultOf.

• success : TraceResult

  Header starts with ✅️ (checkEmoji)

• failure : TraceResult

  Header starts with ❌️ (crossEmoji)

• error : TraceResult

  Header starts with 💥️ (bombEmoji) — an exception was thrown

@[implicit_reducible]

instance Lean.MessageData.instDecidableEqTraceResult : DecidableEq TraceResult

def Lean.MessageData.instReprTraceResult.repr : TraceResult → ℕ → Format

@[implicit_reducible]

instance Lean.MessageData.instReprTraceResult : Repr TraceResult

@[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.

Lean's withTraceNodeBefore 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.

@[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 withTraceNodeBefore have the form "{emoji}[{VS16}] {content}". This strips everything through the first space. Returns the string unchanged if no recognized status prefix is present.

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.

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

Deduplicate an array of MessageData by their rendered string representations.