Description
Hi all,
this is a proposal to define more formally the "jsCoq protocol" between editors / interfaces and servers as a superset of LSP.
cc: @corwin-of-amber
Preliminaries
The first jsCoq protocol was just a reification of the Coq's STM API into JavaScript.
This was good for a first try, however problems with the protocol and implementation quickly arose; in the end, we decided to rewrite the "STM", and adopted a more declarative API, which is a good fit for LSP and most editors.
This protocol added quite a few custom calls for completion, etc...
Flèche
The new implementation, called Flèche, basically provides two methods:
val update: Doc.t -> string -> Doc.t: updates a document (with a diff or full text)val check : Doc.t -> Target.t -> Doc.t: builds a document up totarget
Most functions like goals etc are functions from Doc.t to some object, using Coq API's
On top of that, Flèche has a small scheduler so clients can request to be waken up when the document built reaches a particular point. For example, using making an edit and requesting goals usually work like this:
updateis called, Flèche will invalidate the required parts, including pending requests on old document versionsgoalis called, for atarget. The request is passed to the scheduler, which will either:- serve the request automatically, if the data is already there
- queue the request and schedule
check ~doc ~target - cancel the request if for some reason it cannot be served
Note that actual checking doesn't happen, until coq-lsp is idle. Then, the idle loop will at some point serve the request, as it is on the scheduler queue, or cancel it. This is likely something we could fine tune by doing some speculative checking.
jsCoq "LSP" branch
The new "lsp" branches of jsCoq have been updated to use Flèche, with a custom protocol that basically reifies the above API into JS objects. The document part of the protocol is basically isomorphic to LSP, with TTBOMK minor differences. This seems to work well.
The coq-lsp javascript worker
The coq-lsp project is also a thin layer over Flèche; code is in the controller directory. Most of the code is just the event loop and code for different LSP request, such as goals, hover, completion, etc... Some of the code should we maybe moved to Flèche, but that would be a minor refactoring.
Thanks to all the work done in jsCoq, we were able to build a fully functional Web Worker speaking LSP, which is now used for vscode.dev / github.dev.
As of today, a Web Worker is built automatically on CI, and released to the VSCode marketplace.
While LSP covers a lot of stuff that was done in our custom protocol, such as completion, hover, document management, it is missing a few features that are needed for jsCoq / coq-lsp jsCoq version, in particular, we lack:
- goals and some other specific Coq stuff
- interruption support
- package management
The situation today
While things were not intended to go this way, as of today we are in the situation that duplicates a lot of work:
We build 3 workers, with 3 different protocols, (WASM and JSOO are a bit different too). Moreover, we need to build packages for both of them.
The differences between these workers are actually minimal, mostly cosmetic AFAICT.
Moreover, jsCoq needs to keep coupled to the Coq API which makes it hard to develop; in particular about low-level stuff like initialization, findlib, etc...
Proposal: jsCoq protocol = LSP + jsCoq extensions
I propose we converge to a single web worker implementation (with WASM and JSOO backend), based directly on the lsp layer of coq-lsp.
jsCoq would welcome front-end only, using LSP with our own custom extensions embedded on it. In particular we need to document:
- Interrupt Setup
- Sending and Adding files to the server
- Package management API
Note that LSP has planned support for something pretty essential to us, which is synchronization between the client and server FS. See microsoft/language-server-protocol#1264 for more details.
IMHO this is something to keep in mind when designing our protocol, there are new changes in LSP 3.18 towards improving the situation here, so the closer we get to the protocol the better.
Things to do, what would the switch mean?
On the frontend-side, there should not be a lot to do, our protocols are very close to the JSP (or JLSP = JsCoq Language Server Protocol)
Ideally, our worker.ts code would be replaced by the standard LSP / JSON-RPC client on npm.
I think we should come with a different name for the coq-lsp worker, which is really coq-lsp + jsCoq ; jscoq-lsp ? Branding is IMHO important, and I'd like to see the coq-lsp Web Version to carry jsCoq branding as it used a lot of the knowledge and code of jsCoq.
Where to host package management? This is a point I am not sure very well how to move forward, in principle it seems to me that most logical thing would be to move the package code to coq-lsp repos so the worker build does build some packages, but I dunno.
Advantages of migrating
- Same version of jsCoq can run much more easily for several Coq versions (we already generate coq-lsp workers for each of the Coq branches)
- Our protocol becomes standard which could help contributors
- We reduce duplication a big time
- jsCoq can focus more on usability
- Coq CI problem is solved
Disadvantages
vscode-languageserverlibraries may not be as flexible as rolling up our solution, on the other hand they allow contributions; they are also a bit more complex than our setup- credit and branding needs to have a good story
- missing jsCoq features in the server side need to be implemented first in Flèche / coq-lsp, but IMHO that's a plus; code there may look intimidating but actually it is not so hard.
Conclusion
OK, that's all I could think of; let me know if you folks have any thoughts.