a7bdc55244
This PR fixes several inlay hint race conditions that could result in a violation of the monotonic progress assumption, introduced in #7149. Specifically: - In rare circumstances, it could happen that stateful LSP requests were executed out-of-order with their `didChange` handlers, as both requests and the `didChange` handlers waited on `lake setup-file` to complete, with the latter running those handlers in a dedicated task afterwards. This meant that a request could be added to the stateful LSP handler request queue before the corresponding `didChange` call that actually came before it. This PR resolves this issue by folding the task that waits for `lake setup-file` into the `RequestContext`, which ensures that we only need to wait for it when actually executing the request handler. - While #7164 fixed the monotonic progress assertion violation that was caused by `$/cancelRequest`, it did not account for our internal notion of silent request cancellation in stateful LSP requests, which we use to cancel the inlay hint edit delay when VS Code fails to emit a `$/cancelRequest` notification. This issue is resolved by always producing the full finished prefix of the command snapshot queue, even on cancellation. Additionally, this also fixes an issue where in the same circumstances, the language server could produce an empty inlay hint response when a request was cancelled by our internal notion of silent request cancellation. - For clients that use `fullChange` `didChange` notifications (e.g. not VS Code), we would get several aspects of stateful LSP request `didChange` state handling wrong, which is also addressed by this PR.
77 lines
2.5 KiB
Text
77 lines
2.5 KiB
Text
/-
|
||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Marc Huisinga
|
||
-/
|
||
prelude
|
||
import Init.System.Promise
|
||
|
||
namespace Lean.Server
|
||
|
||
structure RequestCancellationToken where
|
||
cancelledByCancelRequest : IO.Ref Bool
|
||
cancelledByEdit : IO.Ref Bool
|
||
cancellationPromise : IO.Promise Unit
|
||
|
||
namespace RequestCancellationToken
|
||
|
||
def new : BaseIO RequestCancellationToken := do
|
||
return {
|
||
cancelledByCancelRequest := ← IO.mkRef false
|
||
cancelledByEdit := ← IO.mkRef false
|
||
cancellationPromise := ← IO.Promise.new
|
||
}
|
||
|
||
def cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit := do
|
||
tk.cancelledByCancelRequest.set true
|
||
tk.cancellationPromise.resolve ()
|
||
|
||
def cancelByEdit (tk : RequestCancellationToken) : BaseIO Unit := do
|
||
tk.cancelledByEdit.set true
|
||
tk.cancellationPromise.resolve ()
|
||
|
||
def cancellationTask (tk : RequestCancellationToken) : Task Unit :=
|
||
tk.cancellationPromise.result!
|
||
|
||
def wasCancelledByCancelRequest (tk : RequestCancellationToken) : BaseIO Bool :=
|
||
tk.cancelledByCancelRequest.get
|
||
|
||
def wasCancelledByEdit (tk : RequestCancellationToken) : BaseIO Bool := do
|
||
tk.cancelledByEdit.get
|
||
|
||
end RequestCancellationToken
|
||
|
||
structure RequestCancellation where
|
||
|
||
def RequestCancellation.requestCancelled : RequestCancellation := {}
|
||
|
||
abbrev CancellableT m := ReaderT RequestCancellationToken (ExceptT RequestCancellation m)
|
||
abbrev CancellableM := CancellableT IO
|
||
|
||
def CancellableT.run (tk : RequestCancellationToken) (x : CancellableT m α) :
|
||
m (Except RequestCancellation α) :=
|
||
x tk
|
||
|
||
def CancellableM.run (tk : RequestCancellationToken) (x : CancellableM α) :
|
||
IO (Except RequestCancellation α) :=
|
||
CancellableT.run tk x
|
||
|
||
def CancellableT.checkCancelled [Monad m] [MonadLiftT BaseIO m] : CancellableT m Unit := do
|
||
let tk ← read
|
||
if ← tk.wasCancelledByCancelRequest then
|
||
throw .requestCancelled
|
||
|
||
def CancellableM.checkCancelled : CancellableM Unit :=
|
||
CancellableT.checkCancelled
|
||
|
||
class MonadCancellable (m : Type → Type v) where
|
||
checkCancelled : m PUnit
|
||
|
||
instance (m n) [MonadLift m n] [MonadCancellable m] : MonadCancellable n where
|
||
checkCancelled := liftM (MonadCancellable.checkCancelled : m PUnit)
|
||
|
||
instance [Monad m] [MonadLiftT BaseIO m] : MonadCancellable (CancellableT m) where
|
||
checkCancelled := CancellableT.checkCancelled
|
||
|
||
def RequestCancellation.check [MonadCancellable m] : m Unit :=
|
||
MonadCancellable.checkCancelled
|