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

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.

Once you've installed stack, you'll need to do a one-time setup to download the compiler. If you already use Haskell, this will not interfere with your existing Haskell setup. Clone the class repo and, in the statdb-cli directory, run

stack setup

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.