Software installation guide

This page collects installation instructions for all the components used in the various lectures. Feel free to raise installation issues on Piazza to improve this guidebook.

All-in-one

For those that like Nix or Docker, a Nix project for building everything, as well as a Docker image, is available on GitHub: https://github.com/jwiegley/dsss17

(Note that you do not need to clone this repo unless you want the all-in-one Docker image: you want the similarly named dsss17 repo found below!)

Separate Components

For those that prefer an unbundled installation, here's how to build the individual pieces...

Coq

It is recommended to install Coq with OPAM, since many other required packages are also available via OPAM.

The generic installation command is:

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

Other ways to install OPAM: https://opam.ocaml.org/doc/Install.html

In some situations, 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 by:

opam install coq.8.6

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

QuickChick

QuickChick depends on: Coq 8.6 (mentioned above), ssreflect and ext-lib, which are available from OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-ext-lib
opam install coq-mathcomp-ssreflect

Now you can install QuickChick from source:

git clone https://github.com/QuickChick/QuickChick.git
make -C QuickChick -j install

You will see lots of warnings from the compilation. This is expected.

If you see compilation errors, check that your OCaml compiler is new enough using ocamlc -v or:

  opam config report

Version 4.04 is known to work; 4.03 should also work (4.05 was just released and is not yet tested). If your OCaml is too old, you can upgrade it like this:

opam switch 4.04.0

(You may need to reinstall other things afterwards.)

Lecture materials

The dsss17 repository contains lecture material and library packages for various lectures.

To fetch and prepare it run:

git clone https://github.com/DeepSpec/dsss17.git
make -C dsss17

Troubleshooting

“Inconsistent assumptions” errors usually happen because some .v file early in the dependency chain has been changed and recompiled but some later one has not been recompiled. Doing “make clean” usually puts things right.

Optional Packages

Ott (optional)

Ott isvailable via OPAM:

opam install ott

lngen (optional)

The easiest way to install lngen is via the Haskell Tool Stack. The generic command to install Stack is:

curl -sSL https://get.haskellstack.org/ | sh

More installation instructions: https://docs.haskellstack.org/en/stable/install_and_upgrade/

Once you have Stack, you can install lngen from source:

git clone https://github.com/plclub/lngen.git
cd lngen
stack setup
stack install

---