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).
Should I ask in the OCaml forum if others see strange things?
I think that sounds like an OCaml/xcode issue indeed
It must be a rather contrived issue, though, if so much works. Maybe it is something in memory management libraries or so.
I am currently building with gcc13 (or at least I hope so).
An Update on this: it seems to be Xcode. Xcode 14.3.1 works, Xcode 15.X not (I tested all 15.X versions).
Is it worth trying to minimize this with the bug minimizer?
@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.
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?
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.
@Jason Gross : I found a few papers and repos about it, but nothing which explains how to run it locally.
There's some instructions at https://github.com/JasonGross/coq-tools?tab=readme-ov-file#usage
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
I guess I should update the readme with a bit more info, but the other bits of missing info are:
-f path/to/_CoqProject
to get it to register dependenciesGoal True. idtac "File ""./<name>.v"", line <total lines in file>, characters 0-0:"; idtac "Error:". Abort.
at the top of the file, cf https://github.com/JasonGross/coq-tools/issues/100#issuecomment-983989844)Last updated: Oct 13 2024 at 01:02 UTC