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

Re: [PVS-Help] PVS batch mode



Hi Sara,

The first problem I noticed is that you aren't using pvs-validate
correctly.  It should surround the other commands, e.g.,

(pvs-validate "batch.log" "~/Batch"
  (pvs-message "Proving batch")
  (typecheck "batch")
  (let ((current-prefix-arg t))
   (prove-untried-theory "batch" "(grind)"))
  (status-proof-theory "test")
  (pvs-message "Completed"))

Note carefully the parentheses.  This should explain Question 1,

As for Question 2: PVS tries hard to maintain proofs, so that even if a
theory changes the proofs are maintained, and lemmas with the same names
will have the existing proofs attached, even if their definition changes.

There is bug in the error message, which I will fix.  What it should say
is that "every formula already has a proof, so no proofs were attempted".
This is the intended meaning of prove-untried-theory.  If you really
want to reprove regardless, you should use prove-formulas-theory instead.

Regards,
Sam

Sara Kenedy <sarakenedy@gmail.com> wrote:

> Date: Sun, 10 Sep 2006 16:52:28 -0400
> From: "Sara Kenedy" <sarakenedy@gmail.com>
> To: "Sam Owre" <owre@csl.sri.com>
> Subject: Re: [PVS-Help] PVS batch mode
> Cc: "Cesar A. Munoz" <munoz@nianet.org>, pvs-help@csl.sri.com
> 
> Hello all,
> I try to work on batch.el and batch.pvs as follows:
> 
> ------batch.el----
> (pvs-validate "batch.log" "~/Batch")
> (pvs-message "Proving batch")
> (typecheck "batch")
> (let ((current-prefix-arg t))
>  (prove-untried-theory "batch" "(grind)"))
> (status-proof-theory "test")
> (pvs-message "Completed")
> 
> -------batch.pvs---
> batch: THEORY
> BEGIN
> x: VAR real
> batch: LEMMA x > 1 IMPLIES x > 0
> END batch
> 
> Then I run:
> >pvs -batch -load batch.el -v 3
> 
> The results make me confused, so, I have some questions below:
> Question 1) As I expected, PVS needs to display the result in
> "batch.log"  as I declared in "batch.el" ? But in "batch.log", it
> displays only the content:
> "PVS Version 3.1
> Context changed to ~/Batch/"
> 
> And all the resulting, it displays to the terminal, for e.g, it
> dispalys the following to the terminal:
> batch :
>   |-------
> {1}   FORALL (x: real): x > 1 IMPLIES x > 0
> 
> Rerunning step: (grind)
> Trying repeated skolemization, instantiation, and if-lifting,
> Q.E.D.
> 
> Question 2) When the batch process finishes, it automatically
> generates the file "batch.prf". However, when I attempt to change the
> content of "batch.pvs" file and then run batch again, the content of
> "batch.prf" does not change and there is a warning in the terminal
> "Every attempted formula of theory batch has an existing proof and
> failed to prove with the given strategy.No formulas attempted"
> 
> Is there any way if I change the content of specification file
> 'batch.pvs" and run batch, the file ".prf" and ".log" is automatically
> updated?
> 
> Thanks for any help.
> 
> S.
> 
> 
> 
> On 9/8/06, Sam Owre <owre@csl.sri.com> wrote:
> > Hi Sara,
> >
> > For that you need to do two things; first, add a command to
> > prove-all.el to display the information you want, for
> > example
> >
> > (status-proof-theory "test")
> >
> > Then you need to invoke PVS with the verbosity argument set
> > above 0 - I usually set it to 3.  Just add '-v 3' to your
> > invocation of pvs - anywhere after the '-batch' flag.
> >
> > Regards,
> > Sam
> >
> >
> > Sara Kenedy <sarakenedy@gmail.com> wrote:
> >
> > > Thanks a lot for Sam to recognize the error for me. However, I do not
> > > know why it des not display the result after using the strategy
> > > "GRIND". (Sorry if the question seems so "baby")
> > >
> > > I fix the error, and try it again.
> > >
> > > ----------------prove-all.el------------------
> > > (pvs-message "Proving all unproven theorems in batch.pvs")
> > > (typecheck "batch")
> > > (let ((current-prefix-arg t))
> > >  (prove-untried-pvs-file "batch" "(grind)"))
> > > (pvs-message "Completed")
> > > -----------------batch.pvs----------------------------
> > > batch: THEORY
> > > BEGIN
> > >
> > >   a : theorem  1 < 2
> > >   b : theorem  2 < 3
> > >   c : theorem  3 < 4
> > >   d : theorem  4 < 5
> > >
> > > END batch
> > >
> > > > pvs -batch -load prove-all.el
> > > Loading /usr/lib/xemacs/xemacs-packages/lisp/site-start.d/psgml-init.el...
> > > Loading pvs-load...
> > > Loading pvs-prelude-files-and-regions...
> > > Proving all unproven theorems in batch.pvs
> > > Proving all unproven theorems in batch.pvs
> > > Completed
> > > Completed
> > >
> > > Proving all unproven theorems in batch.pvs
> > > Completed
> > >
> > > (No files need saving)
> > > Buffer *scratch* has no process
> > >
> > >
> > >
> > > On 9/8/06, Sam Owre <owre@csl.sri.com> wrote:
> > > > Hi Sara,
> > > >
> > > > I see the problem - the
> > > >
> > > > (pvs-message "Completed)
> > > >
> > > > is missing the closing string quote - it should be:
> > > >
> > > > (pvs-message "Completed")
> > > >
> > > > Sam
> > > >
> >