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.

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.