compcert

Formally verified C compiler
http://compcert.inria.fr

Current version
3.1

compcert requires the following formulae to be installed:
coq 8.6.1_1 Proof assistant for higher-order logic
menhir 20170712 LR(1) parser generator for the OCaml programming language
ocaml 4.05.0 General purpose programming language in the ML family

Formula history

Benjamin Beurdouche compcert 3.1
ilovezfs compcert: revision for ocaml
ilovezfs compcert: revision for ocaml
ilovezfs compcert: depend on coq
Benjamin Beurdouche Compcert 3.0.1
Benjamin Beurdouche compcert 3.0
ilovezfs compcert: build with Coq 8.5pl3 from OPAM
ilovezfs compcert 2.7.1
ilovezfs compcert 2.7
ilovezfs compcert: fix ocaml 4.03.0 induced build failure
Show all revisions of this formula