Re: [powerpc/aarch64] lang/ocaml+math/coq vs lang/compcert

2020-02-15 Thread Daniel Dickman
> On Feb 15, 2020, at 11:23 AM, Charlene Wendling wrote: > > Hi, > > I was looking at the lang/compcert failure on powerpc and aarch64, Thanks for looking into. Please go ahead and remove aarch64 and powerpc from compcert’s ONLY_FOR_ARCHS. > and > found that configure fails on these

[powerpc/aarch64] lang/ocaml+math/coq vs lang/compcert

2020-02-15 Thread Charlene Wendling
Hi, I was looking at the lang/compcert failure on powerpc and aarch64, and found that configure fails on these archs for two reasons after looking at compcert's configure, then at the ocaml port: - ocamlopt(1) is not available on !ocaml_native_dynlink archs, it could be replaced by `ocaml