fix: inlay hint race conditions (#7188)
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.
This commit is contained in:
Marc Huisinga
GitHub
parent
647573d269
commit
a7bdc55244
5 changed files with 101 additions and 93 deletions
|
|
@ -104,7 +104,7 @@ where
|
|||
let tasks : { t : List _ // t.length > 0 } :=
|
||||
match cancelTk? with
|
||||
| none => ⟨[tl, timeoutTask], by exact Nat.zero_lt_succ _⟩
|
||||
| some cancelTk => ⟨[cancelTk, tl, timeoutTask], by exact Nat.zero_lt_succ _⟩
|
||||
| some cancelTk => ⟨[tl, cancelTk, timeoutTask], by exact Nat.zero_lt_succ _⟩
|
||||
let r ← ServerTask.waitAny tasks.val (h := tasks.property)
|
||||
match r with
|
||||
| .inl _ => return ⟨[], none, false⟩ -- Timeout or cancellation - stop waiting
|
||||
|
|
|
|||
|
|
@ -534,22 +534,21 @@ section NotificationHandling
|
|||
let oldDoc := (←get).doc
|
||||
let cancelTk ← RequestCancellationToken.new
|
||||
let newVersion := docId.version?.getD 0
|
||||
let _ ← ServerTask.IO.mapTaskCostly (t := st.srcSearchPathTask) fun srcSearchPath =>
|
||||
let rc : RequestContext :=
|
||||
{ rpcSessions := st.rpcSessions
|
||||
srcSearchPath
|
||||
doc := oldDoc
|
||||
cancelTk
|
||||
hLog := ctx.hLog
|
||||
initParams := ctx.initParams }
|
||||
RequestM.runInIO (handleOnDidChange p) rc
|
||||
let rc : RequestContext := {
|
||||
rpcSessions := st.rpcSessions
|
||||
srcSearchPathTask := st.srcSearchPathTask
|
||||
doc := oldDoc
|
||||
cancelTk
|
||||
hLog := ctx.hLog
|
||||
initParams := ctx.initParams
|
||||
}
|
||||
RequestM.runInIO (handleOnDidChange p) rc
|
||||
if ¬ changes.isEmpty then
|
||||
let newDocText := foldDocumentChanges changes oldDoc.meta.text
|
||||
updateDocument ⟨docId.uri, newVersion, newDocText, oldDoc.meta.dependencyBuildMode⟩
|
||||
for (_, r) in st.pendingRequests do
|
||||
r.cancelTk.cancelByEdit
|
||||
|
||||
|
||||
def handleCancelRequest (p : CancelParams) : WorkerM Unit := do
|
||||
let st ← get
|
||||
let some r := st.pendingRequests.find? p.id
|
||||
|
|
@ -728,32 +727,30 @@ section MessageHandling
|
|||
return
|
||||
|
||||
let cancelTk ← RequestCancellationToken.new
|
||||
-- we assume that any other request requires at least the search path
|
||||
-- TODO: move into language-specific request handling
|
||||
let requestTask ← ServerTask.IO.bindTaskCheap st.srcSearchPathTask fun srcSearchPath => do
|
||||
let rc : RequestContext :=
|
||||
{ rpcSessions := st.rpcSessions
|
||||
srcSearchPath
|
||||
doc := st.doc
|
||||
cancelTk
|
||||
hLog := ctx.hLog
|
||||
initParams := ctx.initParams }
|
||||
let t? ← EIO.toIO' <| handleLspRequest method params rc
|
||||
match t? with
|
||||
let rc : RequestContext :=
|
||||
{ rpcSessions := st.rpcSessions
|
||||
srcSearchPathTask := st.srcSearchPathTask
|
||||
doc := st.doc
|
||||
cancelTk
|
||||
hLog := ctx.hLog
|
||||
initParams := ctx.initParams }
|
||||
let requestTask? ← EIO.toIO' <| handleLspRequest method params rc
|
||||
let requestTask ← match requestTask? with
|
||||
| Except.error e =>
|
||||
emitResponse ctx (isComplete := false) <| e.toLspResponseError id
|
||||
pure <| ServerTask.pure <| .ok ()
|
||||
| Except.ok requestTask => ServerTask.IO.mapTaskCheap (t := requestTask) fun
|
||||
| Except.ok r => do
|
||||
if ← cancelTk.wasCancelledByCancelRequest then
|
||||
-- Try not to emit a partial response if this request was cancelled.
|
||||
-- Clients usually discard responses for requests that they cancelled anyways,
|
||||
-- but it's still good to send less over the wire in this case.
|
||||
emitResponse ctx (isComplete := false) <| RequestError.requestCancelled.toLspResponseError id
|
||||
return
|
||||
emitResponse ctx (isComplete := r.isComplete) <| .response id (toJson r.response)
|
||||
| Except.error e =>
|
||||
emitResponse ctx (isComplete := false) <| e.toLspResponseError id
|
||||
pure <| ServerTask.pure <| .ok ()
|
||||
| Except.ok t => ServerTask.IO.mapTaskCheap (t := t) fun
|
||||
| Except.ok r => do
|
||||
if ← cancelTk.wasCancelledByCancelRequest then
|
||||
-- Try not to emit a partial response if this request was cancelled.
|
||||
-- Clients usually discard responses for requests that they cancelled anyways,
|
||||
-- but it's still good to send less over the wire in this case.
|
||||
emitResponse ctx (isComplete := false) <| RequestError.requestCancelled.toLspResponseError id
|
||||
return
|
||||
emitResponse ctx (isComplete := r.isComplete) <| .response id (toJson r.response)
|
||||
| Except.error e =>
|
||||
emitResponse ctx (isComplete := false) <| e.toLspResponseError id
|
||||
emitResponse ctx (isComplete := false) <| e.toLspResponseError id
|
||||
queueRequest id { cancelTk, requestTask }
|
||||
|
||||
where
|
||||
|
|
|
|||
|
|
@ -126,12 +126,10 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
|
|||
let timeSinceLastEditMs := timestamp - lastEditTimestamp
|
||||
inlayHintEditDelayMs - timeSinceLastEditMs
|
||||
let (snaps, _, isComplete) ← ctx.doc.cmdSnaps.getFinishedPrefixWithConsistentLatency editDelayMs.toUInt32 (cancelTk? := ctx.cancelTk.cancellationTask)
|
||||
-- This cancellation check is crucial for the invariant `finishedSnaps >= oldFinishedSnaps` below.
|
||||
RequestM.checkCancelled
|
||||
let snaps := snaps.toArray
|
||||
let finishedSnaps := snaps.size
|
||||
let oldFinishedSnaps := s.oldFinishedSnaps
|
||||
-- File processing is monotonic modulo `didChange` notifications and cancellation.
|
||||
-- File processing is monotonic modulo `didChange` notifications.
|
||||
assert! finishedSnaps >= oldFinishedSnaps
|
||||
-- VS Code emits inlay hint requests *every time the user scrolls*. This is reasonably expensive,
|
||||
-- so in addition to re-using old inlay hints from parts of the file that haven't been processed
|
||||
|
|
@ -165,55 +163,65 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
|
|||
|
||||
def handleInlayHintsDidChange (p : DidChangeTextDocumentParams)
|
||||
: StateT InlayHintState RequestM Unit := do
|
||||
let meta := (← read).doc.meta
|
||||
let text := meta.text
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let .ok modName? ← EIO.toBaseIO <| do
|
||||
let some path := System.Uri.fileUriToPath? meta.uri
|
||||
| return none
|
||||
let some mod ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return some <| ← moduleNameOfFileName path none
|
||||
return some mod
|
||||
| return
|
||||
let modName := modName?.getD .anonymous -- `.anonymous` occurs in untitled files
|
||||
let s ← get
|
||||
let mut updatedOldInlayHints := #[]
|
||||
for ihi in s.oldInlayHints do
|
||||
let mut ihi := ihi
|
||||
let mut inlayHintInvalidated := false
|
||||
for c in p.contentChanges do
|
||||
let .rangeChange changeRange newText := c
|
||||
| set <| { s with oldInlayHints := #[] } -- `fullChange` => all old inlay hints invalidated
|
||||
return
|
||||
let changeRange := text.lspRangeToUtf8Range changeRange
|
||||
let some ihi' := applyEditToHint? modName ihi changeRange newText
|
||||
| -- Change in some position of inlay hint => inlay hint invalidated
|
||||
inlayHintInvalidated := true
|
||||
break
|
||||
ihi := ihi'
|
||||
if ! inlayHintInvalidated then
|
||||
updatedOldInlayHints := updatedOldInlayHints.push ihi
|
||||
let isInlayHintInsertionEdit := p.contentChanges.all fun c => Id.run do
|
||||
let .rangeChange changeRange newText := c
|
||||
| return false
|
||||
let changeRange := text.lspRangeToUtf8Range changeRange
|
||||
let edit := ⟨changeRange, newText⟩
|
||||
return s.oldInlayHints.any (·.textEdits.contains edit)
|
||||
let timestamp ← IO.monoMsNow
|
||||
let lastEditTimestamp? :=
|
||||
if isInlayHintInsertionEdit then
|
||||
-- For some stupid reason, VS Code doesn't remove the inlay hint when applying it, so we
|
||||
-- try to figure out whether the edit was an insertion of an inlay hint and then respond
|
||||
-- to the request without latency so that it inserted ASAP.
|
||||
none
|
||||
else
|
||||
some timestamp
|
||||
let updatedOldInlayHints ← updateOldInlayHints s.oldInlayHints
|
||||
let lastEditTimestamp? ← determineLastEditTimestamp? s.oldInlayHints
|
||||
set <| { s with
|
||||
oldInlayHints := updatedOldInlayHints
|
||||
oldFinishedSnaps := 0
|
||||
lastEditTimestamp?
|
||||
}
|
||||
|
||||
where
|
||||
|
||||
updateOldInlayHints (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Array Elab.InlayHintInfo) := do
|
||||
let meta := (← read).doc.meta
|
||||
let text := meta.text
|
||||
let srcSearchPath := (← read).srcSearchPath
|
||||
let modName? ← EIO.toBaseIO <| do
|
||||
let some path := System.Uri.fileUriToPath? meta.uri
|
||||
| return none
|
||||
let some mod ← searchModuleNameOfFileName path srcSearchPath
|
||||
| return some <| ← moduleNameOfFileName path none
|
||||
return some mod
|
||||
let modName ← match modName? with
|
||||
| .ok (some modName) => pure modName
|
||||
| .ok none => pure .anonymous -- `.anonymous` occurs in untitled files
|
||||
| .error err => throw <| .ofIoError err
|
||||
let mut updatedOldInlayHints := #[]
|
||||
for ihi in oldInlayHints do
|
||||
let mut ihi := ihi
|
||||
let mut inlayHintInvalidated := false
|
||||
for c in p.contentChanges do
|
||||
let .rangeChange changeRange newText := c
|
||||
| return #[] -- `fullChange` => all old inlay hints invalidated
|
||||
let changeRange := text.lspRangeToUtf8Range changeRange
|
||||
let some ihi' := applyEditToHint? modName ihi changeRange newText
|
||||
| -- Change in some position of inlay hint => inlay hint invalidated
|
||||
inlayHintInvalidated := true
|
||||
break
|
||||
ihi := ihi'
|
||||
if ! inlayHintInvalidated then
|
||||
updatedOldInlayHints := updatedOldInlayHints.push ihi
|
||||
return updatedOldInlayHints
|
||||
|
||||
determineLastEditTimestamp? (oldInlayHints : Array Elab.InlayHintInfo) : RequestM (Option Nat) := do
|
||||
let text := (← read).doc.meta.text
|
||||
let isInlayHintInsertionEdit := p.contentChanges.all fun c => Id.run do
|
||||
let .rangeChange changeRange newText := c
|
||||
| return false
|
||||
let changeRange := text.lspRangeToUtf8Range changeRange
|
||||
let edit := ⟨changeRange, newText⟩
|
||||
return oldInlayHints.any (·.textEdits.contains edit)
|
||||
let timestamp ← IO.monoMsNow
|
||||
if isInlayHintInsertionEdit then
|
||||
-- For some stupid reason, VS Code doesn't remove the inlay hint when applying it, so we
|
||||
-- try to figure out whether the edit was an insertion of an inlay hint and then respond
|
||||
-- to the request without latency so that it inserted ASAP.
|
||||
return none
|
||||
else
|
||||
return some timestamp
|
||||
|
||||
builtin_initialize
|
||||
registerPartialStatefulLspRequestHandler
|
||||
"textDocument/inlayHint"
|
||||
|
|
|
|||
|
|
@ -15,28 +15,28 @@ structure RequestCancellationToken where
|
|||
|
||||
namespace RequestCancellationToken
|
||||
|
||||
def new : IO RequestCancellationToken := do
|
||||
def new : BaseIO RequestCancellationToken := do
|
||||
return {
|
||||
cancelledByCancelRequest := ← IO.mkRef false
|
||||
cancelledByEdit := ← IO.mkRef false
|
||||
cancellationPromise := ← IO.Promise.new
|
||||
}
|
||||
|
||||
def cancelByCancelRequest (tk : RequestCancellationToken) : IO Unit := do
|
||||
def cancelByCancelRequest (tk : RequestCancellationToken) : BaseIO Unit := do
|
||||
tk.cancelledByCancelRequest.set true
|
||||
tk.cancellationPromise.resolve ()
|
||||
|
||||
def cancelByEdit (tk : RequestCancellationToken) : IO Unit := do
|
||||
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) : IO Bool :=
|
||||
def wasCancelledByCancelRequest (tk : RequestCancellationToken) : BaseIO Bool :=
|
||||
tk.cancelledByCancelRequest.get
|
||||
|
||||
def wasCancelledByEdit (tk : RequestCancellationToken) : IO Bool := do
|
||||
def wasCancelledByEdit (tk : RequestCancellationToken) : BaseIO Bool := do
|
||||
tk.cancelledByEdit.get
|
||||
|
||||
end RequestCancellationToken
|
||||
|
|
@ -56,7 +56,7 @@ def CancellableM.run (tk : RequestCancellationToken) (x : CancellableM α) :
|
|||
IO (Except RequestCancellation α) :=
|
||||
CancellableT.run tk x
|
||||
|
||||
def CancellableT.checkCancelled [Monad m] [MonadLiftT IO m] : CancellableT m Unit := do
|
||||
def CancellableT.checkCancelled [Monad m] [MonadLiftT BaseIO m] : CancellableT m Unit := do
|
||||
let tk ← read
|
||||
if ← tk.wasCancelledByCancelRequest then
|
||||
throw .requestCancelled
|
||||
|
|
@ -70,7 +70,7 @@ class MonadCancellable (m : Type → Type v) where
|
|||
instance (m n) [MonadLift m n] [MonadCancellable m] : MonadCancellable n where
|
||||
checkCancelled := liftM (MonadCancellable.checkCancelled : m PUnit)
|
||||
|
||||
instance [Monad m] [MonadLiftT IO m] : MonadCancellable (CancellableT m) where
|
||||
instance [Monad m] [MonadLiftT BaseIO m] : MonadCancellable (CancellableT m) where
|
||||
checkCancelled := CancellableT.checkCancelled
|
||||
|
||||
def RequestCancellation.check [MonadCancellable m] : m Unit :=
|
||||
|
|
|
|||
|
|
@ -137,12 +137,15 @@ def parseRequestParams (paramType : Type) [FromJson paramType] (params : Json)
|
|||
message := s!"Cannot parse request params: {params.compress}\n{inner}" }
|
||||
|
||||
structure RequestContext where
|
||||
rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare
|
||||
srcSearchPath : SearchPath
|
||||
doc : FileWorker.EditableDocument
|
||||
hLog : IO.FS.Stream
|
||||
initParams : Lsp.InitializeParams
|
||||
cancelTk : RequestCancellationToken
|
||||
rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare
|
||||
srcSearchPathTask : ServerTask SearchPath
|
||||
doc : FileWorker.EditableDocument
|
||||
hLog : IO.FS.Stream
|
||||
initParams : Lsp.InitializeParams
|
||||
cancelTk : RequestCancellationToken
|
||||
|
||||
def RequestContext.srcSearchPath (rc : RequestContext) : SearchPath :=
|
||||
rc.srcSearchPathTask.get
|
||||
|
||||
abbrev RequestTask α := ServerTask (Except RequestError α)
|
||||
abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue