fix: interrupt exception was swallowed by some tryCatchRuntimeEx us…

…es (#4569)

This appears to have been a semantic merge conflict between #3940 and
#4129. The effect on the language server is that if two edits are
sufficiently close in time to create an interrupt, some elaboration
steps like `simp` may accidentally catch the exception when it is
triggered during their execution, which makes incrementality assume that
elaboration of the body was successful, which can lead to incorrect
reuse, presenting the interrupted state to the user with symptoms such
as "uses sorry" without accompanying errors and incorrect lints.

(cherry picked from commit f3cb8a6)

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

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

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

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": []}