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. There is no error being thrown, it just returns val it = ():
TYPE, and then locks up. Have to either kill all the window proc id's or
restart the system to get rid of them. Mostly it is restarting b/c kill
sometimes will not remove them for some reason. I was working on the
Peanissimo theory write up. Written it several times and get the lock up
every time, any suggestions on trouble shooting?


On Mon, Aug 13, 2012 at 3:44 PM, Rob Arthan <> wrote:

> On 13 Aug 2012, at 13:31, Jon Lockhart wrote:
> > Rob,
> >
> > Ok so looks like I am looking to rewrite all my specifications again in
> ProofPower. A minor inconvenience but should not be a problem.
> That is likely the quickest way to get started.
> > I will just pop up my specs on one screen and bring up ProofPower's XPP
> up on the other screen in my Linux VM, and I should be able to rewrite them
> with no problems. The only thing I can't seem to find is the symbol library
> in XPP. I have found where I can insert the various Zed structures, no
> problem, but there is supposed to be an XPP keyboard that has these
> symbols, based on the pictures in the documentation. Is this available in
> the editor version of XPP or do I need to run the full version of XPP to
> have access to that?
> >
> The keyboard in the picture is the actual keyboard, although you may need
> to do a bit more work to set it up. There is a tool called the Palette in
> the Tools menu that lets you enter all the symbols with mouse clicks
> without having to do any more set-up and without having to learn the key
> combinations.
> If you do want to set up the keyboard have a read of section 4.3 of the
> Xpp manual and the comments at the head of the file
> app-defaults/XppKeyboard in the first instance.
> > Once I get these in the system though, I definitely need to get some
> proofs written for them. That is where I am having a fair bit of trouble
> with the examples and documentation at the moment. I have a solid grasp of
> Z, and from Rogers email and the documentation, I can just write the proofs
> mostly in Z, which would save me some time in having to learn HOL right
> now, though I think I will learn it anyways for the future, just at a
> slower pace. In any case, the proof writing is not the issue, it is the
> writing in the ProofPower environment I guess I am hung up on, along with a
> few other minor things.
> >
> > I will look over all the documentation again on the site Rob, and
> continuing to see if I can get the examples operational so I can apply what
> is shown there to my open specifications.
> Good luck! And do keep asking if you have any more problems.
> Regards,
> Rob.
Proofpower mailing list

Reply via email to