AbsInt / CompCert

The CompCert formally-verified C compiler
https://compcert.org
Other
1.85k stars 225 forks source link

a patch to Makefile.menhir for ocaml-non-native architctures. #502

Closed yozot closed 1 month ago

yozot commented 1 year ago

OpenBSD ports recently updated CompCert to 3.13, but does not work for ocaml-non-native architectures. The problem comes from Makefile.menhir expecting either menhirLib.cmxa or .cmx is available. It assumes ocaml native compilation environment.

This patch adds one more condition using OCAML_NATIVE_COMP which is prepared by configure, to adjust MENHIR_LIBS according to ocaml-native or ocaml-non-native environment. I confirmed this patch works in OpenBSD ports, and believe it's useful for any other environments.

xavierleroy commented 1 month ago

Thanks for the patch and apologies for the late reply. I think that with recent enough versions of Menhir the issue goes away, because the library is always menhirLib.cmxa or menhirLib.cma, but no longer menhirLib.cmx nor menhirLib.cma. Then, the general .cmxa -> .cma rule for bytecode-only builds in Makefile.extr handles the situation. Or so it seems on my test.

I'm closing this PR, but please do comment if I missed something.