From 7971e57e3faf110800cd157e0b1131cb316f6ecd Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Mon, 18 Oct 2021 19:30:24 +0200
Subject: [PATCH] restructuration
---
.github/workflows/pvs_prelude.yml | 5 +++--
Makefile | 2 +-
docs/main.adoc | 12 +++++++-----
load.lisp | 11 +++++++++++
proofs/{ => src}/proof-json.lisp | 0
proofs/{ => src}/tptp.lisp | 0
pvs-load.lisp | 7 -------
{exporter => specs/src}/dk-recursive.lisp | 0
{exporter => specs/src}/dk-sig.lisp | 0
{exporter => specs/src}/dklog.lisp | 0
{exporter => specs/src}/packages.lisp | 0
{exporter => specs/src}/pp-dk3.lisp | 0
{exporter => specs/src}/pvs.lisp | 0
{exporter => specs/src}/utils.lisp | 0
{tools => specs/tools}/README.md | 0
lambdapi.mk => specs/tools/lambdapi.mk | 0
{tools => specs/tools}/lambdapi.pkg | 0
{tools => specs/tools}/prelude/Makefile | 0
{tools => specs/tools}/prelude/README.md | 0
{tools => specs/tools}/prelude/divides.lp.sh | 0
{tools => specs/tools}/prelude/mk_dummy.sh | 0
.../tools}/prelude/number_fields.lp.patch | 0
{tools => specs/tools}/prelude/theories | 0
.../tools}/prelude_patches/01-functions.diff | 0
.../tools}/prelude_patches/02-orders.diff | 0
.../tools}/prelude_patches/03-sets.diff | 0
.../tools}/prelude_patches/04-sequences.diff | 0
.../tools}/prelude_patches/05-function_image.diff | 0
.../tools}/prelude_patches/patch-prelude.sh | 0
{tools => specs/tools}/pvs2dk.sh | 0
{tools => specs/tools}/simple/Makefile | 0
tools/bootstrap.sh | 2 +-
tools/load-personoj.lisp | 14 ++++++++++++++
33 files changed, 37 insertions(+), 16 deletions(-)
create mode 100644 load.lisp
rename proofs/{ => src}/proof-json.lisp (100%)
rename proofs/{ => src}/tptp.lisp (100%)
delete mode 100644 pvs-load.lisp
rename {exporter => specs/src}/dk-recursive.lisp (100%)
rename {exporter => specs/src}/dk-sig.lisp (100%)
rename {exporter => specs/src}/dklog.lisp (100%)
rename {exporter => specs/src}/packages.lisp (100%)
rename {exporter => specs/src}/pp-dk3.lisp (100%)
rename {exporter => specs/src}/pvs.lisp (100%)
rename {exporter => specs/src}/utils.lisp (100%)
rename {tools => specs/tools}/README.md (100%)
rename lambdapi.mk => specs/tools/lambdapi.mk (100%)
rename {tools => specs/tools}/lambdapi.pkg (100%)
rename {tools => specs/tools}/prelude/Makefile (100%)
rename {tools => specs/tools}/prelude/README.md (100%)
rename {tools => specs/tools}/prelude/divides.lp.sh (100%)
rename {tools => specs/tools}/prelude/mk_dummy.sh (100%)
rename {tools => specs/tools}/prelude/number_fields.lp.patch (100%)
rename {tools => specs/tools}/prelude/theories (100%)
rename {tools => specs/tools}/prelude_patches/01-functions.diff (100%)
rename {tools => specs/tools}/prelude_patches/02-orders.diff (100%)
rename {tools => specs/tools}/prelude_patches/03-sets.diff (100%)
rename {tools => specs/tools}/prelude_patches/04-sequences.diff (100%)
rename {tools => specs/tools}/prelude_patches/05-function_image.diff (100%)
rename {tools => specs/tools}/prelude_patches/patch-prelude.sh (100%)
rename {tools => specs/tools}/pvs2dk.sh (100%)
rename {tools => specs/tools}/simple/Makefile (100%)
create mode 100644 tools/load-personoj.lisp
diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml
index 381bc9e..3cc87a0 100644
--- a/.github/workflows/pvs_prelude.yml
+++ b/.github/workflows/pvs_prelude.yml
@@ -17,13 +17,14 @@ jobs:
run: |
eval $(opam env --switch=~/lambdapi --set-switch)
bmake -C encoding install
- sed "s:PVSDKPATH:$(pwd):" pvs-load.lisp > ~/.pvs.lisp
+ cp 'tools/load-personoj.lisp' > ~/.pvs.lisp
+ echo '(load-personoj)' >> ~/.pvs.lisp
cat ~/.pvs.lisp
- name: translate and typecheck
run: |
eval $(opam env --switch=~/lambdapi --set-switch)
- cd tools/prelude || exit 1
+ cd specs/tools/prelude || exit 1
# Comment out theories that consume too much memory during
# typechecking
sed -i 's/^floor_ceil$/-floor_ceil/' theories
diff --git a/Makefile b/Makefile
index e3d841f..df01951 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
.PHONY: install
install:
${MAKE} -C encoding install
- @sed 's:PVSDKPATH:${PWD}:' pvs-load.lisp | cat
+ @sed 's:PVSDKPATH:${PWD}:' tools/load-personoj.lisp | cat
.PHONY: encoding
encoding:
diff --git a/docs/main.adoc b/docs/main.adoc
index ef136fe..eeaa488 100644
--- a/docs/main.adoc
+++ b/docs/main.adoc
@@ -128,8 +128,10 @@ To install the encoding
[source,sh]
personoj $ bmake -C encoding install
-To install the exporter, add the content of +pvs-load.lisp+ to
-+$HOME/.pvs.lisp+ replacing +PVSDKPATH+ with the path to the root of
-personoj.
-[source,sh]
-personoj $ sed "s:PVSDKPATH:$(pwd):" pvs-load.lisp >> ~/.pvs.lisp
+To install the exporter, add the content of +tools/load-personoj.lisp+ to
++$HOME/.pvs.lisp+, add the line
+[source,lisp]
+(load-personoj)
+
+at the end of +$HOME/.pvs.lisp+ and set the environment variable
++PERSONOJPATH+ to the path to the local copy of +PERSONOJ+.
diff --git a/load.lisp b/load.lisp
new file mode 100644
index 0000000..904bdfe
--- /dev/null
+++ b/load.lisp
@@ -0,0 +1,11 @@
+(dolist (m '("utils"
+ "packages"
+ "dklog"
+ "dk-sig"
+ "dk-recursive"
+ "pp-dk3"
+ "pvs"))
+ (load (concatenate 'string "specs/src/" m ".lisp") ))
+
+(dolist (m '("tptp" "proof-json"))
+ (load (concatenate 'string "proofs/src/" m ".lisp")))
diff --git a/proofs/proof-json.lisp b/proofs/src/proof-json.lisp
similarity index 100%
rename from proofs/proof-json.lisp
rename to proofs/src/proof-json.lisp
diff --git a/proofs/tptp.lisp b/proofs/src/tptp.lisp
similarity index 100%
rename from proofs/tptp.lisp
rename to proofs/src/tptp.lisp
diff --git a/pvs-load.lisp b/pvs-load.lisp
deleted file mode 100644
index bdb1982..0000000
--- a/pvs-load.lisp
+++ /dev/null
@@ -1,7 +0,0 @@
-;;;; Place this at the top of "~/.pvs.lisp"
-
-(defparameter *pvs-dedukti-path* "PVSDKPATH")
-(dolist (m '("utils" "packages" "dklog" "dk-sig" "dk-recursive" "pp-dk3" "pvs"))
- (load (concatenate 'string *pvs-dedukti-path* "/exporter/" m ".lisp")))
-(dolist (m '("tptp" "proof-json"))
- (load (concatenate 'string *pvs-dedukti-path* "/proofs/" m ".lisp")))
diff --git a/exporter/dk-recursive.lisp b/specs/src/dk-recursive.lisp
similarity index 100%
rename from exporter/dk-recursive.lisp
rename to specs/src/dk-recursive.lisp
diff --git a/exporter/dk-sig.lisp b/specs/src/dk-sig.lisp
similarity index 100%
rename from exporter/dk-sig.lisp
rename to specs/src/dk-sig.lisp
diff --git a/exporter/dklog.lisp b/specs/src/dklog.lisp
similarity index 100%
rename from exporter/dklog.lisp
rename to specs/src/dklog.lisp
diff --git a/exporter/packages.lisp b/specs/src/packages.lisp
similarity index 100%
rename from exporter/packages.lisp
rename to specs/src/packages.lisp
diff --git a/exporter/pp-dk3.lisp b/specs/src/pp-dk3.lisp
similarity index 100%
rename from exporter/pp-dk3.lisp
rename to specs/src/pp-dk3.lisp
diff --git a/exporter/pvs.lisp b/specs/src/pvs.lisp
similarity index 100%
rename from exporter/pvs.lisp
rename to specs/src/pvs.lisp
diff --git a/exporter/utils.lisp b/specs/src/utils.lisp
similarity index 100%
rename from exporter/utils.lisp
rename to specs/src/utils.lisp
diff --git a/tools/README.md b/specs/tools/README.md
similarity index 100%
rename from tools/README.md
rename to specs/tools/README.md
diff --git a/lambdapi.mk b/specs/tools/lambdapi.mk
similarity index 100%
rename from lambdapi.mk
rename to specs/tools/lambdapi.mk
diff --git a/tools/lambdapi.pkg b/specs/tools/lambdapi.pkg
similarity index 100%
rename from tools/lambdapi.pkg
rename to specs/tools/lambdapi.pkg
diff --git a/tools/prelude/Makefile b/specs/tools/prelude/Makefile
similarity index 100%
rename from tools/prelude/Makefile
rename to specs/tools/prelude/Makefile
diff --git a/tools/prelude/README.md b/specs/tools/prelude/README.md
similarity index 100%
rename from tools/prelude/README.md
rename to specs/tools/prelude/README.md
diff --git a/tools/prelude/divides.lp.sh b/specs/tools/prelude/divides.lp.sh
similarity index 100%
rename from tools/prelude/divides.lp.sh
rename to specs/tools/prelude/divides.lp.sh
diff --git a/tools/prelude/mk_dummy.sh b/specs/tools/prelude/mk_dummy.sh
similarity index 100%
rename from tools/prelude/mk_dummy.sh
rename to specs/tools/prelude/mk_dummy.sh
diff --git a/tools/prelude/number_fields.lp.patch b/specs/tools/prelude/number_fields.lp.patch
similarity index 100%
rename from tools/prelude/number_fields.lp.patch
rename to specs/tools/prelude/number_fields.lp.patch
diff --git a/tools/prelude/theories b/specs/tools/prelude/theories
similarity index 100%
rename from tools/prelude/theories
rename to specs/tools/prelude/theories
diff --git a/tools/prelude_patches/01-functions.diff b/specs/tools/prelude_patches/01-functions.diff
similarity index 100%
rename from tools/prelude_patches/01-functions.diff
rename to specs/tools/prelude_patches/01-functions.diff
diff --git a/tools/prelude_patches/02-orders.diff b/specs/tools/prelude_patches/02-orders.diff
similarity index 100%
rename from tools/prelude_patches/02-orders.diff
rename to specs/tools/prelude_patches/02-orders.diff
diff --git a/tools/prelude_patches/03-sets.diff b/specs/tools/prelude_patches/03-sets.diff
similarity index 100%
rename from tools/prelude_patches/03-sets.diff
rename to specs/tools/prelude_patches/03-sets.diff
diff --git a/tools/prelude_patches/04-sequences.diff b/specs/tools/prelude_patches/04-sequences.diff
similarity index 100%
rename from tools/prelude_patches/04-sequences.diff
rename to specs/tools/prelude_patches/04-sequences.diff
diff --git a/tools/prelude_patches/05-function_image.diff b/specs/tools/prelude_patches/05-function_image.diff
similarity index 100%
rename from tools/prelude_patches/05-function_image.diff
rename to specs/tools/prelude_patches/05-function_image.diff
diff --git a/tools/prelude_patches/patch-prelude.sh b/specs/tools/prelude_patches/patch-prelude.sh
similarity index 100%
rename from tools/prelude_patches/patch-prelude.sh
rename to specs/tools/prelude_patches/patch-prelude.sh
diff --git a/tools/pvs2dk.sh b/specs/tools/pvs2dk.sh
similarity index 100%
rename from tools/pvs2dk.sh
rename to specs/tools/pvs2dk.sh
diff --git a/tools/simple/Makefile b/specs/tools/simple/Makefile
similarity index 100%
rename from tools/simple/Makefile
rename to specs/tools/simple/Makefile
diff --git a/tools/bootstrap.sh b/tools/bootstrap.sh
index d6eaf11..f21a423 100755
--- a/tools/bootstrap.sh
+++ b/tools/bootstrap.sh
@@ -39,7 +39,7 @@ gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
PVSPATH="${HOME}/PVS"
export PVSPATH
- for p in $(find tools/prelude_patches -name '*.diff' | sort); do
+ for p in $(find specs/tools/prelude_patches -name '*.diff' | sort); do
patch "${PVSPATH}/lib/prelude.pvs" "$p"
done
diff --git a/tools/load-personoj.lisp b/tools/load-personoj.lisp
new file mode 100644
index 0000000..6e91d84
--- /dev/null
+++ b/tools/load-personoj.lisp
@@ -0,0 +1,14 @@
+;;;; Call (load-personoj) from ~/.pvs.lisp to load Personoj automatically into
+;;;; PVS
+
+(defmacro load-personoj (&optional pth)
+ "Load Personoj specification exporter and proof exporter. If given, PTH is the
+path to the root of the repository. Otherwise, the root is taken from the
+environment variable PERSONOJ"
+ (let ((pth (cond
+ (pth pth)
+ ((uiop:getenvp "PERSONOJPATH")
+ (uiop:getenv-pathname "PERSONOJPATH" :ensure-directory t))
+ (t (error "Cannot load personoj: PERSONOJPATH not set.")))))
+ `(uiop:with-current-directory (,pth)
+ (load "load.lisp"))))
--
GitLab