-
Notifications
You must be signed in to change notification settings - Fork 337
New issue
Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? # to your account
Add options to only sync visible documents to the server #848
Comments
I am very reluctant to sync UI state to the server. We really tried hard to not do this. I do see the problem with the diagnostics and the problem there is that it is a pure push model. So there are discussion to allow a pull model as well where this again would go back under the control of the editor. See microsoft/language-server-protocol#737 And even using VS Code visible editor will not help since there is no API for the tab model (e.g. you don't want to see lint errors disappear for editors for which there is still an open tab). Any objection to fold this with microsoft/language-server-protocol#737 |
In Dart the server has a concept of "priority files". That means if there are multiple outstanding requests for multiple files, those that are marked priority are processed first. These are intended to be set to the visible (or at least open) files. Without allowing the server to know what files the user has open (or visible), this isn't possible (currently for non-LSP we use visible files and it works great - for LSP we have to use "open" files which is a bit wonky).
This seems like it would increase server resources (especially if more things move to this model). Servers will have to start caching more data (or re-computing it frequently) if the client can ask for it at any time. The client is already caching it to show it in its UI - having the server able to tell the client when it changes feels like a better model to me. That said - I'm not sure how it solves this issue. How does the server know whether to include the "excluded" file when the client asks for all diagnostics? (I'm assuming the client would ask for all, and not individually for each open file - as that would just lead to a lot of complaints - see microsoft/vscode#13953).
Errors disappearing (for excluded files) when you tab to another file is a lot more understandable than randomly vanishing up to 3 minutes later (and perhaps even appearing when you don't have the file open, since |
To avoid caching on the server side we are looking into the concept of batch requests (see microsoft/language-server-protocol#988). The current concept in LSP is that it is under the clients control what data is visible and what data therefore need to be priorities. And the concept of an open editor is not enough. A tool could for example show the outline inline in the file explorer and therefore the outline needs to be priorities. So if we let the server decide this then we need to let servers know about what is visible in the UI and what not in terms of LSP requests. |
That's true, but I was thinking about things that are pushed from the server (like errors) - if a user opens a project of 5000 files, the server needs to parse/lint them all, and doing the open files first is most useful. I don't think batching helps the case I had in mind, which is the client asking the server for some data multiple times even if it hasn't changed. For example if the client asks the server for errors multiple times, the server has to either keep a cache of them, or re-compute them. Batching requests seems like it could prevent parsing the file multiple times for different requests, but I don't think it prevents requiring the server to keep copies of the data or re-compute them. I also don't think this addresses the original need though - which is wanting to show errors for some files only when they're open. Even if the errors were pulled from the server, they would still persist when the file was closed unless there was some mechanism to tell the client only to show them while the file is open. |
I agree with that case but it is the ONLY case in LSP where the server pushes. Everything else is pull. So instead of having a UI model sync for errors I would prefer having a pull model for errors. And errors are not only presented in the editor. There are problem views and decorations in the file explorer. |
But doesn't pull mean the server has to invalidate everything on every change? If a user is typing inside a comment - with a push model, the server doesn't need to send any new errors, outline, code fixes, etc. - but if the client is pulling, it's going to keep asking for these and forcing the server to compute them (or keep a cache of them). And when the extension host is remote (Codespaces, etc.) it seems like the extra latency/slow round trips would make this worse? That aside - I still don't think any of that addresses this need. Even in a pull model, it doesn't allow us to show errors for ignored files only while they're open. |
#683 is a related issue. VS Code fires did-open events whenever a file is opened (which includes things like extensions opening them, or the hover preview when holding Ctrl/Cmd), which ends up at the LSP server and causes it to start analyzing files that have never been opened. |
@DanTup did you have any chance to look at the new pull model. I would like to close this issue since I really don't want to sync UI state. |
@dbaeumer I've not looked at this yet - last time I looked I couldn't find the related info (I just had a quick search of the specs and still can't see anything obviously related to pulling diagnostics?), and also this same issue affects us in many other ways that are not all related to diagnostics so I was hoping for a more general fix. For example, our server likes to prioritize and cache parsed results for files that are "open" but not for every file in the workspace. |
The proposed implementation and spec is here:
|
For the more general fix. When VS Code has a proper tab model I will add support to the LSP libs to configure if open should be send for invisible files or not. But this will be an implementation detail in the extension / libs. |
Thanks - I'll have a dig through that and see whether it would be useful.
I still think there could be value in discussing this in the spec (for benefit of other servers/editors), but I don't know that any other editors using our server are doing what VS Code is, so solving it there probably solves the issue entirely (at least for me) anyway. Feel free to move this to the LSP lib repo, or I can do it if you want to close this one. Thanks! |
@dbaeumer could you expand on this? Will the option also control whether didClose is sent for invisible files? And will it also control whether (say) documentSymbols is sent for invisible files? (I'm asking because I'm implementing a hacky temporary middleware which suppresses didOpen+didClose in the case that it's an invisible tab, and I'd like my middleware to have the same behavior as what you eventually envisage for your LSP option.) |
@ljw1004 The idea is to not send and open/change/close events for documents that are not visible in an editor. However since LSP allows sending language requests for not opened documents those will still be allowed on these documents. Sending a language request might need to trigger and open/change notification in case the document is dirty on the client. Instead of putting this into your own middleware would you consider providing a PR for this? |
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.
What is the current state of this issue? Is there any workaround that works and reliably filters exactly the invisible documents? Not spamming the language server with A list of things that we have tried in the past to work around this issue:
I don't see any other VS Code API to filter these requests and I'm wary of messing with the control flow of the language client library since it may introduce undesired race conditions. What is the recommended way to mitigate this issue? |
@mhuisi what you can do right now is the following:
|
We can't switch to pull diagnostics because AFAIK VS Code still does not support result streaming / partial results. As mentioned earlier, processing Lean files is expensive and can take a while, so we can't have users wait for diagnostics for (up to) minutes until the diagnostic pull request for the file can be responded to. |
So you have a first error after some seconds and the last once after minutes for one file? |
Yes, because semantic analysis is (necessarily) very expensive in languages like Lean. For a concrete example, proof scripts may use SMT decision procedures to prove lemmas, which in turn can be used by the type checker to ensure that a program satisfies some formal specification. We also implement an additional There are some other extensions we make to LSP to suit interactive theorem proving needs as well, but those are not really relevant here. Note that the streaming support issue also has a comment from one of the maintainers of coq-lsp, which is another interactive theorem prover operating under similar constraints as Lean. |
If you specifically mean it sending open/close when you hover, I think it's hopeless :) I tried that here: It was closed as a dupe of microsoft/vscode#15178 which has since been implemented. It affected TypeScript too: IMO this is a hack. Language servers may want to know about open documents because a) this changes the owner of the document from the disk to the editor and b) they might want to prioritise or cache data related to open files for performance. VS Code sending an open immediately followed by a close when it's just reading the contents from disk because it might show a preview in the tooltip doesn't feel like it needs to trigger any of this, it feels like an implementation detail of VS Code leaking into language servers (either they specifically write code to detect and ignore this, they potentially suffer worse performance because they start work they didn't need to, or they potentially don't send notifications for push-based features until some other request for the file shows up) 😔 |
I work on the Hack LSP server. It also takes time (1s-5mins depending on complexity) to fully recompute diagnostics. My solution:
This solves the transient didOpen/didClose problem nicely. It also offered a HUGE performance benefit for our single-threaded LSP server, because when a user opened a fresh document and did (say) hover/gotodef then the LSP server would be computing latency-sensitive user actions rather than non-critical squiggles. I don't think of this as a hack! I think it's kind of (in retrospect) the obvious way to implement prioritization of what the LSP should work on next. When I talk about "performance" I refer to what percentage of hover/gotodef/autocomplete requests get a useful response within 200ms (which is my team's criterion for "adequately fast"). Once I ceased doing work on didOpen, and changed to this lazy model, then we went from ~90% of requests getting responses in under 200ms up to ~95%. I spent a lot of time experimenting with pull diagnostics and came to the conclusion that they weren't as good a solution. There are two chief reasons: (1) VSCode sends pull diagnostic requests more eagerly than my solution, hence doesn't give as much benefit, (2) more importantly there's no race-free way to combine pull diagnostics with the push diagnostics inherent in a up-to-5-minute error recomputation, although this might be under-specification rather than an inherent blocker. Here are my raw notes: Normal VSCode didChange behavior. When you change an unmodified file on disk, VSCode updates the editor contents and sends didChange; when you change a modified file on disk, VSCode doesn't update the editor contents and doesn't send didChange. Thus for instance if you rebase at the CLI, then VSCode will send didChange for all files modified by the rebase. Also, imagine a file on disk has errors in it, but the modified buffer doesn't, and you close the modified buffer. The user will naturally expect the diagnostic to be restored upon file-close. Well, this is helped by some (undocumented) VSCode behavior that (1) immediately prior to didClose, it first synthesizes a didChange event which restores the editor content to what is on disk, apparently via line-diffing. Then it sends a pull diagnostic request for the file. Then (without waiting for a response) it sends didClose. InterFileDependencies. This is a flag you specify in your server capabilities. It means that a change in one file will give rise to pull diagnostics requests not just for that file, but for all open files. This is true both in the rebase scenario and regular typing. Therefore, rebases will cause exactly the same set of files to get pulled-diagnostic as got didChange. VSCode has weird behavior (bug?) where it doesn't respect already-open-upon-project-start files for its interFileDependencies. Specifically: if you start with editor tabs open for A and B, and change A, then it will pull diagnostics for A but not B. But if you subsequently switch to tab B and back again to A and change A again, then it will now pull for both A and B. Sequencing. VSCode sends pull-diagnostics request immediately after sending didChange, but it seems to wait until the previous pull-diagnostic has gotten a response before sending another request. So (1) if there are multiple editor tabs open then it only requests diagnostics one at a time, (2) if you type really fast then it will send didChange for each keystroke but will consolidate and not have a backlog of pull diagnostic requests. Disk file changes? Races? If you change a file on disk that's not open in the editor, VSCode won't pull any diagnostics (even if you have interFileDependencies turned on). I suppose you must have to use other mechanisms. I don't know what they'd be, i.e. I don't know how my didChangeWatchedFiles handler should trigger the whole pull-diagnostics machinery. Or alternatively, if my LSP responds to this didChangeWatchedFiles event by pushing diagnostics, how will that race with any pull diagnostics that VSCode sends for the file? Another race I don't understand is if we close a file then VSCode sends didChange followed by a pull-diagnostics request followed immediately by didClose. What if the LSP feels free to push diagnostics for the file after didClose, but VSCode acts upon receipt of pull-diagnostics after that? Failure? I didn't yet investigate how pull diagnostics works with failure, e.g. if a pull-diagnostic request gets an error, then are any previously pushed diagnostics for this file removed? are any previously pulled diagnostics for this file removed? All in all, I actually don't see any benefit to pull diagnostics. I think I could achieve the same overall effect by having the LSP server store a list of files which have so far received outstanding didChange/didOpen events, and if it's idle then push diagnostics for them as needed. I could similarly make didChangeWatchedFile add open files into the list to refresh them. This way I wouldn't worry about races. (The only thing I'd lose with this approach is that pull diagnostics tells me which file should be prioritized). |
Unfortunately, I don't think this approach will work for us, as it doesn't really resolve the issue of Thanks for your detailed analysis and the word of caution about pull diagnostics. |
@DanTup I was referring to the |
Oh, you mean so we could use middleware to filter out |
@mhuisi The reason it works for us (solves the ephemeral didOpen pressure) is because for those ephemeral cmd+hovers, VSCode sends didOpen followed immediately by didClose. Our LSP server first handles (There is a theoretical race condition here, that LSP process might discover empty stdin because the VSCode process I guess got switched out before it had a chance to write didClose, but our telemetry never showed that to happen in practice). By the way, I earlier tried
What we observed is that in production, for reasons I never managed to reproduce mlocally, many of our users encountered a legitimate didOpen (i.e. they truly did open a file) for which |
Thanks! I had always assumed that there are
You can find one reproducible example of this in this thread above that was reported by one of our users (saving an untitled file). That's what the |
@ljw1004 @mhuisi @DanTup great discussion. I would like to add a couple of comments:
Regarding the tab eventing in VS Code. Looking at the event order I would not argue that there is something wrong in VS Code. In the case of saving a untitled file, VS Code generates a new document, however since the editor already exists, it only receives a new input. That results in a changed event on the tab API but on a close/open event on the document. This is different from opening an editor, where the editor first gets created and then the input is created and set. So if you want to handle this in the middleware you basically need to do the same as the client does for pull diagnostics:
This is basically what pull diagnostic does. I haven't implemented that behind a flag since I am not convinced anymore that only syncing visible document to the server is a good approach (there can be long lived documents that are not visible and relevant for a server). |
Do you have an example? |
As far as I can tell, pull diagnostics means VS Code chooses which files to request diagnostics for, but we want users to see all errors across their entire project. When using push diagnostics, we have to reanalyze in
Given this, why is it normal for a client to send IMO if VS Code won't fix this, it seems it would be better done here in the LSP client than everyone affected having to write middleware to try and strip this out. (note: I'm not saying the LSP client should necessarily sync only visible files as this issue became, but I do think it could drop these pointless open/closed events that are a VS Code specific quirk and don't make sense over LSP). |
@DanTup I don't think that's true. What we do is that didChange merely sets an "is-dirty" bit in our LS. Then the LS can perform its reanalysis (so clearing the dirty bit) at its leisure, at any time it choses. |
Actually we do similar - but in some cases there is some synchronous work we must do (to ensure consistency), and for some configurations we modify our analysis roots based on open files (to support large workspaces where we don't want to analyze everything). We could certainly work around this, but I just don't understand why this is being considered normal. If the request is for transferring ownership to the server, why would it makes sense to send didOpen/didClose immediately just because the user Ctrl+Clicked on a symbol and holding Ctrl happened to trigger a hover and the hover wanted to show a preview of contents? This feels like a weird quirk/implementation detail of VS Code that doesn't make sense over LSP and servers are having to change their behaviour to try and mitigate the effects of. Why don't we just filter it out here? There is (as far as I can tell) zero benefit in sending those two events over the wire in this case. |
I looked into it and here is what I think would make sense to implement to not make things overly complicated:
This behavior will go behind a flag in the client options. First cut of the code is in If you think that this would help for your scenarios I will make next releases so that you can give it a try. |
That sounds good to me, thank you! :) Will these releases be tied to the next version of LSP? (it's not clear to me what the release schedule is for LSP, I think it's been a while since the last release and I haven't tried to use a client for the new version yet). |
Thanks, sounds good! :-) |
The new client version Please note that the way how the client and server exports their API has changed. It is now based on the |
@dbaeumer I tested this out and it seems to work as described. If I hold ctrl and hover over a bunch of symbols without clicking, it prevents the open/closed events (which also avoids the Dart server doing some analysis and producing some notifications we normally want for open files). Thanks! Out of interest, do you have some approx target for when this client/next LSP will ship? (I'm not in any rush, it's just useful for my planning). |
After summer vacation :-) (August or September) |
Great, thanks! :-) |
@dbaeumer I presume this version was delayed - do you have any new approximate ETA for it? (I won't hold you to it, it'll just help me plan/prioritise things if I know when it might be coming :-)) |
@DanTup sorry about that. Will definitely be next year. Need to focus on something else the last couple of month. |
@dbaeumer no problem, thanks for the update! |
@dbaeumer I saw a new FWIW I did some testing of both this change and the Thanks! |
This is slightly related to microsoft/vscode#15178. Right now there's no way for an editor to know when a document is either "open" or "visible" in a way that matches the users expectation:
There are many situations where a server would like to know what files a user has open (or visible). For example:
Even though VS Code doesn't have an API for "open editors", it does have an API for "visible editors". Even if VS Code plans to never support "open editors" it would be very useful for LSP to provide "visible editors". On the other hand, if VS Code does add support for "open editors", then that could be provided instead/as well. In either case, it seems like LSP needs some changes to support one or the other (or both).
(as a workaround, I'm considering implementing custom messages in the VS Code extension + LSP server to pass the "visible editors" over to the server.. it feels really hacky though).
The text was updated successfully, but these errors were encountered: