yices2 icon indicating copy to clipboard operation
yices2 copied to clipboard

Poor test results on PowerPC: how to improve/fix?

Open barracuda156 opened this issue 2 years ago • 6 comments

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.

tests_10.6.8_Rosetta_ppc32.txt

barracuda156 avatar Dec 27 '22 16:12 barracuda156

Try to compile statically and in debug mode. For example:

make static-check MODE=debug

will run all the tests with assertions enabled.

BrunoDutertre avatar Dec 28 '22 10:12 BrunoDutertre

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.

barracuda156 avatar Dec 28 '22 14:12 barracuda156

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.

BrunoDutertre avatar Jan 07 '23 01:01 BrunoDutertre

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.

barracuda156 avatar Jan 07 '23 01:01 barracuda156

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.

BrunoDutertre avatar Jan 07 '23 02:01 BrunoDutertre

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 :)

barracuda156 avatar Jan 07 '23 02:01 barracuda156