Stream: coq-lsp

Topic: Synchronization

Emilio Jesús Gallego Arias (Jan 25 2023 at 17:38):

@Alex Sanchez-Stern , one extra point about "document synchronization". As of now, the only method coq-lsp supports is full document, then coq-lsp will do it's own diff and recompute what it needs.

This is very convenient for editors, as the cost of that is very small (even for large documents) compared to usual Coq cost, but indeed, that's not so optimal in some cases, in particular when a non-editor tool is at the other side. I'd like to distinguish about 2 main cases I know about:

• The tool uses their own representation for Coq tactics / command that are at some point written down into text. Then, in this case, to support the current model, the tool would need to represent the document as a rope to allow good diff capability. In this case I think it would make sense for coq-lsp to support the diff method so each tool doesn't have to re-implement their rope thing, and they can just send diffs to coq-lsp, but still text based.
• The tool uses the internal Coq representation for ASTs, this is the case for example of mutation tools that read a Coq AST and mutate it back. This is subtle as Coq printer is far from injective (unfortunately) so the tool has to keep working with the ASTs. This is indeed IMHO a case that would warrant a coq-specific protocol extension. coq-lsp can indeed receive the AST and perform the magic to keep everything consistent, however there are some important considerations depending on the application, in particular depending on whether the document manager should be able to work with fully "virtual" doc nodes or not.

Does it make sense? I'll put this info in a coq-lsp issue.

Alex Sanchez-Stern (Jan 25 2023 at 18:46):

Hmm, I'm not sure I understand the first case, though it seems most similar to what I'm doing. Why would the clients representation affect coq-lsp's ability to do diffs? Currently I store the document on my side as a list of string sentences (that's basically a rope, right?), and then I just join them with newlines when I want to send the document to coq-lsp.

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:48):

What I mean by case 1 is that clients can just send Remove(pos, text), Add(pos,text) instead of having to maintain a data structure

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:49):

like your list, or a rope which is in general more efficient

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:49):

for example updating a haskell or OCaml list is O(N) !

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:49):

so that's very costly

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:51):

So the message in point 1 is "clients, don't implement your own structure to efficiently update a document client side, let's just support the diff-based didUpdate in the protocol"

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:52):

Why would the clients representation affect coq-lsp's ability to do diffs?

Sorry I meant "to allow good diff capacity in the tool itself"

Emilio Jesús Gallego Arias (Jan 25 2023 at 18:53):

So if your tool would work fine with didUpdate based on diffs, we can implement it in coq-lsp directly.

Alex Sanchez-Stern (Jan 25 2023 at 18:57):

Ah yeah that makes sense. In Python, list appending is O(1) amortized, they use a dynamically resizing vector under the hood. I think for my use case, it's often useful to compute things about the proof history on the client side, like how many commands have been run since the start of the theorem, as well as what states they resulted in, so that we can look for state-cycles. Also sometimes the tactic history is a feature to the model. So I probably need to have some sort of representation on the client side, if only to keep a list of the visited states in a particular path.

Alex Sanchez-Stern (Jan 25 2023 at 19:06):

Hmm I guess that only really applies to the current proof though, all the proofs earlier in the file aren't changing during search, so it would be nice to just replace the contents of the current proof with my proof command buffer.

Emilio Jesús Gallego Arias (Jan 25 2023 at 19:59):

Indeed, thanks for these details! Indeed client-side will always have some representation of state, the question is whether a full text document may not be the best for some cases; but that's indeed a minor issue when we take into consideration the global complexity of the application.

Last updated: Apr 19 2024 at 15:02 UTC