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

78 lines
7.1 KiB
Text
Raw Permalink Blame History

[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨15, 2⟩-⟨15, 9⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨16, 2⟩-⟨16, 11⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.cdot⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.induction<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ ⟨20, 6⟩-⟨20, 15⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨23, 6⟩-⟨23, 15⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range>
• Goals accomplished!
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>
Reference in a new issue View git blame Copy permalink