Configuring Your Editor

While the toplevel is great for interactively trying out the language, we will shortly need to write Rocq files in an editor.

Rocq has plugins for many editors, but the most actively maintained are for Visual Studio Code, Emacs and Vim.

Visual Studio Code

TL;DR Install the package vsrocq-language-server in your opam switch.

For VSCode, install the Rocq Visual Studio Code extension from the Visual Studio Marketplace. The extension depends on Rocq LSP. To install it in your switch, you can run:

$ opam install vsrocq-language-server

You can alternatively install rocq-lsp.

Now you are ready to write some Rocq code and proofs!

Editor Features at Your Disposal

If your editor is setup correctly, here are some important features you can begin using to your advantage:

1) Hovering for Type Information:

This is a great feature that let's you see type information of any Rocq definition. All you have to do is place your cursor over the code and it will be displayed in the tooltip.

More ...

In Construction

Emacs and Vim

Emacs users can use the major Rocq mode Proof General, that can be extended by the minor Coq mode Company-Coq.

See their webpage for installation instructions.

Vim/NeoVim users can use the Coqtail extension. NeoVim users can also test the experimental support for VsCoq's vscoqtop server or for coq-lsp.

Standalone interfaces

Alternatively, you can use RocqIDE, a standalone desktop application which is developed and distributed alongside the Rocq Prover.

As a way to try Rocq without installing anything, you can use JsRocq. JsRocq loads Rocq entirely in your browser.