diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml index 2ec033a0c940f6f5ae8fa30bb992a35c0f0b705e..e574d3be7fa332fb292f6856df7d795faa76a15e 100644 --- a/.github/workflows/pvs_prelude.yml +++ b/.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: | diff --git a/pvs-load.lisp b/pvs-load.lisp index 969ea6c465c516a9473bdef98f3516e415f1de01..467561d1dace499c011a14abd142e3c02b49eb52 100644 --- a/pvs-load.lisp +++ b/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")))