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

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?

Thanks,

Hanne Gottliebsen
---------------------------------------------------------
Hanne Gottliebsen		    Office P343
Dept. of Computer Science	    Ph: +44 1334 46 3260
University of St Andrews	    hago@dcs.st-and.ac.uk
                   - Who moved the stone?
---------------------------------------------------------