On 21 Nov 2009, at 10:23, I wrote:

> On 21 Nov 2009, at 04:40, <m...@proof-technologies.com> 
> <m...@proof-technologies.com> wrote:
>> I've been trying to install ProofPower 2.8.1p2 on a very recent Ubuntu
>> ...

>> So far I've just been trying to get 'xpp' installed.  Having
>> installed tex, I tried configure:
>>   PPTARGETS="xpp" PPHOME=/home/dangdat/flyspeck/pp/pp-2.8.1p2
>> ./configure
>> To result in this:
>>   Using /home/dangdat/flyspeck/pp/pp-2.8.1p2 as the installation
>> target directory
>>   Using dynamic linking for Motif
>>   [: 321: unexpected operator
> That's unusual. It looks like the shell complaining about the syntax of the 
> configure script. But it works for me and others.

I have installed Ubuntu 9.10 and reproduced the problem. It is the dash shell 
being pernickety about syntax - it doesn't allow "==" as a synonym for "=" in 
the test built-in (also known as "[" for obscure reasons that shell programmers 
understand). The message can be ignored providing you do have a good Motif 
installation - the syntax error just causes configure not to stop with a proper 
error report if Motif is missing or if PPMOTIFHOME isn't set and configure 
can't work out what it should be. You can change the only instance of "==" in 
the configure script to read "=" to get things working properly. I will correct 
this in the next patch release.

I suspect that Mark just wanted to install xpp, but the rest of OpenProofPower 
build on Ubuntu 9.10 once you have installed Poly/ML. The "live" installation 
does not install g++ and Poly/ML needs that. The prerequisites for both Poly/ML 
and ProofPower are satisfied if you do:

sudo aptitude install \
  groff \
  libmotif-dev \
  libxt-dev \
  libxp-dev \
  libxmu-dev \
  texlive-latex-base texlive-generic-recommended \



Proofpower mailing list

Reply via email to