command to load PVS into lisp

tools/load-pvs.lisp

+;;; Place the following definitions into "~/.sbclrc" to be able to load PVS into
+;;; any sbcl session.
+(defmacro load-pvs (&optional pvspath)
+  "Load PVS into the current lisp environment. Argument PVSPATH is the filespec
+to the sources of PVS. If not provided, it is fetched from the environment
+variables PVSPATH."
+  (let (($pvspath (gensym)))
+    `(let ((,$pvspath
+             (cond
+               (,pvspath ,pvspath)
+               ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
+               (t (error "Cannot load PVS: PVSPATH not set.")))))
+       (uiop:with-current-directory (,$pvspath)
+         (load "pvs.system")
+         (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load)))))