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. 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?

Are you saying that the xpp user interface locks up? If so that definitely 
shouldn't be happening. The ProofPower-ML session running in the xpp journal 
window should finish, but the xpp menus and so on should work as normal. Is 
that not what is happening?

Aside: the source of this tutorial is in usr004.doc in the doc directory, so 
you don't need to type it in yourself.



Proofpower mailing list

Reply via email to