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.6.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

We recommend installing Coq with OPAM, since many other required packages are also available via OPAM.

The installation command for OPAM is:

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

On macOS you can get opam through Homebrew with brew install opam. Consult https://opam.ocaml.org/doc/Install.html for other ways to install OPAM.

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.6.1 by:

opam install coq.8.6.1

If you are an Emacs user, you might be interested in Proof General and company-coq.

Install Haskell (beginning with Lab 1)

We will use Haskell to compile and run implementations written in Coq beginning with Lab 1. Before then you don't need to worry about it, but if you want to get Stack installed follow the instructions below.

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/

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.

Creative Commons License