yices2
yices2 copied to clipboard
Poor test results on PowerPC: how to improve/fix?
I am bringing yices
into Macports, and we maintain support for older macOS there. With minimal fixes to build system, I have built yices
for ppc32
on 10.6.8. However, while the build is successful, test results are dismal:
Pass: 128
Fail: 869
P. S. I made no modifications to the code itself – then only thing I had to fix was adding support for powerpc-apple-darwin
to ARCH.
Try to compile statically and in debug mode. For example:
make static-check MODE=debug
will run all the tests with assertions enabled.
Try to compile statically and in debug mode. For example:
make static-check MODE=debug
will run all the tests with assertions enabled.
@BrunoDutertre Thank you, will try that.
By the way, on MacOS x86_64 static targets do not build at all: https://github.com/macports/macports-ports/pull/17078#issuecomment-1366074386
On PPC they did, though I had to add -read_only_relocs suppress
ldflag.
Static builds work fine for me on x86_64 (and have for a long time). No special flag required. The main issue is building GMP in PIC mode.
Static builds work fine for me on x86_64 (and have for a long time). No special flag required. The main issue is building GMP in PIC mode.
I looked into the docs, it appears that it needs three versions of gmp
, which is highly problematic. Not that it is impossible to implement in Macports, but it is hardly justified, and I am not sure such intrusive change will be welcomed.
The three versions is only for windows. On other platforms, you can build GMP once in PIC mode. You'll have libgmp.a for linking statically and libgmp.dylib for linking dynamically.
The three versions is only for windows. On other platforms, you can build GMP once in PIC mode. You'll have libgmp.a for linking statically and libgmp.dylib for linking dynamically.
Well, then maybe we can make a variant of libgmp
port to install in a separate location and then use it --with-pic-gmp=
. Not something convenient, but doable :)