loading pvs

.github/workflows/pvs_prelude.yml

@@ -18,6 +18,7 @@ jobs:
         eval $(opam env --switch=~/lambdapi --set-switch)
         bmake -C encoding install
         sed "s:PVSDKPATH:$(pwd):" pvs-load.lisp > ~/.pvs.lisp
+        cat ~/.pvs.lisp
 
     - name: translate and typecheck
       run: |

pvs-load.lisp

@@ -2,4 +2,4 @@
 
 (defparameter *pvs-dedukti-path* "PVSDKPATH")
 (dolist (m '("utils" "packages" "dklog" "dk-sig" "dk-recursive" "pp-dk3" "pvs"))
-  (load (concatenate 'string *pvs-dedukti-path* m ".lisp")))
+  (load (concatenate 'string *pvs-dedukti-path* "/exporter/" m ".lisp")))