Installing course software

This page helps you install the software you need to complete the assignments in 6.826. 6.826 relies on Coq 8.12 and an IDE to interact with Coq. We assume you will install the software on your own computer. The instructions are for Linux and macOS. If you run Windows, we suggest you create a virtual machine with Linux.

Install an IDE

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.

If you're an expert you can also use Coqtail for (neo)vim or Proof General for Emacs. These aren't officially supported, although the course staff uses Emacs and Proof General.

Install Coq

macOS

On macOS, you can install the latest version of Coq easily using Homebrew with brew install coq.

Linux

All Ubuntu releases have a version of Coq too old to run the lab software. On those systems, we recommend installing Coq with opam, since it's the easiest way to get an up-to-date version of 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're an expert you can also use Coqtail for (neo)vim or Proof General for Emacs. These aren't officially supported, although the course staff uses Emacs and Proof General.

Install Haskell (optional)

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/