INSTALL.md

Installing CertiCoq

Get the code

Fetch the code:

$ git clone [email protected]:CertiCoq/certicoq.git

Fetch the dependencies:

$ git submodule update --init

Install using opam (preferred)

First, pin the dependencies:

$ opam pin -n -y submodules/metacoq

Next, pin CertiCoq:

$ opam pin -n -y .

You can now install CertiCoq:

$ opam install coq-certicoq

Alternatively, if you only want to install the dependencies, you can run:

$ opam install coq-certicoq --deps-only

Build & install manually

Dependencies

If possible, install the dependencies using the opam instructions given above.

If that is not an option, you can instead use these "manual" instructions. Note that this approach will only work if your installation path for Coq is writable without root privileges.

Make sure that you do not have any of the dependencies installed already. From the certicoq/ directory, run:

$ make submodules

Building the compiler

Once the dependencies are installed (either via opam or by the manual method), you can build the Coq theory by running

$ make all

The plugin, which depends on the Coq theory, can be built by running

$ make plugin

To install the theory & plugin, simply run

$ make install

Testing the installation

You can test the installation using the including benchmark suite:

$ make -C benchmarks all