Roger, On Friday 21 Nov 2008 10:03 am, Roger Bishop Jones wrote: > On Friday 21 November 2008 06:00:18 Rob Arthan wrote: > > It seems to work for me. How is it failing? > > A rewrite failed. > > However, I went through it all again more carefully and it has now gone > through OK. Not sure which of the things I changed made the difference. > The first attempt was done in the ProofPower build src directory. This time > I did it in a separate directory so I could pack it up and send it to you. > This failed more radically because I had PPHOME set to the previous > installation directory. > When I set PPHOME correctly the build went through OK .Presumably it would > then also have worked in original build directory. > So if you pick up the right ProofPower because you happen to be in the > right place, but PPHOME is not right, proof scripts may then fail > mysteriously?
I would be very surprised if having PPHOME would cause a subtle error like that. It only influences xpp (not relevant here) and the shell scripts that get things started, once you've got an ML session going, it's going and that's that. This is particularly so with Poly/ML 5.2.1 because the equivalent of the old poly driver program is now a binary in the ProofPower bin directory called pp-ml program and it won't run if it doesn't match the database. By the way, you should only need to use PPHOME for special effects. If you don't set any of the PPXYZ shell variables, everything should work out what PPHOME should be automatically. Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
