feat: add Meta.synthInstance.apply trace class#12699
Merged
kim-em merged 2 commits intoleanprover:masterfrom Mar 1, 2026
Merged
feat: add Meta.synthInstance.apply trace class#12699kim-em merged 2 commits intoleanprover:masterfrom
kim-em merged 2 commits intoleanprover:masterfrom
Conversation
Gives the `generate` function's "apply @foo to Goal" trace nodes their own trace sub-class `Meta.synthInstance.apply` instead of sharing the parent `Meta.synthInstance` class. This allows metaprograms that walk synthesis traces to distinguish instance application attempts from other synthesis nodes without string-matching on the header text. The new class is registered with `inherited := true`, so `set_option trace.Meta.synthInstance true` continues to show these nodes. Motivated by mathlib's `#defeq_abuse` diagnostic tactic which currently has to check `headerStr.contains "apply"` to identify these nodes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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>
pfaffelh
pushed a commit
to pfaffelh/mathlib4
that referenced
this pull request
Mar 2, 2026
…ity#35750) 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
2 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 gives the
generatefunction's "apply @foo to Goal" trace nodes their own trace sub-classMeta.synthInstance.applyinstead of sharing the parentMeta.synthInstanceclass.This allows metaprograms that walk synthesis traces to distinguish instance application attempts from other synthesis nodes by checking
td.clsrather than string-matching on the header text.The new class is registered with
inherited := true, soset_option trace.Meta.synthInstance truecontinues to show these nodes.Motivated by mathlib's
#defeq_abusediagnostic tactic (leanprover-community/mathlib4#35750) which currently checksheaderStr.contains "apply"to identify these nodes. See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency🤖 Prepared with Claude Code