Sorry for the silence. I've been on vacation, returning to find a giant pile of work waiting for me. :-)
On Thu, May 30, 2024 at 3:01 AM Richard W.M. Jones rjones@redhat.com wrote:
Since flocq seems to have no public bug tracker, I might as well write my findings here ...
I believe the error is raised in this code:
https://github.com/coq/coq/blob/ac1e5ebd3f50a53b46cdb59225887841f5d24d02/coq...
I had a lot of trouble getting gdb to understand /usr/bin/coqc. Is it even a native code binary? As I couldn't place a breakpoint, I trapped on write system calls to fd=2, but no useful stack trace was forthcoming. I wonder if it's even a real stack overflow or some stack inside the parser?
However I did observe that /usr/bin/coqc.byte does not have the same problem (so perhaps it is the real stack). I added this very ugly workaround to get it to compile:
https://src.fedoraproject.org/rpms/flocq/c/c46c3bb8222dca716316841514ce91e86...
Also of note: OCaml 5.2 re-enables the ppc64le native code generator, which was previously disabled since OCaml 5, so perhaps this is a new bug in the OCaml compiler?
That would be my suspicion. I recently talked to OCaml upstream about a ppc64le code generation bug that I tripped over while attempting to update frama-c, and they mentioned that they were aware of a number of ppc64le bugs in 5.2.0. Hopefully 5.2.1 will sort many of them out.