Thanks for the fix that really did the trick. I believe the database is
saving and I have full access to the XPP tool bar and editing, including
restarting the execution window.

I did have a question on some of the outputs from the tutorial document.
Currently I am on user013C and when I have placed some of the commands into
the terminal, via the execute line command, the ProofPower output is not
the same as is reported in the document. Is this due to some changes that
have been made since this document was published in 2002? Also a few of the
rewrite commands that were in the document threw exceptions.


On Wed, Aug 22, 2012 at 5:22 PM, Rob Arthan <> wrote:

> On 18 Aug 2012, at 22:14, Jon Lockhart wrote:
> > Rob,
> >
> > I got a trouble shooting question for you. Been going through the
> learning documentation this weekend, currently still on the first tutorial
> wanting to make sure I soak it all in before moving to HOL and Z, but I
> seem to be running into a problem with one of the commands. Every time I
> try to use the save_and_quit() ML command in the execution Window the whole
> system freezes up.
> Thanks to Jon for pointing this out and proviing further details. I now
> have a fix for this problem, whereby what caused a busy wait on some
> operating systems will actually stop xpp responding to the user on a recent
> Debian release. I have attached a patch which should work on any version
> downloaded in the last 18 months or so.
> To use the patch, copy it into /tmp say, then go to your ProofPower build
> directory (where config and install live) and do:
>         gunzip -c /tmp/patch-2.9.1w2.rda.120821.gz | patch -p1 -b -B orig/
> then do:
>         PPTARGETS=xpp ./configure
>         ./install -d
> Regards,
> Rob.
Proofpower mailing list

Reply via email to