Stream: Coq devs & plugin devs

Topic: LSP


view this post on Zulip Théo Zimmermann (May 21 2021 at 16:46):

@Emilio Jesús Gallego Arias and other people working on LSP: Have you seen this? https://cister-labs.pt/f-ide2021/images/preprints/F-IDE_2021_paper_3.pdf
There's an associated presentation at 17:30 CEST on Monday. I can share the Zoom link with those interested.

view this post on Zulip Enrico Tassi (May 21 2021 at 16:51):

Yes, I've seen it. It is a bit unclear to me how much of that could be used in Coq.

view this post on Zulip Emilio Jesús Gallego Arias (May 21 2021 at 18:34):

Thanks @Théo Zimmermann , indeed that slipped my way as I'm still on holidays and likely to extend a bit more.

view this post on Zulip Emilio Jesús Gallego Arias (May 21 2021 at 18:35):

IMHO anything that doesn't involve the LSP developers at MS too may not work well, we had a discussion with Makarius (and transitively with Leo) some time ago, but got stuck due to lack of cycles and due to other issue


Last updated: Oct 16 2021 at 02:03 UTC