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.

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

Equations

• Lean.MessageData.instDecidableEqTraceResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lean.MessageData.instReprTraceResult : Repr TraceResult

Equations

• Lean.MessageData.instReprTraceResult = { reprPrec := Lean.MessageData.instReprTraceResult.repr }

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

Equations

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

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.

Note: the emoji constants include a variation selector (U+FE0F), but String.startsWith handles this since we check for the base codepoint which is always the prefix.

Equations

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

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.

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.