The latest release of the CompCert C compiler is version 2.4, released in September 2014. See here for a description of this compiler. Changes from earlier releases are summarized here. Earlier releases can be found here.
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 a Trimslice machine).
To compile, you will need:
- The Coq proof assistant version 8.4pl1 or 8.4pl2 or 8.4pl3 or 8.4pl4 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, available from Inria or prepackaged in OPAM, MacPorts, and many Linux distributions.
Refer to the user's manual for installation instructions.
The CompCert C compiler is not free software. This release can be used for evaluation, research and education purposes, but not for commercial purposes. See the License 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.