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 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?

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

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

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

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 > {

[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 =