@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.
Yes, I've seen it. It is a bit unclear to me how much of that could be used in Coq.
Thanks @Théo Zimmermann , indeed that slipped my way as I'm still on holidays and likely to extend a bit more.
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