Rob, Rob Arthan wrote:
RC2 is working fine for ProofPower. I am testing on Snow Leopard using SVN rev 924 of the Poly/ML source. I tried both x86_64 and i386 architectures - to get the latter work you still seem to have to specify CXXFLAGS etc. I see that configure is still using xmkmf to test for X windows and therefore not finding it.
I think any change here needs to wait for updates to autoconf. I'd prefer not to put any special tests in myself.
However while hamlet compiles and runs OK with poly compiled for the 32 bit architecture, it compiles but fails with a bus error with the 64 bit architecture. I believe I configured the Makefile correctly - I adjusted the settings for POLY_LIBDIR and added the appropriate -arch option to the step where it links the executable. I've appended the output from the dynamic linker and gdb:
rda]- DYLD_PRINT_LIBRARIES= hamlet dyld: loaded: /Users/rda/bld/hamlet-1.3.1/./hamlet dyld: loaded: /usr/local/poly/x86_64/lib/libpolyml.1.dylib dyld: loaded: /usr/lib/libstdc++.6.dylib dyld: loaded: /usr/lib/libSystem.B.dylib dyld: loaded: /usr/lib/system/libmathCommon.A.dylib Bus error
This is on Mac OS X. I think you probably missed off the -segprot POLY rwx rwx from the link step. Try that and see if it fixes the problem. It builds and runs fine on 64-bit Linux.
I think once 5.3 is released I'll have a go at separating out the code from the mutable data when exporting and then it will be possible to use the conventional "text" (execute-read) and "data" (read-write) segments. That isn't possible at the moment because profiling, at least, writes into the code segments.
Regards, David