From bd7827ed04c3853b98515d2941126e473225fc2d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Mar 2022 08:25:49 -0700
Subject: [PATCH] feat: `dbg_trace` tactic for low-level tactic debugging

---
 src/Init/Notation.lean                  | 2 ++
 src/Lean/Elab/Tactic/BuiltinTactic.lean | 5 +++++
 2 files changed, 7 insertions(+)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 89181b5a44..a3a14040be 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -437,6 +437,8 @@ syntax "trivial" : tactic
 
 syntax (name := split) "split " (colGt term)? (location)? : tactic
 
+syntax (name := dbgTrace) "dbg_trace " str : tactic
+
 /--
 The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`.
 The premises of this hypothesis, either universal quantifications or non-dependent implications,
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index fb32650d29..e80ec4712e 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -291,4 +291,9 @@ where
     | some msg => throwError "{msg}\n{goalsMsg}"
   | _ => throwUnsupportedSyntax
 
+@[tactic dbgTrace] def evalDbgTrace : Tactic := fun stx => do
+  match stx[1].isStrLit? with
+  | none     => throwIllFormedSyntax
+  | some msg => dbg_trace msg
+
 end Lean.Elab.Tactic