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@xxxxxxxxxx> 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/coqpp/coqpp_parser.ml#L36 > > 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/c46c3bb8222dca716316841514ce91e864b83b13?branch=rawhide > > 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. -- Jerry James http://www.jamezone.org/ -- _______________________________________________ devel mailing list -- devel@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to devel-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/devel@xxxxxxxxxxxxxxxxxxxxxxx Do not reply to spam, report it: https://pagure.io/fedora-infrastructure/new_issue
