Revert "Cancel outstanding tasks on document edit in the language server" (#2703)

* Revert "perf: inline `checkInterrupted`"

This reverts commit 6494af4513.

* Revert "fix: switch to C++ interruption whitelist"

This reverts commit 5aae74199b.

* Revert "fix: do not throw interrupt exceptions inside pure functions"

This reverts commit c0e3b9568e.

* Revert "feat: cancel tasks on document edit"

This reverts commit a2e2481c51.

* Revert "feat: translate `interrupted` kernel exception"

This reverts commit 14c640c15e.

* Revert "feat: check task cancellation in elaborator"

This reverts commit 2070df2328.

* Revert "feat: move `check_interrupted` from unused thread class to `Task` cancellation"

This reverts commit bf48a18cf9.

src/Lean/CoreM.lean

@@ -199,11 +199,6 @@ instance [MetaEval α] : MetaEval (CoreM α) where
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
-@[inline] def checkInterrupted : CoreM Unit := do
-  if (← IO.checkCanceled) then
-    -- should never be visible to users!
-    throw <| Exception.error .missing "elaboration interrupted"
-
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
@@ -217,11 +212,6 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats
 
-def checkSystem (moduleName : String) : CoreM Unit := do
-  -- TODO: bring back more checks from the C++ implementation
-  checkInterrupted
-  checkMaxHeartbeats moduleName
-
 private def withCurrHeartbeatsImp (x : CoreM α) : CoreM α := do
   let heartbeats ← IO.getNumHeartbeats
   withReader (fun ctx => { ctx with initHeartbeats := heartbeats }) x
@@ -250,7 +240,7 @@ instance : MonadLog CoreM where
 
 end Core
 
-export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
+export Core (CoreM mkFreshUserName checkMaxHeartbeats withCurrHeartbeats)
 
 @[inline] def withAtLeastMaxRecDepth [MonadFunctorT CoreM m] (max : Nat) : m α → m α :=
   monadMap (m := CoreM) <| withReader (fun ctx => { ctx with maxRecDepth := Nat.max max ctx.maxRecDepth })

src/Lean/Elab/Do.lean

@@ -1595,7 +1595,7 @@ mutual
   partial def doSeqToCode : List Syntax → M CodeBlock
     | [] => do liftMacroM mkPureUnitAction
     | doElem::doElems => withIncRecDepth <| withRef doElem do
-      checkSystem "`do`-expander"
+      checkMaxHeartbeats "`do`-expander"
       match (← liftMacroM <| expandMacro? doElem) with
       | some doElem => doSeqToCode (doElem::doElems)
       | none =>

src/Lean/Elab/Term.lean

@@ -1354,7 +1354,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
   | .missing => mkSyntheticSorryFor expectedType?
   | stx => withFreshMacroScope <| withIncRecDepth do
     withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}") do
-    checkSystem "elaborator"
+    checkMaxHeartbeats "elaborator"
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>

src/Lean/Environment.lean

@@ -230,7 +230,6 @@ inductive KernelException where
   | deterministicTimeout
   | excessiveMemory
   | deepRecursion
-  | interrupted
 
 namespace Environment
 

src/Lean/Message.lean

@@ -370,7 +370,6 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"
   | deepRecursion                       => "(kernel) deep recursion detected"
-  | interrupted                         => "(kernel) interrupted"
 
 end KernelException
 end Lean

src/Lean/Meta/ExprDefEq.lean

@@ -1851,7 +1851,7 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
-  checkSystem "isDefEq"
+  checkMaxHeartbeats "isDefEq"
   whenUndefDo (isDefEqQuick t s) do
   whenUndefDo (isDefEqProofIrrel t s) do
   /-

src/Lean/Meta/SynthInstance.lean

@@ -175,8 +175,7 @@ structure State where
 
 abbrev SynthM := ReaderT Context $ StateRefT State MetaM
 
-def checkSystem : SynthM Unit := do
-  Core.checkInterrupted
+def checkMaxHeartbeats : SynthM Unit := do
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
 @[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
@@ -553,7 +552,7 @@ def resume : SynthM Unit := do
       consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx, size := cNode.size + answer.size }
 
 def step : SynthM Bool := do
-  checkSystem
+  checkMaxHeartbeats
   let s ← get
   if !s.resumeStack.isEmpty then
     resume

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -268,7 +268,7 @@ where
       e
 
 partial def simp (e : Expr) : M Result := withIncRecDepth do
-  checkSystem "simp"
+  checkMaxHeartbeats "simp"
   let cfg ← getConfig
   if (← isProof e) then
     return { expr := e }

src/Lean/Meta/WHNF.lean

@@ -863,7 +863,7 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do
-    checkSystem "whnf"
+    checkMaxHeartbeats "whnf"
     let useCache ← useWHNFCache e
     match (← cached? useCache e) with
     | some e' => pure e'

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -240,7 +240,7 @@ partial def delabFor : Name → Delab
     <|> if k.isAtomic then failure else delabFor k.getRoot
 
 partial def delab : Delab := do
-  checkSystem "delab"
+  checkMaxHeartbeats "delab"
   let e ← getExpr
 
   -- no need to hide atomic proofs

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -351,7 +351,7 @@ abbrev AnalyzeAppM := ReaderT App.Context (StateT App.State AnalyzeM)
 mutual
 
   partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do
-    checkSystem "Delaborator.topDownAnalyze"
+    checkMaxHeartbeats "Delaborator.topDownAnalyze"
     trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}"
     let e ← getExpr
     let opts ← getOptions

src/Lean/Server/AsyncList.lean

@@ -112,20 +112,6 @@ partial def getFinishedPrefix : AsyncList ε α → BaseIO (List α × Option ε
 def waitHead? (as : AsyncList ε α) : Task (Except ε (Option α)) :=
   as.waitFind? fun _ => true
 
-/-- Cancels all tasks in the list. -/
-partial def cancel : AsyncList ε α → BaseIO Unit
-  | cons _ tl => tl.cancel
-  | nil => pure ()
-  | delayed tl => do
-    -- mind the order: if we asked the task whether it is still running
-    -- *before* cancelling it, it could be the case that it finished
-    -- just in between and has enqueued a dependent task that we would
-    -- miss (recall that cancellation is inherited by dependent tasks)
-    IO.cancel tl
-    if (← hasFinished tl) then
-      if let .ok t := tl.get then
-        t.cancel
-
 end AsyncList
 
 end IO

src/Lean/Server/FileWorker.lean

@@ -300,7 +300,6 @@ section Updates
       let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
       -- Ignore exceptions, we are only interested in the successful snapshots
       let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
-      oldDoc.cmdSnaps.cancel
       -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
       -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
       let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
@@ -466,7 +465,6 @@ section MainLoop
     | Message.notification "exit" none =>
       let doc := st.doc
       doc.cancelTk.set
-      doc.cmdSnaps.cancel
       return ()
     | Message.notification method (some params) =>
       handleNotification method (toJson params)

src/kernel/expr_eq_fn.cpp

@@ -60,9 +60,7 @@ template<bool CompareBinderInfo>
 class expr_eq_fn {
     eq_cache & m_cache;
 
-    static void check_system() {
-        ::lean::check_system("expression equality test");
-    }
+    static void check_system() { ::lean::check_system("expression equality test"); }
 
     bool apply(expr const & a, expr const & b) {
         if (is_eqp(a, b))          return true;

src/kernel/kernel_exception.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "runtime/interrupt.h"
 
 namespace lean {
 /** \brief Base class for all kernel exceptions. */
@@ -146,6 +145,21 @@ an `kernel_exception` or `exception`. Then, convert result into `Except KernelEx
 where `T` is the type of the lean objected represented by `A`.
 We use the constructor `KernelException.other <msg>` to handle C++ `exception` objects which
 are not `kernel_exception`.
+```
+inductive KernelException
+0  | unknownConstant  (env : Environment) (name : Name)
+1  | alreadyDeclared  (env : Environment) (name : Name)
+2  | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
+3  | declHasMVars     (env : Environment) (name : Name) (expr : Expr)
+4  | declHasFVars     (env : Environment) (name : Name) (expr : Expr)
+5  | funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
+6  | typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
+7  | letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
+8  | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
+9  | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
+10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+11 | other            (msg : String)
+```
 */
 template<typename A>
 object * catch_kernel_exceptions(std::function<A()> const & f) {
@@ -197,9 +211,6 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (stack_space_exception & ex) {
         // 14 | deepRecursion
         return mk_cnstr(0, box(14)).steal();
-    } catch (interrupted & ex) {
-        // 15 | interrupted
-        return mk_cnstr(0, box(15)).steal();
     }
 }
 }

src/kernel/type_checker.cpp

@@ -287,7 +287,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
         throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it");
 
     lean_assert(!has_loose_bvars(e));
-    check_system("type checker", /* do_check_interrupted */ true);
+    check_system("type checker");
 
     auto it = m_st->m_infer_type[infer_only].find(e);
     if (it != m_st->m_infer_type[infer_only].end())
@@ -410,7 +410,7 @@ static bool is_let_fvar(local_ctx const & lctx, expr const & e) {
     If `cheap == true`, then we don't perform delta-reduction when reducing major premise of recursors and projections.
     We also do not cache results. */
 expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
-    check_system("type checker: whnf", /* do_check_interrupted */ true);
+    check_system("type checker: whnf");
 
     // handle easy cases
     switch (e.kind()) {
@@ -1002,7 +1002,7 @@ bool type_checker::is_def_eq_unit_like(expr const & t, expr const & s) {
 }
 
 bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
-    check_system("is_definitionally_equal", /* do_check_interrupted */ true);
+    check_system("is_definitionally_equal");
     bool use_hash = true;
     lbool r = quick_is_def_eq(t, s, use_hash);
     if (r != l_undef) return r == l_true;

src/runtime/interrupt.cpp

@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "runtime/interrupt.h"
 #include "runtime/exception.h"
 #include "runtime/memory.h"
-#include "lean/lean.h"
 
 namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
@@ -39,17 +38,24 @@ void check_heartbeat() {
         throw_heartbeat_exception();
 }
 
+LEAN_THREAD_VALUE(atomic_bool *, g_interrupt_flag, nullptr);
+
+scoped_interrupt_flag::scoped_interrupt_flag(atomic_bool * flag) : flet(g_interrupt_flag, flag) {}
+
+static bool interrupt_requested() {
+    return g_interrupt_flag && g_interrupt_flag->load();
+}
+
 void check_interrupted() {
-    if (lean_io_check_canceled_core() && !std::uncaught_exception()) {
+    if (interrupt_requested() && !std::uncaught_exception()) {
         throw interrupted();
     }
 }
 
-void check_system(char const * component_name, bool do_check_interrupted) {
+void check_system(char const * component_name) {
     check_stack(component_name);
     check_memory(component_name);
-    if (do_check_interrupted)
-        check_interrupted();
+    check_interrupted();
     check_heartbeat();
 }
 
@@ -66,4 +72,17 @@ void sleep_for(unsigned ms, unsigned step_ms) {
     this_thread::sleep_for(r);
     check_interrupted();
 }
+
+bool interruptible_thread::interrupted() const {
+    return m_flag.load();
+}
+
+void interruptible_thread::request_interrupt() {
+    m_flag.store(true);
+}
+
+void interruptible_thread::join() {
+    m_thread.join();
+}
+
 }

src/runtime/interrupt.h

@@ -42,19 +42,19 @@ public:
 
 void check_heartbeat();
 
+struct scoped_interrupt_flag : flet<atomic_bool *> {
+    scoped_interrupt_flag(atomic_bool *); // NOLINT
+};
+
 /**
-   \brief Throw an interrupted exception if the current task is marked cancelled.
+   \brief Throw an interrupted exception if the (interrupt) flag is set.
 */
 void check_interrupted();
 
 /**
    \brief Check system resources: stack, memory, heartbeat, interrupt flag.
-
-   `do_check_interrupted` should only be set to `true` in places where a C++ exception
-   is caught and would not bring down the entire process as interruption
-   should not be a fatal error.
 */
-void check_system(char const * component_name, bool do_check_interrupted = false);
+void check_system(char const * component_name);
 
 constexpr unsigned g_small_sleep = 10;
 
@@ -65,4 +65,42 @@ constexpr unsigned g_small_sleep = 10;
 */
 void sleep_for(unsigned ms, unsigned step_ms = g_small_sleep);
 inline void sleep_for(chrono::milliseconds const & ms) { sleep_for(ms.count(), 10); }
+
+/**
+   \brief Thread that provides a method for setting its interrupt flag.
+*/
+class interruptible_thread {
+public:
+    template<typename Function>
+    interruptible_thread(Function && fun):
+        m_thread([&, fun]() {
+                save_stack_info(false);
+                scoped_interrupt_flag scope_int_flag(&m_flag);
+                fun();
+            })
+        {}
+
+    /**
+       \brief Return true iff an interrupt request has been made to the current thread.
+    */
+    bool interrupted() const;
+    /**
+       \brief Send a interrupt request to the current thread. Return
+       true iff the request has been successfully performed.
+    */
+    void request_interrupt();
+
+    void join();
+private:
+    atomic_bool m_flag;
+    lthread m_thread;
+};
+
+#if !defined(LEAN_MULTI_THREAD)
+inline void check_threadsafe() {
+    throw exception("Lean was compiled without support for multi-threading");
+}
+#else
+inline void check_threadsafe() {}
+#endif
 }