Re: [PVS-Help] opening files and batch mode

[Sam Owre <owre@csl.sri.com>]

Hi Erika,

The '-l' argument loads an Emacs lisp file, not a Common Lisp file.
Though there are many similarities, the lisps are not really the same.
However, you can send a form to pvs lisp using pvs-send-and-wait:

(pvs-send-and-wait
  "(with-open-file (str \"pvs-strategies-base\" :direction :input)
      (do ((line (read-line str nil 'eof)
                 (read-line str nil 'eof)))
       ((eql line 'eof))
       (format t \"~A~%\" line)))")

Note that embedded strings must be escaped.

The other possibility is to use ~/.pvs.lisp, which is loaded into pvs
lisp at startup.

Hope this helps,
Sam

Erika Rice <erice@cs.washington.edu> wrote:

> Date: Mon, 23 May 2005 20:37:08 -0700
> From: Erika Rice <erice@cs.washington.edu>
> To: pvs-help@csl.sri.com
> Subject: [PVS-Help] opening files and batch mode
> Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com
> 
> I want to use the batch mode of pvs and I want to open a file.  I run 
>     pvs -batch -l file.el
> where file.el contains
>     (with-open-file (str "pvs-strategies-base" :direction :input)
>       (do ((line (read-line str nil 'eof)
>                  (read-line str nil 'eof)))
>        ((eql line 'eof))
>        (format t "~A~%" line)))
> 
> However, when I run this, I get an error saying with-open-file has a
> void function definition.  
> 
> Why is this? Alternately, how can I read in a file for use in pvs
> batch mode?
> 
> Thanks,
> 
>     Erika Rice