max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/infoFromFailure.lean
Kim Morrison e01cbf2b8f
feat: add structured TraceResult to TraceData (#12698) 
This PR adds a `result? : Option TraceResult` field to `TraceData` and
populates it in `withTraceNode` and `withTraceNodeBefore`, so that
metaprograms walking trace trees can determine success/failure
structurally instead of string-matching on emoji.

`TraceResult` has three cases: `.success` (checkEmoji), `.failure`
(crossEmoji), and `.error` (bombEmoji, exception thrown). An
`ExceptToTraceResult` typeclass converts `Except` results to
`TraceResult` directly, with instances for `Bool` and `Option`.
`TraceResult.toEmoji` converts back to emoji for display. This replaces
the previous `ExceptToEmoji` typeclass — `TraceResult` is now the
primary representation rather than being derived from emoji strings.

`withTraceNodeBefore` (used by `isDefEq`) uses
`ExceptToTraceResult.toTraceResult` directly, correctly handling `Bool`
(`.ok false` = failure) and `Option` (`.ok none` = failure), with
`Except.error` mapping to `.error`.

For `withTraceNode`, `result?` defaults to `none`. Callers can pass
`mkResult?` to provide structured results; when set, the corresponding
emoji is auto-prepended to the message.

Motivated by mathlib's `#defeq_abuse` diagnostic tactic
(https://github.com/leanprover-community/mathlib4/pull/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

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-10 02:42:57 +00:00

127 lines
9.2 KiB
Text
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

def A.foo {α : Type} [Add α] (a : α) : α × α :=
(a, a + a)
def B.foo {α : Type} (a : α) : α × α :=
(a, a)
open A
open B
set_option trace.Meta.synthInstance true
/--
info: B.foo "hello" : String × String
---
trace: [Meta.synthInstance] ❌️ Add String
[Meta.synthInstance] ✅️ new goal Add String
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
[Meta.synthInstance] ✅️ new goal Lean.Grind.Semiring String
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommSemiring String
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring String ≟ Lean.Grind.CommSemiring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommRing String
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing String ≟ Lean.Grind.CommRing String
[Meta.synthInstance] ✅️ no instances for Lean.Grind.Field String
[Meta.synthInstance.instances] #[]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.Ring String
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommMonoid String
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
[Meta.synthInstance] ✅️ new goal Lean.Grind.NatModule String
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
[Meta.synthInstance] ✅️ new goal Lean.Grind.IntModule String
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommGroup String
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
[Meta.synthInstance] result <not-available>
-/
#guard_msgs in
-- `foo` is overloaded, the case `A.foo` is discarded because we don't have an instance `[Add String]`.
-- However, we still want to see the trace since we used trace.Meta.synthInstance
#check foo "hello"
/--
trace: [Meta.synthInstance] ❌️ Add Bool
[Meta.synthInstance] ✅️ new goal Add Bool
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.Semiring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommSemiring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring Bool ≟ Lean.Grind.CommSemiring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommRing Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing Bool ≟ Lean.Grind.CommRing Bool
[Meta.synthInstance] ✅️ no instances for Lean.Grind.Field Bool
[Meta.synthInstance.instances] #[]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.Ring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.NatModule Bool
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.IntModule Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
[Meta.synthInstance] result <not-available>
-/
#guard_msgs in
theorem ex : foo true = (true, true) :=
rfl
Reference in a new issue View git blame Copy permalink