max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/815b.lean.out.expected
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

183 lines
12 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.

815b.lean:1:4-1:13: warning: declaration uses `sorry`
815b.lean:6:9-6:17: warning: declaration uses `sorry`
815b.lean:7:9-7:14: warning: declaration uses `sorry`
815b.lean:8:9-8:13: warning: declaration uses `sorry`
815b.lean:9:9-9:13: warning: declaration uses `sorry`
815b.lean:10:9-10:13: warning: declaration uses `sorry`
815b.lean:11:9-11:13: warning: declaration uses `sorry`
[Meta.synthInstance] ✅️ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] ✅️ new goal IsSmooth fun g a => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
[Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
[Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
has unused arguments, reduced type
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance] ✅️ new goal IsSmooth f
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance.apply] ✅️ apply inst✝ to IsSmooth f
[Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
[Meta.synthInstance.answer] ✅️ IsSmooth f
[Meta.synthInstance.resume] ✅️ propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
has unused arguments, reduced type
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.unusedArgs] ∀ (a : α) (b : β), IsSmooth (f b)
has unused arguments, reduced type
∀ (b : β), IsSmooth (f b)
Transformer
fun redf a => redf
[Meta.synthInstance] ✅️ new goal ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
[Meta.synthInstance.apply] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
[Meta.synthInstance] ✅️ new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
[Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ), IsSmooth f
has unused arguments, reduced type
IsSmooth f
Transformer
fun redf a a_1 => redf
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α) (a : δ),
IsSmooth f to subgoal ∀ (a : α) (a : δ), IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ) (b : β), IsSmooth (f b)
has unused arguments, reduced type
∀ (b : β), IsSmooth (f b)
Transformer
fun redf a a_1 => redf
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
has unused arguments, reduced type
∀ (a : α), IsSmooth fun g => f (g a)
Transformer
fun redf a a_1 => redf a
[Meta.synthInstance.apply] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
[Meta.synthInstance.apply] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
[Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
[Meta.synthInstance.apply] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
has unused arguments, reduced type
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
[Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
has unused arguments, reduced type
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance] ✅️ new goal IsSmooth fun g => g
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth f
[Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
[Meta.synthInstance.apply] ❌️ apply @diag to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
[Meta.synthInstance.apply] ❌️ apply @comp to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
[Meta.synthInstance.apply] ❌️ apply @parm to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
[Meta.synthInstance.apply] ❌️ apply @const to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
[Meta.synthInstance.apply] ✅️ apply @identity to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun a => a
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] ✅️ propagating IsSmooth fun a =>
a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
has unused arguments, reduced type
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
[Meta.synthInstance.resume] size: 3
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] ✅️ propagating IsSmooth fun b a =>
b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
has unused arguments, reduced type
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun b a => b a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 8
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
[Meta.synthInstance.resume] size: 6
[Meta.synthInstance.answer] ✅️ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] result swap fun a g => f (g a) d
Reference in a new issue View git blame Copy permalink