I?ve been looking into getting HOL4 working with Poly/ML 5.6 (Git version 8592e2a) on Mac OS 10.11.2 with Xcode 7.2.
When trying to build Poly/ML with
./configure --enabled-shared
I got
ld: illegal text-relocation to 'assign_word' in .libs/x86asmtemp.o from '_entryPointVector' in .libs/x86asmtemp.o for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[2]: *** [libpolyml.la] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2
However, the build was successful with the default ./configure.
Once built there was a problem when calling polyc, as I was getting the error
ld: unknown option: -R/path/lib
Replacing
-Wl,-R${LIBDIR}
with
-Wl,-rpath ${LIBDIR}
seemed to work (things also worked when I deleted this option). I was then able to build HOL4.
The warning message
ld: warning: could not create compact unwind for _ffi_call_unix64: does not use RBP or RSP based frame
seems to be back, i.e. it doesn?t go away with -Wl,-no_pie. I?m not sure of the best way to silence this message. I?ve ended up adding -w to EXTRALDFLAGS.
Thanks, Anthony