feat: add trace <string> tactic

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.

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

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 []
 

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

tests/lean/traceStateBactracking.lean.expected.out

@@ -1,2 +1,3 @@
 h : 0 = 1
 ⊢ False
+first branch