[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