feat: add structured TraceResult to TraceData#12698
Open
kim-em wants to merge 4 commits intoleanprover:masterfrom
Open
feat: add structured TraceResult to TraceData#12698kim-em wants to merge 4 commits intoleanprover:masterfrom
kim-em wants to merge 4 commits intoleanprover:masterfrom
Conversation
Adds a `result? : Option TraceResult` field to `TraceData`, so that `withTraceNode` and `withTraceNodeBefore` record structured success/failure information alongside the existing emoji in the rendered header. This allows metaprograms that walk trace trees to determine success or failure by checking `td.result?` instead of string-matching on emoji characters in the rendered `MessageData`. For `withTraceNodeBefore`, `result?` is derived from the emoji computed by `ExceptToEmoji`, correctly handling `Bool` (where `.ok false` = failure) and `Option` (where `.ok none` = failure). For `withTraceNode`, `result?` defaults to `.ok _ => success`, `.error _ => failure`. Callers needing different semantics can pass `result?` explicitly. Trace nodes not created by `withTraceNode`/`withTraceNodeBefore` (e.g. from `addTrace` or diagnostic formatting) get `result? := none`. Motivated by mathlib's `#defeq_abuse` diagnostic tactic (mathlib4#35750) which currently has to string-match on emoji to determine trace node outcomes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
eric-wieser
reviewed
Feb 26, 2026
`withTraceNode` doesn't have access to `ExceptToEmoji`, so it can't distinguish `Except.ok none` (failure) from `Except.ok (some _)` (success). Defaulting to `none` is the honest choice; callers that need structured results can pass `result?` explicitly. `withTraceNodeBefore` is unaffected — it correctly derives from the emoji string via `ExceptToEmoji`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…raceNodeBefore Both `withTraceNode` and `withTraceNodeBefore` now take a `mkResult? : Except ε α → Option TraceResult` callback instead of a fixed `result? : Option TraceResult`. This lets callers compute the structured result from the actual `Except` outcome. - `withTraceNode`: defaults to `fun _ => none` (callers opt in) - `withTraceNodeBefore`: defaults to inferring from `ExceptToEmoji` (success if emoji == checkEmoji, failure otherwise) This addresses the semantic mismatch where `Except.ok none` or `Except.ok false` would need to be reported as failure, not success. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The bomb emoji (💥) indicates an exception was thrown, which is semantically different from a normal failure (❌). Lumping them together as `.failure` loses this distinction. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
eric-wieser
reviewed
Feb 26, 2026
Comment on lines
+396
to
+398
| if emoji == checkEmoji then some .success | ||
| else if emoji == bombEmoji then some .error | ||
| else some .failure) : m α := do |
Contributor
There was a problem hiding this comment.
Rather thand doing a unicode string comparison here, I think it would make more sense to define ExceptToTraceResult, superseding ExceptToEmoji, and TraceResult.toEmoji?
Collaborator
Author
There was a problem hiding this comment.
Thanks, this is much better. I was a bit afraid of making breaking changes here, but it seems to be okay.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 1, 2026
This PR adds `#defeq_abuse in`, a tactic/command combinator for diagnosing `backward.isDefEq.respectTransparency` failures. It runs the given tactic or command with the option both `true` and `false`, and when the strict setting fails, walks the trace tree to identify the specific `isDefEq` checks that are root causes. Reusable trace-tree analysis utilities are extracted into `Mathlib.Lean.MessageData.Trace`: - `TraceResult` / `traceResultOf` — structured access to the ✅/❌/💥 status encoding - `foldTraceNodes` — generic fold over `MessageData` trace trees - `stripTraceResultPrefix` / `dedupByString` — helpers for trace content comparison Companion lean4 PRs that will simplify this further: - leanprover/lean4#12698 — structured `TraceResult` field on `TraceData` - leanprover/lean4#12699 — `Meta.synthInstance.apply` trace class See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency 🤖 Prepared with Claude Code Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
result? : Option TraceResultfield toTraceDataand populates it inwithTraceNodeandwithTraceNodeBefore, so that metaprograms walking trace trees can determine success/failure structurally instead of string-matching on emoji.TraceResulthas three cases:.success(checkEmoji),.failure(crossEmoji), and.error(bombEmoji, exception thrown). AnExceptToTraceResulttypeclass convertsExceptresults toTraceResultdirectly, with instances forBoolandOption.TraceResult.toEmojiconverts back to emoji for display. This replaces the previousExceptToEmojitypeclass —TraceResultis now the primary representation rather than being derived from emoji strings.For
withTraceNodeBefore(used byisDefEq), themkResultparameter defaults toExceptToTraceResult.toTraceResult, correctly handlingBool(.ok false= failure) andOption(.ok none= failure), withExcept.errormapping to.error.For
withTraceNode,result?defaults tonone. Callers can passmkResult?to provide structured results.Motivated by mathlib's
#defeq_abusediagnostic tactic (leanprover-community/mathlib4#35750) which currently string-matches on emoji to determine trace node outcomes. See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency🤖 Prepared with Claude Code