diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml
index 381bc9efcc7be99aff0e2e9da6ac3ac04945c312..3cc87a073f8e687c4e138682b794876309ba31d2 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 e3d841f1c6d15d485503552a68e118e1f739b87b..df019513700d4f72228e3cb4f71018dc7af2b10e 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 ef136fed398135f56bc92960ed7c23c4357629da..eeaa4884f5afe1cd78b08b3e39eb5cf16446a6c2 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 0000000000000000000000000000000000000000..904bdfeb1cb9834ef36aa3c61de27def67209154
--- /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 bdb1982f08b6c406977922c533ac24dc2b0959af..0000000000000000000000000000000000000000
--- 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 d6eaf1177d792e42b9e3afbd88f19cdff414b3e3..f21a423c27cd72dad25c08694bd8d1c8d9cfcf03 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 0000000000000000000000000000000000000000..6e91d8460d05ef159a9e1500c47ad0ac6e12102e
--- /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"))))