[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Use of Common Lisp functions in ".el" file in batch mode
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.