Chapter 2 Installation instructions

This chapter explains how to install CompCert C.

2.1 Obtaining CompCert C

CompCert C is distributed in source form. It can be freely downloaded from

The public release above can be used freely for evaluation, research and educational purposes, but commercial uses require purchasing a license from AbsInt (https://www.absint.com/). See the license conditions at https://compcert.org/doc/LICENSE.txt for more details.

2.2 Prerequisites

The following software components are required to build, install, and execute the CompCert C compiler.

2.2.1 Software required for building and installing CompCert C

The Coq proof assistant, version 8.12.0 to 8.19.1

Coq is free software, available from https://coq.inria.fr/ and also as precompiled packages in several Linux distributions and in Homebrew and MacPorts for macOS.

The OCaml functional language, version 4.05 to 4.14

OCaml is free software, available from http://ocaml.org/. OCaml is also available as precompiled packages in most Linux distributions, in Homebrew and MacPorts for macOS, and in Cygwin for Windows.

The Menhir parser generator, version 20190626 or newer

Menhir is free software, available from https://gallium.inria.fr/~fpottier/menhir/.

The simplest way to install these three prerequisites is to install the Coq platform (https://coq.inria.fr/download), which provides suitable versions of OCaml, Coq, and Menhir.

Another option is to use OPAM, the OCaml Package Manager, available from https://opam.ocaml.org/ and also as precompiled packages in several Linux distributions, in Homebrew and MacPorts for macOS, and in Cygwin for Windows. (Version 2 of OPAM is required; version 1, as provided by some Linux distributions, is too old.) Once OPAM is installed, initialized (opam init) and up to date (opam upgrade), just issue the following commands:

      opam switch create 4.14.1     # Use OCaml version 4.14.1 (for example)
      eval $(opam env)
      opam install coq=8.15.2       # Use Coq version 8.15.2 (for example)
      opam install menhir

2.2.2 Software required for using CompCert C

A C compiler: either GNU GCC version 3 or later, or Wind River Diab C Compiler 5

CompCert C provides its own core compiler, of course, but relies on an external toolchain for preprocessing, assembling and linking. For simplicity, the external preprocessor, assembler and linker are invoked through the gcc driver command (for GCC) or dcc driver command (for Diab C). It is recommended to use a recent version of GCC.

Cross-compilation (e.g. generating PowerPC code from an x86 host) is possible but requires the installation of a matching GCC or Diab cross compiler and cross libraries.

For a Debian or Ubuntu GNU/Linux host, install the gcc package for native compilation, or a package such as gcc-powerpc-linux-gnu for cross-compilation.

For a Microsoft Windows host, install the Cygwin development environment from https://www.cygwin.com/. Alternatively, you can install WSL, the Windows Subsystem for Linux, https://aka.ms/wsl, and use it like a GNU/Linux host.

For hosts running macOS 10.9 or newer install the command line tools via xcode-select --install in the Terminal application. The installation of the Xcode IDE is optional.

Standard C library and header files

CompCert C does not provide its own implementation of the C standard library, relying on the standard library and header files of the host system.

For a Debian or Ubuntu GNU/Linux host, install the libc6-dev packages. If you are running a 64-bit version of Debian or Ubuntu and a 32-bit version of CompCert, also install libc6-dev-i386.

Under macOS, the command line tools installed via xcode-select --install also install the required libraries and header files.

2.3 Installation

Unpacking  Unpack the .tgz archive from a terminal window:

    tar xzf compcert-version-number.tgz
    cd compcert-version-number

Configuration  Run the configure script with appropriate options:

The mandatory target argument identifies the target platform. It must be one of the following:

See section 1.4.1 for more information on the supported platforms. For ARM targets, the arm- or armeb- prefixes can be refined into:

The default arm- and armeb- prefixes correspond to armv7a- and armebv7a- respectively.

For PowerPC targets, the ppc- prefix can be refined into:

The default ppc- prefix corresponds to PowerPC 32 bits.

For x86 targets in 32-bit mode, ia32- is recognized as synonymous for x86_32-.

For x86 targets in 64-bit mode, amd64- is recognized as synonymous for x86_64-.

The configure script recognizes the following options:

-bindir dir

Install the compiler’s executable ccomp in directory dir. The default location is /usr/local/bin.

-libdir dir

Install the compiler’s supporting library and header files in directory dir. The default location is /usr/local/lib/compcert.

-sharedir dir

Install the shared configuration file compcert.ini in directory dir. The default location is bindir/../share/ where bindir is the directory containing the compiler’s executable ccomp.

-prefix dir

Equivalent to “-bindir dir/bin -libdir dir/lib/compcert”.

-toolprefix pref

Prefix the name of the external C compiler driver (gcc or dcc) with pref. This option is particularly useful if a cross-compiler is used. For example:

• If the gcc executable to use is not contained in the search path, but in the directory /opt/local/powerpc-linux-gnu, give the option
  -toolprefix /opt/local/powerpc-linux-gnu/ (note the trailing slash).
• If the gcc executable to use can be found in the search path, but is called powerpc-linux-gnu-gcc, give the option
  -toolprefix powerpc-linux-gnu- (note the trailing dash).

-no-runtime-lib

Do not compile, install, and use the libcompcert library that provides helper functions for 64-bit integer arithmetic and for variable-argument functions. By default, this library is installed and linked with CompCert-generated executables. If it is not, some operations involving 64-bit integers (e.g. division, remainder, conversion to/from floating-point numbers) or variable arguments (e.g. the va_next macro) may not work.

-no-standard-headers

Do not install the CompCert-specific standard header files. By default, the following standard header files are installed and used: <float.h>, <stdarg.h>, <stdbool.h>, <stddef.h>, <stdnoreturn.h>, <iso646.h>, and <varargs.h>.

-use-external-Flocq

Use an already-installed version of the Flocq Coq library. By default, the version of the library used is the one included in the CompCert source distribution.

-use-external-Menhirlib

Use an already-installed version of the MenhirLib Coq library. By default, the version of the library used is the one included in the CompCert source distribution.

After successful completion, the configure script generates a configuration file Makefile.config and prints a summary of the configuration. If anything looks wrong, re-run ./configure with different options, or edit Makefile.config by hand.

Building the system  From the same directory where ./configure was executed, issue the command

    make all

or, on a N-core machine, to take advantage of parallel compilation:

    make -j N all

This re-checks all the Coq proofs, then extracts Caml code from the Coq specification and combines it with supporting hand-written Caml code to generate the executable for CompCert. This step can take about 15 minutes on a recent machine with a single core, less if several cores are used.

Installation  CompCert is now ready to be installed. This will create the ccomp command (documented in chapter 3) in the binary directory selected during configuration, and install supporting .h and .a files in the library directory if needed. Become superuser if necessary and do make install.