Extension support: coq-lsp

[ejgallego]

cc: #34 [opening a new issue, but happy to move to #34 if that's better for you]

Dear Live Share developers,

I am requesting you add the ejgallego.coq-lsp extension to the whitelist for shareService. More details below:

• Programming Language: The Coq Interactive Therorem Prover https://github.com/coq/coq
• Extension: coq-lsp https://github.com/ejgallego/coq-lsp

Describe your extension briefly

The coq-lsp extension provides LSP support for Coq and Coq markdown files, mainly via LSP.

Describe why you need access to shareService()

Live Share works pretty well already on coq-lsp by virtue of LSP support in LS, however a crucial functionality of the extension is missing for Live Share to become usable: goal display.

In Coq, as in other theorem provers, users work with a side panel (the main job of the client extension) that displays proof obligations. We have implemented this "Goal Request" as a LSP extension, see https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md#goal-display

The typical workflow without Live Share is that the editor request the server for the goals, then these are displayed on the side panel.

All we need is to be able to forward a LSP request and get the answer back. AFAICT shareService seems the supported way, but if there is an easier way to integrate LSP extensions with Live Share we'd gladly follow that path.

Live Share is a key use case of the extension, as Coq is most often used in many graduate and under graduate level teaching courses.

How do you intent to use shareService() ?

We intent to use shareService to:

• relay the goals request of the host to the guests, so they can see them:
  • host send a notification
  • guest listens to the notification, show host goals in info panel (notated with the host provenance)
• allow guests to request goals for a particular point of the document:
  • guest sends a request to the service for goals
  • the request is fullfilled by the host in a standard way

Size of the payload depends a lot on the Coq development, but it usually goes from a few bytes to a few KiBs

Security analysis

In principle the forwarded data is displayed by React in the guest, which is safe; most of the data is Coq's own Rich Text Format setup, but indeed it would be maybe wise to restrict the first versions to just sending string payloads, which should be safe, until we can assess the security of the Rich Text renderer (which escapes React briefly to do some layout and could be, as of today, vulnerable to injection from a malicious host).

Further comments

coq-lsp is an official Inria project, the institute that develops Coq.

We have a prototype of VSLS support in the works, it is not public as we hacked the extension ID to be able to test it, we'd be very happy to share the code with you.

Thank you very much for your help, I am at your disposal for any further questions.