CompCert Install Instructions

Dependencies

Additional dependencies

Replace with the package manager for your distribution

sudo <pkg-manager> install -y mercurial darcs ocaml bubblewrap

Opam

sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)

Post-install

Run

eval `opam config env`

Add this to your .bashrc or .bash_profile

. $HOME/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

Switch to a recent OCaml compiler version

opam switch create 4.12.0
opam switch 4.12.0

Install dependencies available through opam

opam install coq menhir

Note: it may happen that a newer version of Coq is not supported yet. You may downgrade to solve the problem:

opam pin add coq 8.13.2 # example of Coq version

For Kalray KVX

On this platform, we also need Gappa installed. You may need to first install some development packages. On Ubuntu:

apt install bison flex libmpfr-dev libboost-dev

This install Gappa and Flocq:

opam pin add coq-flocq 3.4.0 --no-action
opam install gappa coq-gappa coq-flocq

Compilation

You can choose change the installation directory by modifying the config_simple.sh file before running the configuration script.

Then, use the configuration script corresponding to your desired platform: (for Kalray Coolidge it is config_kvx.sh)

./config_<platform>.sh

If using Kalray's platform, make sure that the kvx tools are on your path Compile (adapt -j# to the number of cores and available RAM)

make -j12
make install

Tests

Documentation

You can generate the documentation locally with:

make documentation

Note that you need to install coq2html before doing so.

Utilization

ccomp binaries are installed at $(CCOMP_INSTALL_PREFIX)/bin (variable defined in config_simple.sh). Make sure to add that to your path to ease its use Now you may use it like a regular compiler

ccomp -O3 test.c -S
ccomp -O3 test.c -o test.bin

Changing platform

If you decide to change the platform, for instance from kvx-cos to kvx-mbr, you should change the compcert.ini file with the respective tools and then run

make install

Cleaning

To clean only object files while keeping the platform configuration:

make clean

To clean everything (to then reconfigure for another platform):

make distclean