Skip to content
Snippets Groups Projects
Commit cdb25bc2 authored by Gabriel's avatar Gabriel Committed by hondet
Browse files

fixed recipe

parent 4a6dcc8a
No related branches found
No related tags found
No related merge requests found
......@@ -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
#!/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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment