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
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:
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: *** [Makefile.build:880: theories/FSets/FMapFullAVL.vo] Illegal instruction (core
make: *** [theories/FSets/FMapFullAVL.vo] Deleting file
make: 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
Associate Professor Division of Policy and Planning Science
Faculty of Systems and Information
Email: turnbull(a)sk.tsukuba.ac.jp University of Tsukuba
Tel: 029-853-5175 Tennodai 1-1-1, Tsukuba 305-8573 JAPAN