Clang support?

[brad0]

Looking at Compcert I'm trying to clarify if this project absolutely requires GCC or if it should work with Clang?

[didickman]

Hello Xavier and team. For context Brad is looking at the OpenBSD CompCert package and is interested in seeing whether the gcc requirement could be switched to clang. I’ve already pointed him to section 2.2.2 in the manual which states that gcc or diab are required. Although given his interest in clang I’d suggested he could also check with you if there was any appetite to support clang. OpenBSD has mostly switched to clang on platforms that support it. Although gcc and gnu binutils remain available for packages that need them. All the best and happy holidays.

[xavierleroy]

I would expect CompCert to work fine with Clang, with two caveats: 1- CompCert invokes gcc or targetname-gcc to perform preprocessing, assembling, and linking. This may need to be changed to clang or to cc to fit your use case. 2- For development and CI, we use GCC for Linux and Windows and Clang for macOS. So, Clang is tested for x86-64 and for aarch64, but has never been tested for PowerPC, say.

Why not give it a try and let us know how it goes?

[didickman]

Thank you. Will take some time but we will try 32-bit/64-bit x86 and aarch64 on OpenBSD. Last I checked, PowerPC does build here although looked like it needs some minor fix at runtime. I do not have access to powerpc64 or riscv boxes although the project does, so we may be able to test those too. (Will need to check if ocaml and coq are built on those platforms though).