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

Re: [PVS-Help] Use of Common Lisp functions in ".el" file in batch mode



Hi Min,

The way to invoke PVS Lisp functions from Emacs is with with
pvs-send-and-wait, which invokes the Lisp function and returns the result,
or pvs-send, which does not wait for the result.  Thus

(pvs-send-and-wait "(format nil \"~a\" *pvs-context*)") will return the
value of *pvs-context* - not that string quotes must be escaped.

The pvs-validate macro just makes it easy to set up for batch processing,
but does not directly provide a means to invoke PVS lisp functions.

Regards,
Sam

Kyongho Min <min@xxxxxxxxxxxxxxx> wrote:

> Dear helpers,
> 
> Is there any way to use ACL common lisp functions in ".el" file in
> batch mode? If I use some ACL functions inside (pvs-validate ... ) macro
> block, then it returns undefined function error.
> 
> In my understanding, the el macro (pvs-validate ... ) in "pvs-utils.el"
> invokes PVS with ACL lisp (pvs-init) to prove a theory.
> 
> I wonder if it is possible to use ACL functions (e.g. parse-file,
> collect-tccs, found in "pvs.lisp") in "el" file in batch mode.
> 
> In addition, elisp functions solved my expectation with a little work.
> 
> Thanks a lot for your help.
> 
> regards,
> 
> min