You'll also need an IDE, since Coq is an interactive tool. We recommend using VSCode and its Coq extension, VSCoq, for this purpose, which is easy to use even if you're not familiar with this text editor and has a decent Vim emulation plugin if that's your editor of choice. Follow the installation instructions for VSCode from its website, then go to extensions and install VSCoq.
There are three main commands to learn in VSCoq, with their default keybindings: alt-down to "step forward" and process the next command, alt-up to "step backward" and undo one command, and alt-right to "interpret to point" and process all the commands up to where the cursor is (or back up to that point). On macOS these keybindings are ctrl-alt-down, ctrl-alt-up, and ctrl-alt-right.
Note: this is the first year we're trying VSCoq; if you have trouble using it, please post on Piazza and we can help troubleshoot it for you. We used to recommend CoqIDE, which we believe is much more painful to use than VSCode, but if you get it to work it's definitely sufficient for the course.
On macOS, you can install the latest version of Coq easily using Homebrew with brew install coq.
The installation instructions for opam for your particular distribution are available at https://opam.ocaml.org/doc/Install.html (note that you do need opam 2; opam 1 will not work). On any distribution, the following should work to install opam:
sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)
After installing OPAM, you need to initialize its state with:
opam init eval $(opam env) opam update
Once you have OPAM ready, install Coq 8.12.0 by running:
opam install coq.8.12.0
To interact with Coq you'll need CoqIDE. Debian/Ubuntu users should first get necessary system packages using sudo apt-get install libgtksourceview-3.0-dev. You can install CoqIDE with:
opam install coqide
If you want to compile and run the software we're writing (beginning with lab 1), you can install Haskell.
We recommend you install Haskell using Stack. On Arch Linux, you can install Stack using sudo pacman -S stack. The generic command (recommended for Debian/Ubuntu) to install Stack is:
curl -sSL https://get.haskellstack.org/ | sh
On macOS, we recommend you use Homebrew to install Stack with brew install haskell-stack, though you can use the curl command above.
More installation instructions: https://docs.haskellstack.org/en/stable/install_and_upgrade/