diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 83ff845c16..49fa5a5df3 100644
--- a/src/Init/Notation.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 1f695bf4b0..8beda4ffe3 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/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
diff --git a/tests/playground/sleep_save.lean b/tests/playground/sleep_save.lean
new file mode 100644
index 0000000000..598dfd4498
--- /dev/null
+++ b/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›