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

Re: [PVS-Help] PVS batch mode



Hi Sara,

The usual cause of this is an unfinished parentheses or string in the
Emacs input.  I was able to recreate the error by leaving off the last
closing parentheses in the prove-all.el file - I would look carefully at
that.  If you're still having problems, try loading the expressions in
one at a time interactively, or send me your prove-all.el file and I'll
take a look.

Regards,
Sam Owre

Sara Kenedy <sarakenedy@gmail.com> 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,