diff --git a/.github/workflows/pvs_prelude.yml b/.github/workflows/pvs_prelude.yml index 3cc87a073f8e687c4e138682b794876309ba31d2..bab941ebe75ea07b20dec55613f0a0338ed4eda5 100644 --- a/.github/workflows/pvs_prelude.yml +++ b/.github/workflows/pvs_prelude.yml @@ -8,26 +8,28 @@ jobs: steps: - uses: actions/checkout@v2 + with: + path: personoj - name: setup - run: tools/bootstrap.sh + run: ${GITHUB_WORKSPACE}/personoj/tools/bootstrap.sh shell: sh - name: install personoj run: | eval $(opam env --switch=~/lambdapi --set-switch) - bmake -C encoding install - cp 'tools/load-personoj.lisp' > ~/.pvs.lisp + bmake -C "${GITHUB_WORKSPACE}"/personoj/encoding install + cp "${GITHUB_WORKSPACE}/personoj/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 specs/tools/prelude || exit 1 + cd "${GITHUB_WORKSPACE}"/personoj/specs/tools/prelude || exit 1 # Comment out theories that consume too much memory during # typechecking sed -i 's/^floor_ceil$/-floor_ceil/' theories sed -i 's/^modulo_arithmetic$/-modulo_arithmetic/' theories sed -i 's/^mod$/-mod/' theories - bmake PVSPATH=~/PVS # Set in bootstrap.sh + PERSONOJPATH="${GITHUB_WORKSPACE}"/personoj/ + bmake PERSONOJPATH="${PERSONOJPATH}" PVSPATH=~/PVS diff --git a/tools/bootstrap.sh b/tools/bootstrap.sh index f21a423c27cd72dad25c08694bd8d1c8d9cfcf03..0e48e6803dc710a88961a5e1828029d0477475ab 100755 --- a/tools/bootstrap.sh +++ b/tools/bootstrap.sh @@ -1,6 +1,10 @@ #!/bin/sh set -eu +SCRIPT=$(realpath "$0") +DIR=$(dirname "$SCRIPT") +ROOT=$(realpath "${DIR}/..") # Root of personoj repo + curl -s 'http://www.lsv.fr/~hondet/pvs/lambdapi-pvs_1.0_all.deb' > lambdapi-pvs.deb yes | sudo apt-get -q install ./lambdapi-pvs.deb yes | sudo apt-get install -q emacs # For PVS @@ -39,7 +43,7 @@ gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1 PVSPATH="${HOME}/PVS" export PVSPATH - for p in $(find specs/tools/prelude_patches -name '*.diff' | sort); do + for p in $(find "${ROOT}"/specs/tools/prelude_patches -name '*.diff' | sort); do patch "${PVSPATH}/lib/prelude.pvs" "$p" done