Simple Makefile example for CompCert C compiler.

Hello, World! at CompCert C compiler.

make run

However, it is also possible to build using CMake for confirmation.

mkdir -p cmake-build-debug && cd $_ && cmake ..
make run

Details are written on the official page, so I will explain how to obtain what you need such as Coq.

1. Install OPAM. On Ubutu 16.04:

sudo apt install opam
opam init --comp 4.06.1  # Initialize ~/.opam
eval `opam config env`

sudo apt install m4  # If you get a warning about m4

2. Install Coq.

opam update  # Update the packages database
opam install coq.8.7.1

3. Install Menhir.

opam install menhir

4. Add the path $HOME/.opam/4.06.1/bin and check installation was successful.

coqc -v
menhir --version

MIT