[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] opening files and batch mode
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:
"(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,
Erika Rice <firstname.lastname@example.org> wrote:
> Date: Mon, 23 May 2005 20:37:08 -0700
> From: Erika Rice <email@example.com>
> To: firstname.lastname@example.org
> Subject: [PVS-Help] opening files and batch mode
> Sender: email@example.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?
> Erika Rice