Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Roger Bishop Jones 
Magic.

Build complete.
I just had to change the path.

xpp seems to come up ok.

Thanks, I’ll post a resume.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Rob Arthan 
Roger,

> On 30 Apr 2016, at 15:55, Roger Bishop Jones  wrote:
> 
> Rob,
> 
> Now failing to find mkfontdir.
> 
> PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9
> 
> Am I missing something from the PATH or do I need to install something else?


I have it in /usr/X11R6/bin/mkfontdir, so it looks like you need /usr/X11/bin 
on your path.
If it’s not there, then you may need to install more from the XQuartz site.

Regards,

Rob.


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Roger Bishop Jones 
Rob,

Now failing to find mkfontdir.

PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9

Am I missing something from the PATH or do I need to install something else?

Roger


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Rob Arthan 
Roger,

> On 30 Apr 2016, at 10:43, Roger Bishop Jones  wrote:
> 
> Rob,
> 
> Thanks for you continuing support.

Not a problem. Thank you for persisting with this bit of the
installation, because I have a bit of difficulty testing it on
Mac OS in a clean environment. I will look into improving
the way I test it.

> 
>> On 30 Apr 2016, at 10:16, Rob Arthan > > wrote:
>> 
>> 
> 
> ...
> 
>> Try it in in src/dev. I think it will fail. If so, try it without the 
>> obsolete options:
>> 
>>  polyc -o pp-ml pp-ml.o
>> 
> 
> Here are the results:
> 
> bash-3.2$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
> bash-3.2$ polyc -o pp-ml pp-ml.o
> ld: warning: could not create compact unwind for _ffi_call_unix64: does not 
> use RBP or RSP based frame
> 
> So I need to build my own?

Hopefully not. That warning should be harmless.

I’ve just realised that it is only src/hol/hol.mkf which has this legacy way of
linking a poly executable. src/dev/dev.mkf creates slrp-ml the modern way
and will already have done that.

For the next step, I realise that you don’t need to edit thesrc/hol/hol.mkf:
to get it to call polyc correctly, run configure like this:

PPPOLYLINKFLAGS=“ “ ./configure

together with any other environment variable settings you need. I think there
is a good chance that the rest of the ML compilations will work then.

Regards,

Rob.

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Roger Bishop Jones 
Rob,

Thanks for you continuing support.

> On 30 Apr 2016, at 10:16, Rob Arthan  wrote:
> 
> 

...

> Try it in in src/dev. I think it will fail. If so, try it without the 
> obsolete options:
> 
>   polyc -o pp-ml pp-ml.o
> 

Here are the results:

bash-3.2$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
Only one source file name allowed
Usage: polyc [OPTION]... [SOURCEFILE]
bash-3.2$ polyc -o pp-ml pp-ml.o
ld: warning: could not create compact unwind for _ffi_call_unix64: does not use 
RBP or RSP based frame

So I need to build my own?

Roger___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-30 Thread Rob Arthan 
Roger,

> On 29 Apr 2016, at 23:16, Roger Bishop Jones  wrote:
> 
> Rob,
> 
>> On 29 Apr 2016, at 20:31, Rob Arthan  wrote:
>> 
>> 
>> 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?
>> 
> 
> I did:
>   port install polymer
> 
> poly -v gives
> 
> Poly/ML 5.5.2 ReleaseRTS version: X86_64-5.5.1
> 
> 
OK. You may need to build your own, but let's see if we can get it working
with the MacPorts version.

>> If you go into src/dev, what happens if you run the following command 
>> interactively?
>> 
> 
> src/dev where?  Can’r find one.

In the directory OpenProofPower-3.1w7 you got when you unpacked the tarball.
> 
> But if I run it in my home directory I get:
> 
> Rogers-MacBook:~ rbj$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o 
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
> 

Try it in in src/dev. I think it will fail. If so, try it without the obsolete 
options:

polyc -o pp-ml pp-ml.o

If that works, then if you get rid of those options from the polyc command
lines in src/dev/dev.mkf and src/hol/hol.mkf, you should get a bit further.

Regards,

Rob.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-29 Thread Roger Bishop Jones 
Rob,

> On 29 Apr 2016, at 20:31, Rob Arthan  wrote:
> 
> 
> 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?
> 

I did:
port install polymer

poly -v gives

Poly/ML 5.5.2 ReleaseRTS version: X86_64-5.5.1


> If you go into src/dev, what happens if you run the following command 
> interactively?
> 

src/dev where?  Can’r find one.

But if I run it in my home directory I get:

Rogers-MacBook:~ rbj$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o 
Only one source file name allowed
Usage: polyc [OPTION]... [SOURCEFILE]

Roger

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

2016-04-29 Thread Rob Arthan 
Roger,

> On 29 Apr 2016, at 17:17, Roger Bishop Jones  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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] ProofPower build on OS X

2016-04-29 Thread Roger Bishop Jones 
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