Coq On Your Computer

Supported Coq Versions

The following Coq versions will work well with the code provided with the learning material:

  • 8.18
  • 8.19.1
  • 8.19.2
  • 8.20.1
  • 9.0.0 (with deprecation warnings)

You can try other versions as well, but we might be less able to help you with problems you encounter.

Installing and Using Coq

There are multiple ways to use / install Coq on your machine. An extensive overview is given on the official website.

VsCoq (Visual Studio Code + Coq)

We recommend installing the VsCoq extension in VS Code on your own machine. In case that doesn’t work for you, you can try using the FRS Coq Virtual Machine or some of the other options.

Installing VsCoq on Your Own Machine

  1. Follow the installation instructions.
  2. In case the instructions above do not work for you, you can try following the official guide.
  3. In the extension settings, change Vscoq > Proof: Mode to Continuous (instead of Manual). This will allow VsCoq to provide you with continuous information about the state of your proof.

FRS Coq VM

If installing VsCoq on your machine doesn’t work, you can download a Debian-based virtual machine that we’ve prepared for this course:

  1. Download the VM.
  2. Download VirtualBox.
  3. Start the VM in VirtualBox and open Visual Studio Code - everything should be preinstalled and set up.

Both the user and root passwords for the VM are pwd.

Other

If VsCoq doesn’t work for you, you can try one of the following: