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

Re: [PVS-Help] PVS batch mode



You are completely right. Thanks a lot.

S.

On 9/10/06, Sam Owre <owre@csl.sri.com> wrote:
> 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"))

> > > > > Sam