You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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.
The text was updated successfully, but these errors were encountered:
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 forshareService
. More details below:coq-lsp
https://github.com/ejgallego/coq-lspDescribe 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: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.
The text was updated successfully, but these errors were encountered: