-
Notifications
You must be signed in to change notification settings - Fork 444
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: make watchdog more resilient against badly behaving clients #4443
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
mhuisi
force-pushed
the
mhuisi/resilient-watchdog
branch
from
June 13, 2024 12:19
b79a9e2
to
aec48f4
Compare
github-actions
bot
added
the
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
label
Jun 13, 2024
Mathlib CI status (docs):
|
…/lean4 into mhuisi/resilient-watchdog
github-actions bot
pushed a commit
that referenced
this pull request
Jun 13, 2024
This PR addresses some non-critical but annoying issues that sometimes cause the language server to report an error: - When using global search and replace in VS Code, the language client sends `textDocument/didChange` notifications for documents that it never told the server to open first. Instead of emitting an error and crashing the language server when this occurs, we now instead ignore the notification. Fixes #4435. - When terminating the language server, VS Code sometimes still sends request to the language server even after emitting a `shutdown` request. The LSP spec explicitly forbids this, but instead of emitting an error when this occurs, we now error requests and ignore all other messages until receiving the final `exit` notification. Reported on Zulip several times over the years but never materialized as an issue, e.g. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Got.20.60shutdown.60.20request.2C.20expected.20an.20.60exit.60.20notification/near/441914289. - Some language clients attempt to reply to the file watcher registration request before completing the LSP initialization dance. To fix this, we now only send this request after the initialization dance has completed. Fixes #3904. --------- Co-authored-by: Sebastian Ullrich <[email protected]> (cherry picked from commit 3119fd0)
Kha
pushed a commit
that referenced
this pull request
Jun 13, 2024
…badly behaving clients (#4445) Backport 3119fd0 from #4443. Co-authored-by: Marc Huisinga <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
backport releases/v4.9.0
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
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 addresses some non-critical but annoying issues that sometimes cause the language server to report an error:
textDocument/didChange
notifications for documents that it never told the server to open first. Instead of emitting an error and crashing the language server when this occurs, we now instead ignore the notification. Fixes search and replace across files crashes server #4435.shutdown
request. The LSP spec explicitly forbids this, but instead of emitting an error when this occurs, we now error requests and ignore all other messages until receiving the finalexit
notification. Reported on Zulip several times over the years but never materialized as an issue, e.g. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Got.20.60shutdown.60.20request.2C.20expected.20an.20.60exit.60.20notification/near/441914289.initialized
is needed here? #3904.