From 10657f5e812cd9dcd9f27415506f6106bb2ea53e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Feb 2022 11:16:42 -0800
Subject: [PATCH] feat: add `trace <string>` tactic

---
 RELEASES.md                                        | 2 ++
 src/Init/Notation.lean                             | 1 +
 src/Lean/Elab/Tactic/BuiltinTactic.lean            | 7 +++++++
 tests/lean/traceStateBactracking.lean              | 3 +++
 tests/lean/traceStateBactracking.lean.expected.out | 1 +
 5 files changed, 14 insertions(+)

diff --git a/RELEASES.md b/RELEASES.md
index f508cecbc6..4c42671e5d 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -88,3 +88,5 @@ termination_by' measure fun ⟨i, _⟩ => as.size - i
 * Add `fail msg?` tactic that always fail.
 
 * Add support for acyclicity at dependent elimination. See [issue #1022](https://github.com/leanprover/lean4/issues/1022).
+
+* Add `trace <string>` tactic for debugging purposes.
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 1525a1585c..b6f2612f4f 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -303,6 +303,7 @@ syntax (name := skip) "skip" : tactic
 /-- `done` succeeds iff there are no remaining goals. -/
 syntax (name := done) "done" : tactic
 syntax (name := traceState) "trace_state" : tactic
+syntax (name := traceMessage) "trace " str : tactic
 syntax (name := failIfSuccess) "fail_if_success " tacticSeq : tactic
 syntax (name := paren) "(" tacticSeq ")" : tactic
 syntax (name := withReducible) "with_reducible " tacticSeq : tactic
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 21d54e8182..fb32650d29 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -131,6 +131,13 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   let gs ← getUnsolvedGoals
   addRawTrace (goalsToMessageData gs)
 
+@[builtinTactic traceMessage] def evalTraceMessage : Tactic := fun stx => do
+  match stx[1].isStrLit? with
+  | none     => throwIllFormedSyntax
+  | some msg =>
+    let gs ← getUnsolvedGoals
+    withRef stx[0] <| addRawTrace msg
+
 @[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx =>
   liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure []
 
diff --git a/tests/lean/traceStateBactracking.lean b/tests/lean/traceStateBactracking.lean
index ec5a4ba9f0..921bf8da80 100644
--- a/tests/lean/traceStateBactracking.lean
+++ b/tests/lean/traceStateBactracking.lean
@@ -1,2 +1,5 @@
 example (h : 0 = 1) : False := by
   first | trace_state; fail | contradiction
+
+example (h : 0 = 1) : False := by
+  first | trace "first branch"; fail | contradiction
diff --git a/tests/lean/traceStateBactracking.lean.expected.out b/tests/lean/traceStateBactracking.lean.expected.out
index 0b6f1f21b1..c9eb230451 100644
--- a/tests/lean/traceStateBactracking.lean.expected.out
+++ b/tests/lean/traceStateBactracking.lean.expected.out
@@ -1,2 +1,3 @@
 h : 0 = 1
 ⊢ False
+first branch