[PVS-Help] PVS batch mode

["Sara Kenedy" <sarakenedy@xxxxxxxxx>]

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,