From aeb03dc2b58c529472ebcbf665ddb831cafe83a2 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Mon, 18 Oct 2021 18:13:22 +0200
Subject: [PATCH] command to load PVS into lisp

---
 tools/load-pvs.lisp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 tools/load-pvs.lisp

diff --git a/tools/load-pvs.lisp b/tools/load-pvs.lisp
new file mode 100644
index 0000000..f8dfe47
--- /dev/null
+++ b/tools/load-pvs.lisp
@@ -0,0 +1,15 @@
+;;; 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)))))
-- 
GitLab