Stream: Coq devs & plugin devs

Topic: Ocaml 4.07.1 fails to compile with Apple XCode 12


view this post on Zulip Michael Soegtrop (Sep 17 2020 at 12:19):

I just updated (or gut updated) to XCode 12. Among other things (like remake @Guillaume Melquiond is using) it breaks the OCaml base compiler 4.07.1 - my current pick for the Coq platform. It ends with:

Fatal error: exception Invalid_argument("Sys.getcwd not implemented")

any suggestions what I could do about this? The make log looks a bit bizarre and I have difficulties to see where the error happens.

view this post on Zulip Michael Soegtrop (Sep 17 2020 at 12:59):

P.S.: OCaml 4.11.1 does build with XCode 12. But as far as I have heard it is not ideal for Coq cause of some issues with changes in linking of dynamic libraries?

view this post on Zulip Karl Palmskog (Sep 17 2020 at 13:02):

@Michael Soegtrop the issues with >= 4.08 break down to: (1) linking issue, and (2) performance issues. To my knowledge, these are near orthogonal.

view this post on Zulip Michael Soegtrop (Sep 17 2020 at 13:04):

I see. I will first do a platform build with 4.11.1 and XCode 12. If this gets reasonably far, I will try to fix 4.07.1 - shouldn't be a big thing then.

view this post on Zulip Karl Palmskog (Sep 17 2020 at 13:08):

so basically XCode has its own compiler? I thought everything was some basic Clang-whatnot

view this post on Zulip Michael Soegtrop (Sep 17 2020 at 13:48):

Afaik XCode is derived from clang but I think the libraries are different. The issue with remake was that there was some funny definition of log which messed up the use of a structure names log.
For OCaml 4.07.1 it seems to be some configure issuse - some basic system functions are not found.

view this post on Zulip Michael Soegtrop (Sep 17 2020 at 14:48):

I got an opam patch for this - some additional arguments to configure. Luckily I can register my local coq platform patch repo already during switch creation, so that opam picks it up when compiling OCaml.


Last updated: Oct 16 2021 at 07:02 UTC