VSCode extension runs into infinite leanpkg spawning loop on Ctrl+hover #367
Comments
|
It turns out the/a root cause is that VS Code will send a @gebner Any ideas? 🙏 |
|
I've been playing around with this issue for a while now, so I'd like to provide some additional context.
One possible (server-sided) solution would be to simply ignore |
|
I believe sending didOpen/didClose is intentional, but sending them on repeat is not. I can reproduce the issue, I'll see if I can hack up some workaround. |
I just noticed that this is just because I use Ctrl+X to delete |
|
I believe the endless repeat of didOpen/didClose is due to our |
|
Can you try out leanprover/vscode-lean4#17? |
|
I cannot reproduce the issue anymore with that PR. |
|
That fixes the problem for me as well. Many thanks! |
ChrisHughes24
pushed a commit
to ChrisHughes24/lean4
that referenced
this issue
Dec 2, 2022
mhuisi
added a commit
to leanprover/vscode-lean4
that referenced
this issue
Jun 4, 2024
This PR fixes an issue reported at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/VSCODE.20outline.20mode.20not.20working.20in.20imports/near/442000461 that caused the VS Code outline and other features that rely on document symbols to not display anything when initially opening the document. The synopsis is as follows (in case anyone stumbles upon related issues in the future): 1. By default, VS Code triggers `onDidOpenTextDocument` when hovering over an identifier while holding `Ctrl`, which in turn makes the language client library emit a `didOpen` notification to the language server (closely followed by `didClose` when moving the mouse away from the identifier). 2. This puts unnecessary pressure on the language server since it starts elaborating the file, especially given that VS Code does not emit any further requests in this situation. microsoft/vscode#78453 leanprover/lean4#367 3. Hence, [it was suggested](microsoft/vscode#78453 (comment)) to filter these notifications in the language client middleware by only sending these notifications for `window.visibleTextEditors`, which does not contain "synthetic" documents like the one opened in the `Ctrl` hover. 4. This doesn't work because `window.visibleTextEditors` is not up-to-date yet when the corresponding `onDidOpenTextDocument` handler is executed. 5. To work around this, #17 filtered all `didOpen` notifications emitted by the client and registered its own handler to emit these notifications. This handler was executed *after* `window.visibleTextEditors` had been updated and so could use `window.visibleTextEditors` to decide for which files `didOpen` should be emitted. See microsoft/vscode-languageserver-node#848 for the currently still open issue to properly fix this in the language client library. 6. This worked fine until we added language server support for requests that are commonly emitted right after the file is opened (e.g. document symbols). 7. Since the language client registers its own handlers for emitting requests and vscode-lean4 manages `didOpen` notifications, there's now the potential for a race condition: If the handlers from different sources are called in the wrong order and a file is opened after a request is emitted, the language server may respond to the request with an error since it doesn't know about the document yet. 8. VS Code does not frequently issue these requests if the file doesn't change, so the empty state sticks around until the document is changed (or even longer for some requests). 9. This causes an empty document symbols view when initially opening the document, which is especially critical when using 'Go to Definition'. In VS Code version 1.67 (long after the initial vscode-lean4 work-around for this issue), a new `window.tabGroups` API was added that allows querying all documents that are currently open in VS Code tabs. `window.tabGroups` is fortunately already up-to-date when `onDidOpenTextDocument` is called, so we can now use this information to directly filter the `didOpen` notifications in the language client middleware without registering our own handler that introduces a race condition. This fixes the bug. One strange thing I noticed while debugging this issue is that VS Code actually emits multiple requests of the same kind when the document is first opened. One of these typically fails because the document is not open yet whereas the second one typically succeeds. But for some reason (I suspect a bug), VS Code does not actually end up using the result of the successful request in this case. This lead to a very confusing situation during debugging where both the language server and the language client library seemed to return a correct result, but VS Code still produced an empty outline. I also suspect that this issue is one cause of other non-deterministic issues that we have previously encountered in the language server. For example, while we already fixed this issue using other means, the non-deterministic behavior of semantic highlighting sometimes being broken (leanprover/lean4#2977) may also have been partially caused by this as VS Code queries the semantic tokens for the full document right after opening the document as well and only rarely re-queries them afterwards. This PR also replaces our own tracking of documents opened in the language server with the open documents tracked by the language client library. I suspect that the language client library has a bug here (the set of `openDocuments` in the language client library will probably also contain documents that were filtered in the `didOpen` middleware if the document was opened while starting the client), but it shouldn't affect us as we only filter `didOpen` notifications for documents that can only be opened after the language client was already launched.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Description
In the Lean 4 VSCode extension, holding Ctrl and hovering over a term that references a definition frequently causes lots of
leanpkgprocesses being started, apparently in an infinite loop, consuming all CPU and grinding the system to a halt.With the given steps I can reliably reproduce it on Ubuntu 20.04.
Steps to Reproduce
def Test := Truein an empty.leanfile.True. (Note: Ctrl+clicking very quickly actually avoids the issue.)Expected behavior:
Trueshould be underlined (for Ctrl+click) but this shouldn't cause any harm.Actual behavior:
Trueis underlined correctly and everything appears to work normally for a moment, but in the background two things happen:leanpkg print-pathsprocesses are spawned in a loop until I close VSCode. Depending on the complexity of the file/project, these processes accumulate because they are started faster than they can finish, though in this small example this doesn't happen and there are always just one or two such processes.Reproduces how often: Always.
Versions
Lean (version 4.0.0-nightly-2021-03-22, commit 19b24e3, Release)
Ubuntu 20.04.2 LTS (x64)
The text was updated successfully, but these errors were encountered: