From fb0d0245db9bcb9ff649794f57522c52cb80c993 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 17 Oct 2023 11:59:11 +1100 Subject: [PATCH] Revert "Cancel outstanding tasks on document edit in the language server" (#2703) * Revert "perf: inline `checkInterrupted`" This reverts commit 6494af4513da28b13f3e3175e4cf59e24ad05dc8. * Revert "fix: switch to C++ interruption whitelist" This reverts commit 5aae74199b6cc2eb01619f0eaa04285c76cd388d. * Revert "fix: do not throw interrupt exceptions inside pure functions" This reverts commit c0e3b9568e92cea8cf1c07ff911da78462c0ed57. * Revert "feat: cancel tasks on document edit" This reverts commit a2e2481c51e12166dc1163ff7b8e27613c4ebaea. * Revert "feat: translate `interrupted` kernel exception" This reverts commit 14c640c15e30c19c3c196afe38347b278ff34b13. * Revert "feat: check task cancellation in elaborator" This reverts commit 2070df2328397abd3552e2e44f33d6e4c20afac7. * Revert "feat: move `check_interrupted` from unused thread class to `Task` cancellation" This reverts commit bf48a18cf9d4d1be2063a2af091520756a992156. --- src/Lean/CoreM.lean | 12 +---- src/Lean/Elab/Do.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Environment.lean | 1 - src/Lean/Message.lean | 1 - src/Lean/Meta/ExprDefEq.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 5 +- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- src/Lean/Meta/WHNF.lean | 2 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 2 +- src/Lean/Server/AsyncList.lean | 14 ------ src/Lean/Server/FileWorker.lean | 2 - src/kernel/expr_eq_fn.cpp | 4 +- src/kernel/kernel_exception.h | 19 +++++-- src/kernel/type_checker.cpp | 6 +-- src/runtime/interrupt.cpp | 29 +++++++++-- src/runtime/interrupt.h | 50 ++++++++++++++++--- 18 files changed, 97 insertions(+), 60 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index ce19929d3a..c38191e82f 100644 --- a/src/Lean/CoreM.lean +++ b/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} ' 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 }) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 85392b5d38..3865223498 100644 --- a/src/Lean/Elab/Do.lean +++ b/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 => diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 778d599a8a..e2d699aa31 100644 --- a/src/Lean/Elab/Term.lean +++ b/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?) => diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index c81573aa63..8fb7da9258 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -230,7 +230,6 @@ inductive KernelException where | deterministicTimeout | excessiveMemory | deepRecursion - | interrupted namespace Environment diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 459873e4d2..cfb3508279 100644 --- a/src/Lean/Message.lean +++ b/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 diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 4aa501b0bc..ad4eb4cc47 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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 /- diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 0a315f985f..15f2bcc61a 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 08c1c03a89..4fca5307a0 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/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 } diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index baab851203..62fc0779ee 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/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' diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index f557f93e98..2e1ebeb6ad 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index c62292de3a..ee89be8e30 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/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 diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean index dc4abbc688..5da2648899 100644 --- a/src/Lean/Server/AsyncList.lean +++ b/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 diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index b7e7910b04..d9b7ab33f2 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/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) diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 647bbec2d3..d3942470d6 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -60,9 +60,7 @@ template 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; diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 930185828f..f5d66133ee 100644 --- a/src/kernel/kernel_exception.h +++ b/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 ` 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 object * catch_kernel_exceptions(std::function const & f) { @@ -197,9 +211,6 @@ object * catch_kernel_exceptions(std::function 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(); } } } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 4c8d8f2d60..42decd8f8b 100644 --- a/src/kernel/type_checker.cpp +++ b/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; diff --git a/src/runtime/interrupt.cpp b/src/runtime/interrupt.cpp index 0bc31d0738..f3bbb2d421 100644 --- a/src/runtime/interrupt.cpp +++ b/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(); +} + } diff --git a/src/runtime/interrupt.h b/src/runtime/interrupt.h index 4e628fb511..a01a539404 100644 --- a/src/runtime/interrupt.h +++ b/src/runtime/interrupt.h @@ -42,19 +42,19 @@ public: void check_heartbeat(); +struct scoped_interrupt_flag : flet { + 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 + 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 }