An odyssey to port compcert

Blog post by Anarchos on Tue, 2024-04-09 09:44

The goal 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.