diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index a5c6ebee6832..b76cb4686370 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -472,23 +472,30 @@ def Exception.isInterrupt : Exception → Bool
 
 /--
 Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
-`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
+exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
+See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
+exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
     if ex.isInterrupt || ex.isRuntime then
-
-      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
+      throw ex
     else
       h ex
 
+/--
+A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
+Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
+exceptions.
+-/
 @[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
+    if ex.isInterrupt then
+      throw ex
     h ex
 
 instance : MonadExceptOf Exception CoreM where
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index c171612f296c..28acce42a624 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -81,7 +81,10 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
+/--
+Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
+want to catch and process them at the command level.
+-/
 @[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
     CommandElabM α := do
   try
diff --git a/tests/lean/interactive/incrementalCommand.lean b/tests/lean/interactive/incrementalCommand.lean
index 6a2dfcc311c8..80073dfc0ad1 100644
--- a/tests/lean/interactive/incrementalCommand.lean
+++ b/tests/lean/interactive/incrementalCommand.lean
@@ -38,3 +38,20 @@ elab "wrap" num c:command : command => do
    --v change: "1" "2"
 wrap 1 def wrapped := by
   dbg_trace "w"
+
+/-!
+The example used to result in nothing but "declaration uses 'sorry'" (and using the downstream
+"unreachable tactic" linter, the `simp` would be flagged) as `simp` among other elaborators
+accidentally swallowed the interrupt exception.
+-/
+-- RESET
+import Lean
+
+open Lean Elab Core in
+elab "interrupt" : tactic =>
+  throw <| .internal interruptExceptionId
+
+example : False := by
+  interrupt
+  simp
+--^ collectDiagnostics
diff --git a/tests/lean/interactive/incrementalCommand.lean.expected.out b/tests/lean/interactive/incrementalCommand.lean.expected.out
index 1f6ed9d79987..58fc2d238b16 100644
--- a/tests/lean/interactive/incrementalCommand.lean.expected.out
+++ b/tests/lean/interactive/incrementalCommand.lean.expected.out
@@ -2,3 +2,4 @@
 {"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
 w
 w
+{"version": 1, "uri": "file:///incrementalCommand.lean", "diagnostics": []}