compcert

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

Current version
3.1

compcert requires the following formulae to be installed:
menhir 20171013_1 LR(1) parser generator for the OCaml programming language
ocaml 4.06.0 General purpose programming language in the ML family
ocaml-num 1.1 OCaml legacy Num library for arbitrary-precision arithmetic
opam 1.2.2_4 Package manager for OCaml

Formula history

ilovezfs compcert: depend on ocaml-num
ilovezfs compcert: build with Coq 8.6.1 from OPAM (#19742)
ilovezfs Use “squiggly” heredocs.
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
Show all revisions of this formula