From f3cb8a6c2d19c9325f3e5154c66b0a2c884860f2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 27 Jun 2024 12:03:22 +0200
Subject: [PATCH] fix: interrupt exception was swallowed by some
 `tryCatchRuntimeEx` uses (#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.
---
 src/Lean/CoreM.lean                             | 15 +++++++++++----
 src/Lean/Elab/Command.lean                      |  5 ++++-
 tests/lean/interactive/incrementalCommand.lean  | 17 +++++++++++++++++
 .../incrementalCommand.lean.expected.out        |  1 +
 4 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index a5c6ebee68..b76cb46863 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 c171612f29..28acce42a6 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 6a2dfcc311..80073dfc0a 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 1f6ed9d799..58fc2d238b 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": []}