This chapter explains how to install 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.
The following software components are required to build, install, and execute the CompCert C compiler.
For all systems, the recommended way to install these three prerequisites is to use OPAM, the OCaml Package Manager, available from http://opam.ocaml.org/. (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.07.1 # Use OCaml version 4.07.1 eval `opam env` opam install coq=8.11.2 # Use Coq version 8.11.2 opam install menhir
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 http://www.cygwin.com/.
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.
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.
Unpack the .tgz archive from a terminal window:
tar xzf compcert-version-number.tgz cd compcert-version-number
Run the configure script with appropriate options:
The mandatory target argument identifies the target platform. It must be one of the following:
|ppc-eabi||PowerPC, EABI, with GNU or Unix tools|
|ppc-eabi-diab||PowerPC, EABI, with Diab tools|
|arm-eabi||ARM, EABI, default calling conventions, little endian|
|arm-linux||synonymous for arm-eabi|
|arm-eabihf||ARM, EABI, hard floating-point calling conventions, little endian|
|arm-hardfloat||synonymous for arm-eabihf|
|armeb-eabi||ARM, EABI, default calling conventions, big endian|
|armeb-linux||synonymous for armeb-eabi|
|armeb-eabihf||ARM, EABI, hard floating-point calling conventions, big endian|
|armeb-hardfloat||synonymous for armeb-eabihf|
|aarch64-linux||AArch64 (ARMv8 in 64-bit mode), Linux|
|x86_32-linux||x86 32 bits (IA32), Linux|
|x86_32-bsd||x86 32 bits (IA32), BSD|
|x86_32-cygwin||x86 32 bits (IA32), Cygwin environment under Windows|
|x86_64-linux||x86 64 bits (AMD64), Linux|
|x86_64-macosx||x86 64 bits (AMD64), macOS|
|x86_64-cygwin||x86 64 bits (AMD64), Cygwin environment under Windows|
|rv32-linux||RISC-V 32 bits, Linux|
|rv64-linux||RISC-V 64 bits, Linux|
See section 1.4.1 for more information on the supported platforms. For ARM targets, the arm- or armeb- prefixes can be refined into:
|armv6-||Little Endian ARMv6 architecture with VFPv2 coprocessor|
|armv7a-||Little Endian ARMv7-A architecture with VFPv3-D16 coprocessor|
|armv7r-||Little Endian ARMv7-R architecture with VFPv3-D16 coprocessor|
|armv7m-||Little Endian ARMv7-M architecture with VFPv3-D16 coprocessor|
|armebv6-||Big Endian ARMv6 architecture with VFPv2 coprocessor|
|armebv7a-||Big Endian ARMv7-A architecture with VFPv3-D16 coprocessor|
|armebv7r-||Big Endian ARMv7-R architecture with VFPv3-D16 coprocessor|
|armebv7m-||Big Endian ARMv7-M architecture with VFPv3-D16 coprocessor|
The default arm- and armeb- prefixes correspond to armv7a- and armebv7a- respectively.
For PowerPC targets, the ppc- prefix can be refined into:
|ppc64-||PowerPC 64 bits|
|e5500-||Freescale e5500 core (PowerPC 64 bits with EREF extensions)|
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:
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.
From the same directory where ./configure was executed, issue the command
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.
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.