# Using vsrocq language server with Emacs

**URL:** <https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119>\
**Category:** Developing plugins\
**Tags:** coq-lsp\
**Created:** [September 29, 2026, 9:36am UTC](https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119 "2026-09-29T09:36:48Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Michalis](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/michalis/32/1302_2.png) [@Michalis](https://discourse.rocq-prover.org/u/Michalis)\
**Post date:** [September 29, 2026, 9:36am UTC](https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119/1 "2026-09-29T09:36:48Z")

</div>

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](https://codeberg.org/jpoiret/rocq-mode.el), 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.

---

<div class="post-metadata">

**Author:** ![TDiazT](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/tdiazt/32/196_2.png) [@TDiazT](https://discourse.rocq-prover.org/u/TDiazT)\
**Post date:** [September 29, 2026, 10:13pm UTC](https://discourse.rocq-prover.org/t/using-vsrocq-language-server-with-emacs/3119/2 "2026-09-29T22:13:33Z")

</div>

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 🙂.