Rocq

Running/Installing Rocq Theorem Prover

Remote running (jscoq)

You can have a limited setup to run simple examples and test basic tactics online. It can be useful for the first lecture.

https://jscoq.github.io/scratchpad.html

Local Setup

For a more robust interfacing, it is recommended to have it installed locally. The official Rocq page, i.e., https://rocq-prover.org/install contains specific installations for your platform, including Windows.

During the lectures, we will use vscode which I recommend for its simplicity.