An odyssey to port compcert | Haiku Project

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.

This is a companion discussion topic for the original entry at

Good luck to add/enable your fav compiler to Haiku!


You are probably aware but there was a port of ocaml to haiku before. It even has somewhat working haiku bindings. Perhaps it is outdated or not fully working, though.

It will be great to have compcert available. A truly impressive piece of engineering.

Had to follow the link to the blog post to see from who this was (the gtksourceview4 should have gave that away when I saw it) :slight_smile: Congrats on the progress @Anarchos ! :+1:

Long road ahead…

Yes, but the recent versions of ocaml have disabled the native compilation, which is mandatory to compile coq. So i have to rebuild myself the OCaml compiler with native compilation enabled.

Thanks Begasus, i could not have compiled gtksourceview3 without your help.