Rocq Installation

The over-arching recommendation I have for a clean and quick Rocq install is:

1. Use a Unix-esque environment (WSL for Windows, default for macOS and Linux)
2. Use opam and follow the install instructions. In particular, I would suggest using the shell script.
3. Once you have opam installed (and properly initialized), just run opam install coq.9.0.0

FAQs

1. What is WSL? WSL is the Windows Subsystem for Linux. It gives you all the benefits of a Linux programming environment, from your Windows machine. Here are some WSL install Docs.
2. Do I need to use WSL? Not necessarily… but opam support for Windows natively is very new and relatively buggy. You might find yourself up against cases of “sorry you just can’t do that on Windows with opam currently”
3. Okay I have this WSL thing, what do I do? Enter the WSL Linux environment with the command:

wsl

Navigate to some folder you care about putting the Rocq code in:

cd ~/Rocq/2025/lf       # navigate to folder
code .                  # Launches vscode

From there, make sure you have the right Rocq extension installed (see below)

Proving with Rocq

Use VSCode… alternatives exist, but they are not well-supported or have hardly any features. In particular, I use the coq-lsp vscode extension. Others also have great success with vsrocq. Both will involve you using opam to install a language server. Thus, the importance of using opam.

Still having trouble?

Try searching online, it might be a common issue with a fix. Otherwise, come to office hours.