VsCoq 1.0 Roadmap

VsCoq currently relies on an adapter between the protocol spoken by Coq (the XML protocol used by CoqIDE) and LSP. This architecture is fragile because the CoqIDE protocol was designed for a different interaction model, and makes the codebase hard to maintain and extend.

We are currently working on simplifying this architecture, with a language server interfacing with Coq and natively speaking (an extension of) LSP. In order to do so, we will go through the following steps:

• Separate parsing and execution in Coq. Since Coq's parsing rules can be extended by commands in the middle of a file, the system sometimes requires full execution before being able to continue parsing. This can be improved by a better separation of parsing effects. See https://github.com/coq/coq/pull/15825 (Maxime & Enrico, end of September 2022)

• Design and implement a minimal language server which maintains a representation of a Coq document and speaks LSP. See https://github.com/gares/vscoq/tree/document-manager (Maxime & Enrico, end of October 2022)

• Create a new, minimal VsCoq extension supporting the corresponding features and a testing infrastructure (Research Engineers, December 2022)

Once these three main steps are completed, the following ones are listed in the project https://github.com/coq-community/vscoq/projects/1 (Enrico, Maxime and research engineers). At this point, we will welcome external contributions.