[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: 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?
You could try
to load the edited .prf into PVS. But starting a new PVS image does
that, I so I am not really sure what the problem is.
P.S. Another good way to do this kinda thing is to use M-x dump-pvs-files,
edit, then M-x undump-pvs-file