feat: add sleep tactic for debugging purposes

src/Init/Notation.lean

@@ -601,6 +601,9 @@ syntax (name := checkpoint) "checkpoint " tacticSeq : tactic
 
 macro (name := save) "save" : tactic => `(skip)
 
+/-- The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing. It is used for debugging purposes only. -/
+syntax (name := sleep) "sleep" num : tactic
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -351,9 +351,14 @@ where
     | some msg => throwError "{msg}\n{goalsMsg}"
   | _ => throwUnsupportedSyntax
 
-@[tactic dbgTrace] def evalDbgTrace : Tactic := fun stx => do
+@[builtinTactic dbgTrace] def evalDbgTrace : Tactic := fun stx => do
   match stx[1].isStrLit? with
   | none     => throwIllFormedSyntax
   | some msg => dbg_trace msg
 
+@[builtinTactic sleep] def evalSleep : Tactic := fun stx => do
+  match stx[1].isNatLit? with
+  | none    => throwIllFormedSyntax
+  | some ms => IO.sleep ms.toUInt32
+
 end Lean.Elab.Tactic

tests/playground/sleep_save.lean

@@ -0,0 +1,10 @@
+macro "expensive_tactic" : tactic => `(sleep 5000)
+
+example (h₁ : x = y) (h₂ : y = z) : z = x := by
+  expensive_tactic
+  save
+  have : y = x := h₁.symm
+  have : z = y := h₂.symm
+  trace "hello world"
+  apply this.trans
+  exact ‹y = x›