[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: How to recover from a runaway proof attempt?

> I have encountered problems when trying to recover after a proof attempt
> gone wrong (various reasons, eg rewriting depth going wild :-)
> I have tried stop (C-c C-z) followed by quit, but this does not seem to
> work as I thought, as I cannot start a new proof. If trying to start a new
> proof, I get the message "Must exit prover first". 
> So far my only way to solve the problem has been to exit pvs, killing the
> (otherwise unaccessible?) process in doing so. 
> Is there not some better way to solve this problem?

    Type (quit) at the Rule? prompt and then exit normally ie, C-xC-c

-------------------------------	V Arun Kumar, -------------------------------
------------------------------- Fourth Yr. B.tech., -------------------------
------------------------------- Dept. of Computer Science & Engineering -----
------------------------------- Indian Institute of Technology Bombay -------
------------------------------- email : arun@cse.iitb.ernet.in --------------
------------------------------- URL   : http://www.cse.iitb.ernet.in/~arun --