Coq build issues in F32
I've been talking to Richard Jones about this privately, and he
suggested that a message to fedora-devel could be helpful.
I've been talking for weeks about updating the entire coq stack,
badgering people into swapping reviews with me, etc. Today I finally
had all the bits in place to do the updates. I built the whole stack
for Rawhide with no issues.
The same builds need to happen for F32, where parts of the stack
currently have broken deps. But I can't get coq to build
successfully, even though it did in Rawhide. It went like this:
Attempt 1: the x86_64 build segfaulted while running "bin/coqc -coqlib . -q
-native-compiler yes theories/FSets/FMapFullAVL.v", where coqc is a
binary built from the coq sources. Coq is a theorem prover. The coqc
run is essentially checking that a series of proof steps indeed prove
a theorem. The "-native-compiler yes" part means that the OCaml
compiler will be invoked to generate native code for parts of this
process.
I was puzzled by the segfault. I decided to see if the segfault is
deterministic, so I launched...
Attempt 2: the x86_64 build succeeded. The s390x build failed with an
illegal instruction error while running *the same command*.
Attempt 3: The s390x build again failed with an illegal instruction
error while running the same command, and aarch64 segfaulted while
running the same command. All other arches succeeded. I saved the
URL for this one:
https://koji.fedoraproject.org/koji/taskinfo?taskID=42768075
Either I got lucky when I launched the Rawhide build, or something is
fundamentally different between F32 and Rawhide. Clearly something
nondeterministic is at work. I have been unable to reproduce this
failure in mock so far, but will keep trying.
If anybody has any ideas, I am all ears. Thank you,
--
Jerry James
http://www.jamezone.org/