test failure bugs/closed/bug_5127.v on s390x

[treinen]

Description of the problem

On the s390x architecture, the test case bugs/closed/bug_5127.v fails, see here for a complete log of the compilation. Among the ~10 architectures on which compilation of coq is finished so far this is the only architecture where this failure occurs.

Coq Version

8.10.2

[ppedrot]

See #5127.

[ppedrot]

I don't think that any coqdev has a mainframe to play with, unfortunately. Are the debian packages compiled on an emulator, or on a real machine?

[SkySkimmer]

You should run the test suite with PRINT_LOGS=1 to get the specific failing log.

[treinen]

In this case the build was done on a real IBM machine (specs of zani.debian.org). The machines running the build demons are restricted and I cannot log into them, but as debian developer I have access to a different s390x box which does not have exactely the same processor. I can try to reproduce the failure on that machine using PRINT_LOGS=1 as @SkySkimmer suggested. The question is : are you interested in these kind of failures? Otherwise I can in the debian package just skip this test.

[ppedrot]

This error is likely to be caused by C code, so it's either due to some non-portable code from the VM, a VM abuse of an implementation-specific behaviour of the C compiler, or who knows even a bug in the compiler itself. The architecture is fairly exotic, so I think that disabling the test is the fastest strategy. A variant of the Drake equation taking into account the potential number of Coq-s390x users, of Coq-s390x developers, and relativized to the actual overall Coq dev time doesn't seem much in favour of the possibility of the creation of a fix soon.

Anyways, we need to ping @coq/vm-native-maintainers for more input.

[maximedenes]

• Do we support this architecture?
• Are there users for it? (I mean Coq users)

[treinen]

Thanks @ppedrot. Just ping me if you need further tests on that architecture.

[rwmjones]

There's a bit more information about this including stack traces and disassembly on the following Fedora bug: https://bugzilla.redhat.com/show_bug.cgi?id=1874249#c2