The latest release of the CompCert C compiler is version 2.5, released in June 2015. 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.
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 or 8.4pl2 or 8.4pl3 or 8.4pl4 or 8.4pl5, available from coq.inria.fr or prepackaged in OPAM, MacPorts, and many Linux distributions.
- The OCaml functional language, version 4.00 or later, available from caml.inria.fr or prepackaged in OPAM, MacPorts, and many Linux distributions.
- The Menhir parser generator version 20140422 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 firstname.lastname@example.org 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.