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

Re: [PVS-Help] PVS batch mode



Thanks for Cesar.

However, I have a problem for this. Currently, I do not have the right
to install another version of PVS (the version of PVS I am using is
PVS 3.1).

For more clearly about the error I face now, I copy the batch file and
the specification file in the following:

>pvs -batch -load prove-all.el

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

And it displays in the terminal as follows:

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

End of file or stream: "internal input stream"
End of file or stream: "internal input stream"
(No files need saving)

Thanks for any help.


On 9/8/06, Cesar A. Munoz <munoz@nianet.org> wrote:
> Sara,
> I have implemented a PVS package for using PVS in batch mode. You can
> find it at:
>
> http://research.nianet.org/~munoz/ProofLite
>
> Hope that it helps,
>
> Cesar
> --
> Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
> National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
> 100 Exploration Way, Room 214       http://research.nianet.org/~munoz
> Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
> GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4
>
>