feat: fast path for inlay hints #7149
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
github-merge-queue bot
pushed a commit
that referenced
this pull request
Feb 20, 2025
This PR fixes an assertion violation introduced in #7149 where the monotonic progress assumption was violated by request cancellation.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Feb 22, 2025
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.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 24, 2025
This PR adds a fast path to the inlay hint request that makes it re-use already computed inlay hints from previous requests instead of re-computing them. This is necessary because for some reason VS Code emits an inlay hint request for every line you scroll, so we need to be able to respond to these requests against the same document state quickly. Otherwise, every single scrolled line would result in a request that can take a few dozen ms to be responded to in long files, putting unnecessary pressure on the CPU. It also filters the result set by the inlay hints that have been requested.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 24, 2025
This PR fixes an assertion violation introduced in leanprover#7149 where the monotonic progress assumption was violated by request cancellation.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 24, 2025
This PR fixes several inlay hint race conditions that could result in a violation of the monotonic progress assumption, introduced in leanprover#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 leanprover#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.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 25, 2025
This PR adds a fast path to the inlay hint request that makes it re-use already computed inlay hints from previous requests instead of re-computing them. This is necessary because for some reason VS Code emits an inlay hint request for every line you scroll, so we need to be able to respond to these requests against the same document state quickly. Otherwise, every single scrolled line would result in a request that can take a few dozen ms to be responded to in long files, putting unnecessary pressure on the CPU. It also filters the result set by the inlay hints that have been requested.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 25, 2025
This PR fixes an assertion violation introduced in leanprover#7149 where the monotonic progress assumption was violated by request cancellation.
luisacicolini
pushed a commit
to opencompl/lean4
that referenced
this pull request
Feb 25, 2025
This PR fixes several inlay hint race conditions that could result in a violation of the monotonic progress assumption, introduced in leanprover#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 leanprover#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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a fast path to the inlay hint request that makes it re-use already computed inlay hints from previous requests instead of re-computing them. This is necessary because for some reason VS Code emits an inlay hint request for every line you scroll, so we need to be able to respond to these requests against the same document state quickly. Otherwise, every single scrolled line would result in a request that can take a few dozen ms to be responded to in long files, putting unnecessary pressure on the CPU.
It also filters the result set by the inlay hints that have been requested.