Re: [ProofPower] Question about installation.

[Robert White]

Oh, okay. I will do it :) Thanks!

On 2 June 2015 at 16:38, Rob Arthan  wrote:

>
> > On 1 Jun 2015, at 21:31, Robert White 
> wrote:
> >
> > This is what I have now. Is this a correct version?
> >
> > Poly/ML 5.2 ReleaseRTS version: X86_64-5.2.1
>
> You need 5.5 or later. So you will need to build it from source.
> Don’t hesitate to ask if you need any help with that.
>
> Regards,
>
> Rob.
>
>


-- 

Regards,
Robert White (Shuai Wang)
INRIA Deducteam 
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Question about installation.

[Rob Arthan]

> On 1 Jun 2015, at 21:31, Robert White  wrote:
> 
> This is what I have now. Is this a correct version?
> 
> Poly/ML 5.2 ReleaseRTS version: X86_64-5.2.1

You need 5.5 or later. So you will need to build it from source.
Don’t hesitate to ask if you need any help with that.

Regards,

Rob.


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

Re: [ProofPower] Question about installation.

[Robert White]

Dear Rob,

Sorry about this late reply.
I installed it from apt-get . I am not familiar with PolyML. Do you
recommend to uninstall polyml from apt-get and install it again from source?

Cheers
Robert

On 28 May 2015 at 07:24, Rob Arthan  wrote:

> Robert,
>
> > On 27 May 2015, at 21:52, Robert White 
> wrote:
> >
> > Dear all,
> >
> > I have the following errors while installing. It doesn't seem that
> google give me much help on solving this problem.
> >
> > Can anyone help please?
> >
> >
> > [ -d   "/home/robert/pp" ] || mkdir "/home/robert/pp"
> > [ -d   "/home/robert/pp"/bin ] || mkdir "/home/robert/pp"/bin
> > {   { echo "val product_version : string = \"3.1w5\"; val copyright
> : string = \"Copyright (c) Lemma 1 Ltd. 2008\"; use\"dtd108.sml\";
> use\"imp108.sml\";" | poly ; } && { polyc  -o slrp-ml pp-ml.o ||
> LD_RUN_PATH=/usr/lib c++  -o slrp-ml pp-ml.o -L/usr/lib -lpolymain -lpolyml
> ; } && { echo "PPBuild.pp'save_name := \"slrpdb\"; PPBuild.pp'save ();" |
> slrp-ml ; }   }  > dtd108.ldd
> > /bin/sh: 1: polyc: not found
> > /usr/bin/ld: cannot find -lpolyml
> > collect2: error: ld returned 1 exit status
> > dev.mkf:334: recipe for target 'slrp-ml' failed
> > make: *** [slrp-ml] Error 1
>
>
> It looks like a problem either with the location or the version of you
> Poly/ML installation..
> What did the configure script report about Poly/ML? There may also be some
> more useful
> information in the file src/dev/dtd108.ldd.
>
> Regards,
>
> Rob.




-- 

Regards,
Robert White (Shuai Wang)
INRIA Deducteam 
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Question about installation.

[Rob Arthan]

Robert,

> On 27 May 2015, at 21:52, Robert White  wrote:
> 
> Dear all,
> 
> I have the following errors while installing. It doesn't seem that google 
> give me much help on solving this problem. 
> 
> Can anyone help please?
> 
> 
> [ -d   "/home/robert/pp" ] || mkdir "/home/robert/pp"
> [ -d   "/home/robert/pp"/bin ] || mkdir "/home/robert/pp"/bin
> {   { echo "val product_version : string = \"3.1w5\"; val copyright : 
> string = \"Copyright (c) Lemma 1 Ltd. 2008\"; use\"dtd108.sml\"; 
> use\"imp108.sml\";" | poly ; } && { polyc  -o slrp-ml pp-ml.o || 
> LD_RUN_PATH=/usr/lib c++  -o slrp-ml pp-ml.o -L/usr/lib -lpolymain -lpolyml ; 
> } && { echo "PPBuild.pp'save_name := \"slrpdb\"; PPBuild.pp'save ();" | 
> slrp-ml ; }   }  > dtd108.ldd
> /bin/sh: 1: polyc: not found
> /usr/bin/ld: cannot find -lpolyml
> collect2: error: ld returned 1 exit status
> dev.mkf:334: recipe for target 'slrp-ml' failed
> make: *** [slrp-ml] Error 1


It looks like a problem either with the location or the version of you Poly/ML 
installation..
What did the configure script report about Poly/ML? There may also be some more 
useful
information in the file src/dev/dtd108.ldd.

Regards,

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

[ProofPower] Question about installation.

[Robert White]

Dear all,

I have the following errors while installing. It doesn't seem that google
give me much help on solving this problem.

Can anyone help please?


[ -d   "/home/robert/pp" ] || mkdir "/home/robert/pp"
[ -d   "/home/robert/pp"/bin ] || mkdir "/home/robert/pp"/bin
{   { echo "val product_version : string = \"3.1w5\"; val copyright :
string = \"Copyright (c) Lemma 1 Ltd. 2008\"; use\"dtd108.sml\";
use\"imp108.sml\";" | poly ; } && { polyc  -o slrp-ml pp-ml.o ||
LD_RUN_PATH=/usr/lib c++  -o slrp-ml pp-ml.o -L/usr/lib -lpolymain -lpolyml
; } && { echo "PPBuild.pp'save_name := \"slrpdb\"; PPBuild.pp'save ();" |
slrp-ml ; }   }  > dtd108.ldd
/bin/sh: 1: polyc: not found
/usr/bin/ld: cannot find -lpolyml
collect2: error: ld returned 1 exit status
dev.mkf:334: recipe for target 'slrp-ml' failed
make: *** [slrp-ml] Error 1

Thanks very much!
-- 

Regards,
Robert White (Shuai Wang)
INRIA Deducteam 
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com