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. 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?
Thanks, Jon On Mon, Aug 13, 2012 at 3:44 PM, Rob Arthan <r...@lemma-one.com> 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
