question: why wait for initialized is needed here?
#3904
Comments
|
Thanks for the bug report. We should probably just send the watcher requests after the initialization dance is done so that this race condition cannot occur. |
github-merge-queue bot
pushed a commit
that referenced
this issue
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]>
github-actions bot
pushed a commit
that referenced
this issue
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)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
See
lean4/src/Lean/Server/Watchdog.lean
Line 1047 in 1c20b53
in some async language server implementation, for example, async-lsp, client may response the
register_lean_watcherrequest (register_ilean_watcher) before sendinginitializednotification. So the client side router should take care of the sequence of messages, first sendinginitialized, then response theregister_lean_watcherThe text was updated successfully, but these errors were encountered: