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

No Subject



Hi Hanne,

Currently changes to strategy files are only recognized by the
prover at the beginning of a proof, or when the user issues the
M-x load-pvs-strategies command.  If the file dates are
different, the file is reloaded.  Obviuosly more could be done
in this area.

All of the prover commands can be given an extra argument that
forces everything to be reproved.  Thus C-u C-c C-p t will
reprove all the lemmas and TCCs of the specified theory.  This
is described in the User Manual on page 23.

Regards,
Sam Owre

> I am working on some strategies, and I have found that even if a strategy
> is changed a previously finished proof is still accepted.
> 
> Example:
> 
> a is proven using strategy s
> s is changed
> if using C-c C-p t to re-prove the theory, the old proof of a is still
> assumed correct, even if s might not work on a anymore.
> 
> Is there a way to force PVS to re-prove all the lemmas in a theory, other
> than doing each of them individually?
> 
> Thanks,
> Hanne
> ---------------------------------------------------------
> Hanne Gottliebsen		    Office P337
> Dept. of Computer Science	    Ph: +44 1334 46 3265
> University of St Andrews	    hago@dcs.st-and.ac.uk
>                    - Who moved the stone?
> ---------------------------------------------------------