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

Re: [PVS-Help] PVS batch mode

I have implemented a PVS package for using PVS in batch mode. You can
find it at:


Hope that it helps,

On Thu, 2006-09-07 at 21:22, Sara Kenedy wrote:
> Hello all,
> Now I need to weok with PVS batch mode. I read about PVS batch mode in
> the document "PVS Prover Guide" and also follow the example given in
> http://pvs.csl.sri.com/mail-archive/pvs-help/msg00486.html.
> However, when I try the same example in the link (prove-all.el for
> batch file and test.pvs for PVS specification file), it displays in
> the terminal as follows:
> [sara@hamill ~]$ pvs -batch -l prove-all.el
> Loading /usr/share/xemacs/site-packages/lisp/site-start.d/maxima.el...
> Loading leim-list...
> Loading pvs-load...
> Loading pvs-prelude-files-and-regions...
> Proving all unproven theorems in test.pvs
> Proving all unproven theorems in test.pvs
> End of file or stream: "internal input stream"
> End of file or stream: "internal input stream"
> (No files need saving)
> I do not know why it displays like this. If anyone knows the reasons,
> please let me know. I really appreciate for that. Thanks a lot.
> Sara,
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