[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

      M-x install-pvs-proof-file

  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.

  Rick Butler

  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