My goal is to be able to use CompCert, a certified compiler.
It is a compiler whose passes are formally verified to not introduce change in the semantics from the C code to its translation in asm.
The installation goals
Compcert is installed from its Coq sources. So i need Coq.
Coq is installed from sources or as an OPAM package. OPAM being the Ocaml PAckage Manager.
opam needs OCaml anyway. So I need OCaml.
OCaml is installable through OPAM or from sources.
The easiest part
Porting OCaml was not too hard: copying most of Linux configuration in the configure{.ac} files work as is.
Don’t forget to add some platform detection in config.guess, and some libraries tweaking:
