Hi Jerry! Long time no see. Jerry James writes: > I built the whole stack for Rawhide with no issues. Zero compiler warnings? No fiddling to suppress compiler warnings *anywhere* in the build chain (whether options or pragmas)? Not suggesting you go looking for pragmas (probably have 10 million lines of code :-( ), but you could check for warnings in the build logs. I didn't see any in the tail, though. > 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. Where is the segfault? Is it in coqc or is it in the generated code or is it in the OCaml compiler or is it somewhere else? If you can't rule out the OCaml compiler (or other parts of the OCaml toolchain) and the generated code: - what happens if you use -native-compiler=no? - How is the native code used? Compiled and linked as a .so, then dynamically loaded and called? Compiled and linked as an executable, then run as a separate process? If you can't rule out OCaml: does it produce native code directly, or does it produce C or similar and then use GCC or similar to produce the native code? What optimizations to gcc are being used where it's being used? Are other compilers (LLVM) supported in lieu of GCC for any parts of the build chain? > > 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 >From the tail of the S390 build log: rm -f theories/FSets/FMapFullAVL.glob bin/coqc -coqlib . -q -native-compiler yes theories/FSets/FMapFullAVL.v make[1]: *** [Makefile.build:880: theories/FSets/FMapFullAVL.vo] Illegal instruction (core dumped) make[1]: *** [theories/FSets/FMapFullAVL.vo] Deleting file 'theories/FSets/FMapFullAVL.glob' make[1]: Leaving directory '/builddir/build/BUILD/coq-8.11.0' make: *** [Makefile:177: submake] Error 2 That seems pretty unhelpful, as Makefile.build:880 is presumably just the rule that invokes bin/coqc, which evidently is actually a compiler driver that invokes various executables. Do you have access to the core that was allegedly dumped, to at least determine the identity of the executable that segfaulted? Is it possible to reproduce outside of Koji? Stay healthy! -- Associate Professor Division of Policy and Planning Science http://turnbull.sk.tsukuba.ac.jp/ Faculty of Systems and Information Email: turnbull@xxxxxxxxxxxxxxxx University of Tsukuba Tel: 029-853-5175 Tennodai 1-1-1, Tsukuba 305-8573 JAPAN _______________________________________________ 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
