@camrein do you know if the LSP server will queue a parsing+resolution task for each textDocument/didChange request it receives? If so, can we make the queue have a maximum size of one, so only the latest code is analysed?

I know there is some batching of changes on the client side. I vaguely recall it sends out a didChange if there's no more edits for 200 ms, but since a parse+resolution task may take more than 200 ms, it's still possible that these tasks could get queued on the server.

The behavior that I think might be nice is:

User does:

• type 'A' and wait 200ms
• type 'B' and wait 200ms
• type 'C' and wait 200ms

Server does:

• Receive didChange for 'A' and start analysing 'A'
• Receive didChange for 'B' and queue the analysis of 'AB'
• Receive didChange for 'C', queue the analysis of 'ABC' and drop the analysis of 'AB'
• Finish the analysis of 'A', start analysis of 'ABC'.

This issue is closely related to dafny-lang/ide-vscode#31.

@camrein do you know if the LSP server will queue a parsing+resolution task for each textDocument/didChange request it receives? If so, can we make the queue have a maximum size of one, so only the latest code is analysed?

All document related events (for example change/save/open/close) are synchronous/serial. See for example DidChangeTextDocumentParams.
If any request is processed on a handler with the Serial-Attribute, it blocks all other requests - including the ones with the Parallel-Attribute. Unfortunately, I don't know how this mechanic is achieved in the LSP library behind the scenes. I.e., if there's a queue or that it simply blocks the input (that'd be stdin for Dafny VSCode).

I have the feeling that we have to implement this behavior ourselves. But there are a few challenges we have to keep in mind:

• Offload any incoming document events into a separate task/document queue. That way, we can complete the document request immediately; thus, new changes can be received.
• The event in the task/queue will then be processed, if not overtaken by a newer event (ABC will be processed in place of AB as in your example). If a change is overtaken, we have to process the change but can leave parsing/resolution/verification aside.
• Since all other queries such as hover can now run concurrently to the document updates, we have to make sure that these queries happen on the correct document version.

Maybe we could combine it with a debouncing of the automatic verification in a later iteration.

If any request is processed on a handler with the Serial-Attribute, it blocks all other requests

I'm guessing that if you process the request in a fresh thread then the block is lifted. For example by adding the request data to a thread-safe queue and then letting a worker thread manage it.

But there are a few challenges we have to keep in mind...

One option is to merge consecutive textDocument/didChange requests, and otherwise process the requests sequentially, where processing a didChange request also includes computing diagnostics.

Another option might be to cancel any currently running analysis, including computing diagnostics, as soon as a didChange comes in, so we never do processing on an out of date document state.