/CompCert-Makefile

A simple Makefile example for `ccomp`

Primary LanguageMakefileMIT LicenseMIT

CompCert-Makefile

Simple Makefile example for CompCert C compiler.

Usage

Build & Run

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

How to Install CompCert C compiler

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
  1. Install Coq.
opam update  # Update the packages database
opam install coq.8.7.1
  1. Install Menhir.
opam install menhir
  1. Add the path $HOME/.opam/4.06.1/bin and check installation was successful.
coqc -v
menhir --version

License

MIT