> On Feb 15, 2020, at 11:23 AM, Charlene Wendling <[email protected]> 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 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 --version | awk '{print $NF}'`.
> - coqc(1) on powerpc and aarch64 outputs:
>
> $ coqc
> Fatal error: cannot load shared library dllnums
> Reason: File not found
>
> ... and i did not find a replacement
>
> I know nothing about the whole ocaml environment and if coqc can be run
> on !ocaml_native_dynlink archs, so i let you three decide the proper
> course of action :)
>
> Charlène.
