sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
lean4/tests/elab/simpGround1.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

162 lines
9.4 KiB
Plaintext
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.
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f1 => f1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f1 [1, 2, 3] 5 => [6, 7, 8]
[Meta.Tactic.simp.ground] unfolded, f1 [1, 2, 3] 5 => (1 + 5) :: f1 [2, 3] 5
[Meta.Tactic.simp.ground] unfolded, f1 [2, 3] 5 => (2 + 5) :: f1 [3] 5
[Meta.Tactic.simp.ground] unfolded, f1 [3] 5 => (3 + 5) :: f1 [] 5
[Meta.Tactic.simp.ground] unfolded, f1 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: 6 => 6
[Meta.Tactic.simp.ground] ✅️ seval: 7 => 7
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f2 => f2
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 10 => 10
[Meta.Tactic.simp.ground] ✅️ seval: @Neg.neg => @Neg.neg
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [-2, 8] => [-2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [10, -2, 8] => [10, -2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 10, -2, 8] => [1, 10, -2, 8]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f2 [1, 10, -2, 8] (-5) => [-3, 15, -9, 11]
[Meta.Tactic.simp.ground] unfolded, f2 [1, 10, -2, 8] (-5) => add2 1 (-5) :: f2 [10, -2, 8] (-5)
[Meta.Tactic.simp.ground] unfolded, add2 1 (-5) => 1 + 1 + -5
[Meta.Tactic.simp.ground] unfolded, f2 [10, -2, 8] (-5) => add2 10 (-5) :: f2 [-2, 8] (-5)
[Meta.Tactic.simp.ground] unfolded, add2 10 (-5) => 10 + 10 + -5
[Meta.Tactic.simp.ground] unfolded, f2 [-2, 8] (-5) => add2 (-2) (-5) :: f2 [8] (-5)
[Meta.Tactic.simp.ground] unfolded, add2 (-2) (-5) => -2 + -2 + -5
[Meta.Tactic.simp.ground] unfolded, f2 [8] (-5) => add2 8 (-5) :: f2 [] (-5)
[Meta.Tactic.simp.ground] unfolded, add2 8 (-5) => 8 + 8 + -5
[Meta.Tactic.simp.ground] unfolded, f2 [] (-5) => []
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: 15 => 15
[Meta.Tactic.simp.ground] ✅️ seval: 9 => 9
[Meta.Tactic.simp.ground] ✅️ seval: 11 => 11
[Meta.Tactic.simp.ground] ✅️ seval: [11] => [11]
[Meta.Tactic.simp.ground] ✅️ seval: [-9, 11] => [-9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: [15, -9, 11] => [15, -9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: [-3, 15, -9, 11] => [-3, 15, -9, 11]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f3 => f3
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: 5 => 5
[Meta.Tactic.simp.ground] ✅️ seval: f3 [1, 2, 3] 5 => [6, 7, 8]
[Meta.Tactic.simp.ground] unfolded, f3 [1, 2, 3] 5 => (1 + 5) :: f3 [2, 3] 5
[Meta.Tactic.simp.ground] unfolded, f3 [2, 3] 5 => (2 + 5) :: f3 [3] 5
[Meta.Tactic.simp.ground] unfolded, f3 [3] 5 => (3 + 5) :: f3 [] 5
[Meta.Tactic.simp.ground] unfolded, f3 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: 6 => 6
[Meta.Tactic.simp.ground] ✅️ seval: 7 => 7
[Meta.Tactic.simp.ground] ✅️ seval: 8 => 8
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: f4 => f4
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: f4 [1, 2, 3] 5 => [6, 7, 8]
[Meta.Tactic.simp.ground] unfolded, f4 [1, 2, 3] 5 => (1 + 5) :: f4 [2, 3] 5
[Meta.Tactic.simp.ground] unfolded, f4 [2, 3] 5 => (2 + 5) :: f4 [3] 5
[Meta.Tactic.simp.ground] unfolded, f4 [3] 5 => (3 + 5) :: f4 [] 5
[Meta.Tactic.simp.ground] unfolded, f4 [] 5 => []
[Meta.Tactic.simp.ground] ✅️ seval: [8] => [8]
[Meta.Tactic.simp.ground] ✅️ seval: [7, 8] => [7, 8]
[Meta.Tactic.simp.ground] ✅️ seval: [6, 7, 8] => [6, 7, 8]
List.instAppend.{u} {α : Type u} : Append (List α)
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: @List.reverse => @List.reverse
[Meta.Tactic.simp.ground] ✅️ seval: @List.map => @List.map
[Meta.Tactic.simp.ground] ✅️ seval: @HAdd.hAdd => @HAdd.hAdd
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3, 4] => [2, 3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: @HAppend.hAppend => @HAppend.hAppend
[Meta.Tactic.simp.ground] ✅️ seval: 4 => 4
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3] => [4, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: @Eq => @Eq
[Meta.Tactic.simp.ground] ✅️ seval: @rev => @rev
[Meta.Tactic.simp.ground] ✅️ seval: @List.map => @List.map
[Meta.Tactic.simp.ground] ✅️ seval: @HAdd.hAdd => @HAdd.hAdd
[Meta.Tactic.simp.ground] ✅️ seval: 1 => 1
[Meta.Tactic.simp.ground] ✅️ seval: @List.cons => @List.cons
[Meta.Tactic.simp.ground] ✅️ seval: 2 => 2
[Meta.Tactic.simp.ground] ✅️ seval: 3 => 3
[Meta.Tactic.simp.ground] ✅️ seval: @List.nil => @List.nil
[Meta.Tactic.simp.ground] ✅️ seval: [] => []
[Meta.Tactic.simp.ground] ✅️ seval: [3] => [3]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3] => [2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [1, 2, 3] => [1, 2, 3]
[Meta.Tactic.simp.ground] ✅️ seval: [4] => [4]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 4] => [3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: [2, 3, 4] => [2, 3, 4]
[Meta.Tactic.simp.ground] ✅️ seval: rev [2, 3, 4] => [4, 3, 2]
[Meta.Tactic.simp.ground] unfolded, rev [2, 3, 4] => rev [3, 4] ++ [2]
[Meta.Tactic.simp.ground] unfolded, rev [3, 4] => rev [4] ++ [3]
[Meta.Tactic.simp.ground] unfolded, rev [4] => rev [] ++ [4]
[Meta.Tactic.simp.ground] unfolded, rev [] => []
[Meta.Tactic.simp.ground] unfolded, [] ++ [4] => instHAppendOfAppend.1 [] [4]
[Meta.Tactic.simp.ground] unfolded, instHAppendOfAppend => { hAppend := fun a b => Append.append a b }
[Meta.Tactic.simp.ground] unfolded, Append.append [] [4] => List.instAppend.1 [] [4]
[Meta.Tactic.simp.ground] unfolded, List.instAppend => { append := List.append }
[Meta.Tactic.simp.ground] unfolded, [].append [4] => [4]
[Meta.Tactic.simp.ground] unfolded, [4] ++ [3] => instHAppendOfAppend.1 [4] [3]
[Meta.Tactic.simp.ground] unfolded, Append.append [4] [3] => List.instAppend.1 [4] [3]
[Meta.Tactic.simp.ground] unfolded, [4].append [3] => 4 :: [].append [3]
[Meta.Tactic.simp.ground] unfolded, [].append [3] => [3]
[Meta.Tactic.simp.ground] unfolded, [4, 3] ++ [2] => instHAppendOfAppend.1 [4, 3] [2]
[Meta.Tactic.simp.ground] unfolded, Append.append [4, 3] [2] => List.instAppend.1 [4, 3] [2]
[Meta.Tactic.simp.ground] unfolded, [4, 3].append [2] => 4 :: [3].append [2]
[Meta.Tactic.simp.ground] unfolded, [3].append [2] => 3 :: [].append [2]
[Meta.Tactic.simp.ground] unfolded, [].append [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: 4 => 4
[Meta.Tactic.simp.ground] ✅️ seval: [2] => [2]
[Meta.Tactic.simp.ground] ✅️ seval: [3, 2] => [3, 2]
[Meta.Tactic.simp.ground] ✅️ seval: [4, 3, 2] => [4, 3, 2]
Reference in New Issue View Git Blame Copy Permalink