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

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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

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 --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.

Reply | Threaded
Open this post in threaded view
|

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

Daniel Dickman


> On Feb 15, 2020, at 11:23 AM, Charlene Wendling <[hidden email]> 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.