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

Checkpointing PVS theories

Whenever I have reached a significant development point in theory x,
and have all theorems proven, I have been copying the x.pvs and x.prf
files to y.pvs and y.prf, and editing the theory names in both files
from x to y.  I then continue developing with y.  However, in my
latest attempt, PVS refuses to find any proofs for theory y.
Starting a new PVS image after deleting all .bin files hasn't worked.

Is this approach approved?  Have I been just lucky in the past?  Is
there some special trick to perform this operation?

Paul Loewenstein          Sun Microsystems Inc., Mailstop UMPK12-302
Staff Engineer            901 San Antonio Road, Palo Alto, California 94303
		          Tel: 650-786-6015  FAX: 650-568-9603