Stream: Coq devs & plugin devs

Topic: coqc hangs on QED with latest MacOS/Xcode - works fine with


view this post on Zulip Michael Soegtrop (May 06 2024 at 13:10):

I see really weird things going on on MacOS. There have been various reports that some Coq Platform things don't compile on MacOS Sonoma >= 14.3.X, I updated today and can reproduce this. It is not a stack overflow, but an invalid pointer access in coq-relation-algebra.

I have an even weirder case: one of my proofs hangs on QED with latest MacOS and did work fne before.

Now I kept my old .opam folder, and when I use the old switches, it still works fine, but the new one doesn't. So this is likely not a MacOS problem, but an XCode problem.

Any thoughts?

I try to downgrade XCode and/or try a different C compiler (gcc).

view this post on Zulip Michael Soegtrop (May 06 2024 at 13:11):

Should I ask in the OCaml forum if others see strange things?

view this post on Zulip Matthieu Sozeau (May 06 2024 at 13:15):

I think that sounds like an OCaml/xcode issue indeed

view this post on Zulip Michael Soegtrop (May 06 2024 at 13:29):

It must be a rather contrived issue, though, if so much works. Maybe it is something in memory management libraries or so.

view this post on Zulip Michael Soegtrop (May 06 2024 at 13:29):

I am currently building with gcc13 (or at least I hope so).

view this post on Zulip Michael Soegtrop (May 07 2024 at 08:57):

An Update on this: it seems to be Xcode. Xcode 14.3.1 works, Xcode 15.X not (I tested all 15.X versions).

view this post on Zulip Jason Gross (May 07 2024 at 16:00):

Is it worth trying to minimize this with the bug minimizer?

view this post on Zulip Michael Soegtrop (May 08 2024 at 07:43):

@Jason Gross The file which eventually fails is not long and fails quickly (a second or so), but if you can create a one file failure, it would certainly help reporting this.

One major issue with this is that 14.3.1 cannot be used to compile UI libraries on current MacOS (more a MacPorts policy thing than something real), so I need to switch compilers hence and forth during Coq Platform build - not yet sure how to do this.

view this post on Zulip Jason Gross (May 08 2024 at 13:10):

The bug minimizer inlines dependencies. If you can replicate on GH Actions macos arm64 runners, we can have GH Actions minimize it, or you can run the minimizer locally. Is there any issue with doing this?

view this post on Zulip Michael Soegtrop (May 08 2024 at 15:13):

Is there any issue with doing this?

I never used it. I will have a look at the doku. If I can't make it work I will ping you.

view this post on Zulip Michael Soegtrop (May 08 2024 at 16:19):

@Jason Gross : I found a few papers and repos about it, but nothing which explains how to run it locally.

view this post on Zulip Jason Gross (May 08 2024 at 17:27):

There's some instructions at https://github.com/JasonGross/coq-tools?tab=readme-ov-file#usage

view this post on Zulip Jason Gross (May 08 2024 at 17:28):

Plausibly the easiest way to install is by downloading the standalone binary (coq-bug-mininizer-os) from a release, though it's also on pip as coq-tools

view this post on Zulip Jason Gross (May 08 2024 at 17:34):

I guess I should update the readme with a bit more info, but the other bits of missing info are:


Last updated: Oct 13 2024 at 01:02 UTC