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.
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
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/
Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at firstname.lastname@example.org.