Roger,
> On 29 Apr 2016, at 17:17, Roger Bishop Jones <[email protected]> wrote:
>
> 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?
The linker can’t find the gmp library. What version of Poly/ML are you using?
Did you build
it yourself or download it ready-made from somewhere?
If you go into src/dev, what happens if you run the following command
interactively?
polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
Regards,
Rob.
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
