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.9.1 and on Haskell (to run code extracted from 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 Coq

macOS

On macOS, you have two options: CoqIDE or Emacs. For CoqIDE, install from the pre-compiled macOS installer from GitHub, then use it as your Coq installation. You can do that by adding the following to the end of your ~/.bash_profile file (or adapt this for whatever shell you use):

export PATH="/Applications/CoqIDE_8.9.1.app/Contents/Resources/bin:$PATH"

You only need this to compile the provided framework code for the labs.

If you are an Emacs user and know what you're doing, instead of CoqIDE you may want to try Proof General and optionally company-coq. In that case, you can install Coq with Homebrew using 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 are available at https://opam.ocaml.org/doc/Install.html (note that you do need opam 2; opam 1 will not work). The following should work to install opam in /usr/local/bin:

wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin

After installing OPAM, you need to initialize its state with:

opam init
eval `opam config env`
opam update

Once you have OPAM ready, install Coq 8.9.1 by running:

opam install coq.8.9.1

To interact with Coq you'll need CoqIDE, which you can install with:

opam install coqide

If you are an Emacs user, instead of CoqIDE you may want to try Proof General and optionally company-coq.

Install Haskell

We will use Haskell to compile and run implementations written in Coq beginning with Lab 1.

We recommend you install Haskell using Stack. The generic command 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/