2023.11.0 on Mac M2: coq-unicoq, coq-relation-algebra fail with seg fault

[andrew-appel]

I am not sure whether to report this here or on the coq-unicoq git, so I will report it here.

I am installing Coq Platform 8.18~2023.11 by opam built from sources, on a Mac M2 with 64 GB memory.

The build fails in installing coq-unicoq.1.6+8.18 with,

COQC test-suite/munifytest.v
make[1]: *** [test-suite/munifytest.vo] Segmentation fault: 11

And also fails in installing coq-relation-algebra.1.7.10 with,

make[1]: *** [theories/normalisation.vo] Segmentation fault: 11

This happens with or without parallel jobs (-j).

After commenting these (and mtac2 which depends on unicoq) out of the package-pick-8.18~2023.11.sh file, I was able to install the platform. (Is there a more elegant way to do this?)

[MSoegtropIMC]

Thanks for the report. This is rather odd since I am mostly testing / working on a M1 Max also with 64 GB and this works fine (I am usually using -j 6) . There shouldn't be differences between an M1 and M2 observable by coqc. I will re-test on my machine.

A few questions:

• what library manager do you use? Homebrew or MacPorts?
• what MacOS version do you use?
• what shell do you use (things like stack size limits might be shell specific, since e.g. ulimit is a shell built in)?

[andrew-appel]

Homebrew, macOS 14.3.1, zsh

[MSoegtropIMC]

@andrew-appel : can you please post the output of

ulimit -S -a
ulimit -H -a

[andrew-appel]

% ulimit -S -a
-t: cpu time (seconds)              unlimited
-f: file size (blocks)              unlimited
-d: data seg size (kbytes)          unlimited
-s: stack size (kbytes)             8176
-c: core file size (blocks)         0
-v: address space (kbytes)          unlimited
-l: locked-in-memory size (kbytes)  unlimited
-u: processes                       10666
-n: file descriptors                2560

% ulimit -H -a
-t: cpu time (seconds)              unlimited
-f: file size (blocks)              unlimited
-d: data seg size (kbytes)          unlimited
-s: stack size (kbytes)             65520
-c: core file size (blocks)         unlimited
-v: address space (kbytes)          unlimited
-l: locked-in-memory size (kbytes)  unlimited
-u: processes                       16000
-n: file descriptors                unlimited

[MSoegtropIMC]

Thanks - all as it should be. I am out of ideas here (still works for me on M1 Max). The only difference is that I am using MacPorts instead of Homebrew, but I am testing Homebrew regularly on my old Intel Mac. If it is a Homebrew issue, it must be ARM silicon specific.

I see a few options:

1.) You try with MacPorts, but this might be tricky. Unlike MacPorts (which lives under /opt/local) Homebrew is distributed in a few places and not trivial to remove or hide temporarily. 2.) We ask the Unicoq team if they have a M2 Mac to try 3.) You send me a coredump and I see what I can get out of this. Creating coredumps on Mac is said to be tricky, though. At the minimum you need to set the ulimit for core files (see above) to unlimited, but I have heard that more is required (I never tried).

It did btw. work in CI last time it did run (https://github.com/coq/platform/actions/runs/7982114209/job/21795066633#step:7:518) - the Mac CI got broken after a Github update 3 weeks back and I didn't manage to fix it as yet (but I think I know how to do it meanwhile - just no time to test it as yet). CI uses (or used) Homebrew + Intel.

[MSoegtropIMC]

I btw. don't see how Homebrew / MacPorts supplied libraries could have the effect that coqc crashes just for UniCoq.

[andrew-appel]

Perhaps we can just make the installation of those 3 packages optional in the Coq platform script.

[rongcuid]

This also fails on me with MacPorts:

...
∗ installed coq-paramcoq.1.1.3+coq8.18
∗ installed coq-itauto.8.18.0
∗ installed coq-gappa.1.5.4
∗ installed coq-mathcomp-finmap.1.5.2
∗ installed coq-coquelicot.3.4.0
∗ installed coq-simple-io.1.8.0
∗ installed coq-reglang.1.1.3
[ERROR] The compilation of coq-relation-algebra.1.7.10 failed at "make -j8".
∗ installed coq-mathcomp-fingroup.1.18.0
[ERROR] The compilation of coq-unicoq.1.6+8.18 failed at "make -j8".
...

[MSoegtropIMC]

@rongcuid : thanks for the additional data point!

[rtetley]

Weird, this seems to work for me on my M2 with Homebrew, macOS 13.4.1, zsh... Maybe it is macOS version specific ? I could update and try again afterwards ? Won't have time today though :-/

[MSoegtropIMC]

@andrew-appel : after a day of testing I found that this is not an issue with MacOS but with Xcode. Installing Xcode 14.3.1 at /Applications/Xcode_14.3.1.app and activating it for command line use via:

sudo xcode-select --switch /Applications/Xcode_14.3.1.app
hash -r

and recreating the switch (I also recompiled all MacPorts packages to be sure, but I don't think this is the issue) fixes the issue. The next published version of XCode, 15.0.1 and all newer versions don't work for me.

It likely also works to not use Xcode command lines tools (that is do sudo xcode-select --reset) and instead use a MacPorts / Homebrew supplied clang / gcc (still testing).

[MSoegtropIMC]

An update: using MacPorts supplied gcc and/or clang did not work. The only working configuration seems to be Xcode 14.3.1. MacPorts in general does not work well if no Xcode is supplied.

[MSoegtropIMC]

Apparently this needs a bit more work if one wants CoqIDE - some of the dependency packages of CoqIDE fail to compile via MacPorts with Xcode 14.3.1, but I believe this is just a sanity check of MacPorts rather than an actual issue. I see what I can do.

[MSoegtropIMC]

This has been fixed by updating to OCaml 4.14.2 in commit eeeabce7caaf94481d010ca6fc50ff32868b879a.