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

Re: problem with pvs

Hi Victoria,

This can happen if the .prf file somehow gets corrupted, which I have seen
happen upon occasion.   You can sometime recover by editing the proof file
and looking for things like unbalanced parentheses or strange line breaks
and fixing them.  I'd be happy to look at your .prf file is you want to
send it (gzipped and uuencoded).  If you think the file is being generated
improperly by PVS, please send your specification as well.

Sam Owre

> From:    Victoria Chernyakhovsky <vchernya@ececs.uc.edu>
> Subject: problem with pvs
> Date:    Sat, 18 Apr 1998 12:05:10 EDT
> To:      pvs-help@csl.sri.com
> X-Mailing-List: <pvs-help@csl.sri.com> archive/latest/145
> X-Loop:  pvs-help@csl.sri.com
> Hi,	
> 	I am using  pvs  and whenever I exit the pvs prover in the middle of a
> proof by typing "quit" at the pvs prover command prompt, it gives a
> message 
> 		"Error reading proof file" and prints the proof file name
> "prooffilename.prfNIL" and exits. This overwrites the proof file with
> only the existing partial proof and all other proofs in the same file is
> lost.
> Please help.
> Thanks
> Victoria