The latest release of the CompCert C compiler is version 2.7, released in June 2016. See here for a description of this compiler. Changes from earlier releases are summarized here. Earlier releases can be found here. The current state of the development can be viewed on Github.
Download the source code:
Compcert C version 2.7 (for Coq 8.4)
or Compcert C version 2.7.1 (for Coq 8.5).
(Check integrity with the SHA1 checksums.)
Download the user's manual in PDF or browse it online.
The sources compile and run on the following platforms:
- Intel and AMD x86 processors (with SSE2), under Linux, MacOS X, or Windows with Cygwin.
- PowerPC / Linux machines.
- ARM / Linux machines (tested on Raspberry Pi and Cubie Truck machines).
To compile, you will need:
- The Coq proof assistant version 8.4pl1 to 8.4pl6 (for CompCert 2.7) or version 8.5pl2 (for CompCert 2.7.1), available from coq.inria.fr or prepackaged in OPAM, MacPorts, and many Linux distributions.
- The OCaml functional language, version 4.02 or later, available from caml.inria.fr or prepackaged in OPAM, MacPorts, and many Linux distributions.
- The Menhir parser generator version 20160303 or later, available from Inria or prepackaged in OPAM.
Refer to the user's manual for installation instructions.
The CompCert C compiler is not free software. This public release can be used for evaluation, research and education purposes, but not for commercial purposes. See the License for more information. The AbsInt company sells a version of CompCert that has no such restrictions and can be used for commercial purposes. Contact email@example.com for more information.
For questions and feedback about the CompCert C compiler, please contact
Browse the Coq development
The Coq development can also be browsed online.