Rob, OK, so now I am through to the ProofPower build, which fails pretty fast, just after compiling dtd108.
Here’s the tail of the log: rm -f hol.polydb Compiling dtd108.sml and imp108.sml { { echo "val system_version : string = \"3.1w7\"; val build_date : Date.date = Date.fromTimeLocal(Time.now()); use\"dtd108.sml\"; use\"imp108.sml\";" | poly ; } && { polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o || LD_RUN_PATH=/opt/local/lib c++ -segprot POLY rwx rwx -o pp-ml pp-ml.o -L/opt/local/lib -lpolymain -lpolyml ; } && { echo "PPBuild.pp'save ();" | pp-ml ; } } > dtd108.ldd0 ld: warning: could not create compact unwind for _ffi_call_unix64: does not use RBP or RSP based frame Undefined symbols for architecture x86_64: "___gmpn_add_n", referenced from: add_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in libpolyml.a(arb.o) "___gmpn_gcd", referenced from: gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o) "___gmpn_gcd_1", referenced from: gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o) "___gmpn_lshift", referenced from: gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o) "___gmpn_mul", referenced from: mult_longc(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o) "___gmpn_rshift", referenced from: gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o) "___gmpn_sub_n", referenced from: sub_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in libpolyml.a(arb.o) "___gmpn_tdiv_qr", referenced from: quotRem(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*&, SaveVecEntry*&) in libpolyml.a(arb.o) ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make: *** [hol.ldd] Error 1 Any idea what the problem is here? Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com