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

Re: [PVS-Help] PVS batch mode



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
> >