feat: dbg_trace tactic for low-level tactic debugging

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,

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