Using vsrocq language server with Emacs

Developing plugins
1

Has anyone looked at integrating the vsrocq language server with emacs? I have been using jpoiret/rocq-mode.el: An Emacs mode for the Rocq theorem prover, using coq-lsp - Codeberg.org, and I really like its workflow over Proof-General, but I wonder if it would be better to base it on vsrocq, rather than rocq-lsp, since the former seems to be the more full-featured language server.

If nothing exists, I might experiment with either adapting rocq-mode or building something new. Curious if that is something people would be interested in.

2

Hi Michalis, yes, I will be working on VsRocq soon and one of my intentions is to integrate the language server with Josselin’s project. Feel free to reach out in Zulip (or privately here if you prefer) and maybe we can organize some meeting with Josselin and the other developers of VsRocq, to setup a route to have this working :slight_smile:.