restructuration

.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

Makefile

 .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:

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+.

load.lisp

+(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")))

pvs-load.lisp

-;;;; 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")))