[Feature Request] Incremental textDocument/didChange

[huynhtrankhanh]

This is mainly useful when coq-lsp and the client are separated by a network.

Currently, coq-lsp only supports whole document sync. This is fine when both the server and the client are on the same machine, as parsing is pretty fast.

However, when the client has to access the server over a network, the client would need to send the whole document, possibly on every keystroke. This can have a deleterious effect on latency.

I propose that we should implement incremental textDocument/didChange simply by applying the diff on the document, then continue as if we'd been given the whole document.

[Alizter]

We definitely could implement incremental didChange. From what I have read the important parts of the LSP protocol are here:

• https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_synchronization

Rust-analyzer (the LSP server for rust) implements incremental changes in the following way:
https://github.com/rust-lang/rust-analyzer/blob/ba329913fa33c29d4ccabf46998d3a0cfac57b0c/crates/rust-analyzer/src/lsp_utils.rs#L131

So we can take some inspiration from that.

I think we would like to have such a feature configurable since it might work better for others. I would be interested to see if there are any performance issues when processing a lot of changes.

Applying a diff seems like a sensible way to do this, however we would have to understand what the server should do when given an invalid diff.

[ejgallego]

Indeed this would be nice to have, as I mentioned in Zulip the reason I didn't put time on it is:

• gains are quite marginal, I'm actually quite surprised to hear that is a problem even in a "network" case (do you have more details folks)
• the change algorithm itself is not so easy to implement, LSP did a pretty bad, windows-specific choice of encoding so often you'll have to convert text to UTF-16 then back to UTF-8 which Coq can understand. So that'd be a source of bugs I don't feel like debugging myself.

Note that both ocaml-lsp and vscoq2 have implemented this algorithm (tho I'm not sure if they handle UTF properly) so in principle anyone interested could just go ahead a submit a PR.