diff --git a/.github/workflows/proof_tools.yml b/.github/workflows/proof_tools.yml
new file mode 100644
index 0000000000000000000000000000000000000000..66b1f2c76161df073df5cae6bbfaea2d73809423
--- /dev/null
+++ b/.github/workflows/proof_tools.yml
@@ -0,0 +1,30 @@
+name: proof_tools
+
+on: [push]
+
+jobs:
+ build:
+ runs-on: ubuntu-latest
+
+ steps:
+ - uses: actions/checkout@v2
+ with:
+ path: personoj
+
+ - name: setup
+ run: ${GITHUB_WORKSPACE}/personoj/tools/bootstrap.sh
+ shell: sh
+
+ - name: compile and run tests
+ run: |
+ cd "${GITHUB_WORKSPACE}"/personoj/proofs/ || exit 1
+ (cd dopth || exit 1
+ opam switch create . --packages dune --yes
+ eval $(opam env)
+ dune build) # TODO implement tests
+ (cd chainprops || exit 1
+ opam switch create . --deps-only --yes
+ eval $(opam env)
+ opam pin add ~/lambdapi --yes
+ eval $(opam env)
+ bmake tests)
diff --git a/proofs/man/.gitignore b/proofs/.gitignore
similarity index 100%
rename from proofs/man/.gitignore
rename to proofs/.gitignore
diff --git a/proofs/asciidoc.mk b/proofs/asciidoc.mk
deleted file mode 100644
index 117f9e5af94851d8fbac4d3582af1654ceec64a9..0000000000000000000000000000000000000000
--- a/proofs/asciidoc.mk
+++ /dev/null
@@ -1,6 +0,0 @@
-A2X ?= a2x
-
-.SUFFIXES: .1 .asciidoc
-
-.asciidoc.1:
- ${A2X} -f manpage -d manpage $<
diff --git a/proofs/chainprops/Makefile b/proofs/chainprops/Makefile
index dc2e1f754990d7e82d7a3fe3762e036f3021ca66..ff5959654bd062200620d481b313f2dab3c9a17b 100644
--- a/proofs/chainprops/Makefile
+++ b/proofs/chainprops/Makefile
@@ -1,24 +1,18 @@
-PREFIX ?= /usr/local/
-DUNE ?= dune
+EXE = psnj-chainprops
+MAN1 = psnj-chainprops.1
-all: psnj-chainprops psnj-chainprops.1
+DUNE ?= dune
_build/default/chainprops.exe: chainprops.ml
@${DUNE} build
psnj-chainprops: _build/default/chainprops.exe
- @ln -sf _build/default/chainprops.exe $@
-
-tests:
- @${DUNE} runtest
+ @cp -f _build/default/chainprops.exe $@
psnj-chainprops.1: psnj-chainprops
@./psnj-chainprops --help=groff > $@
-man: psnj-chainprops.1
-
-install: all
- cp -f psnj-chainprops ${PREFIX}/bin/
- cp -f psnj-chainprops.1 ${PREFIX}/man/man1/
+tests:
+ @${DUNE} runtest
-.PHONY: install all man
+.include "../tools.mk"
diff --git a/proofs/dopth/Makefile b/proofs/dopth/Makefile
index 4cbb2807aed0a35c18b25696010f0487b4464c36..c3226ed70346397aadce64b1d0d7d007270e550c 100644
--- a/proofs/dopth/Makefile
+++ b/proofs/dopth/Makefile
@@ -1,19 +1,12 @@
DUNE ?= dune
-PREFIX ?= /usr/local
-all: psnj-dopth psnj-dopth.1
-.include "../asciidoc.mk"
+EXE = psnj-dopth
+MAN1 = psnj-dopth.1
_build/default/dopth.exe: dopth.ml
${DUNE} build
psnj-dopth: _build/default/dopth.exe
- @ln -f _build/default/dopth.exe $@
+ @cp -f _build/default/dopth.exe $@
-man: psnj-dopth.1
-
-install: all
- @cp -f psnj-dopth ${PREFIX}/bin/
- @cp -f psnj-dopth.1 ${PREFIX}/man/man1/
-
-.PHONY: man install all
+.include "../tools.mk"
diff --git a/proofs/man/Makefile b/proofs/man/Makefile
deleted file mode 100644
index 11d645d5dd8527b4c1bc1b23bf140b74a7d168d8..0000000000000000000000000000000000000000
--- a/proofs/man/Makefile
+++ /dev/null
@@ -1,3 +0,0 @@
-all: psnj-split.1
-
-.include "../asciidoc.mk"
diff --git a/proofs/split/Makefile b/proofs/split/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..d556daf606412b9250c3a8f997a3a55b93320f44
--- /dev/null
+++ b/proofs/split/Makefile
@@ -0,0 +1,4 @@
+EXE = psnj-split
+MAN1 = psnj-split.1
+
+.include "../tools.mk"
diff --git a/proofs/bin/psnj-split b/proofs/split/psnj-split
similarity index 100%
rename from proofs/bin/psnj-split
rename to proofs/split/psnj-split
diff --git a/proofs/man/psnj-split.asciidoc b/proofs/split/psnj-split.asciidoc
similarity index 100%
rename from proofs/man/psnj-split.asciidoc
rename to proofs/split/psnj-split.asciidoc
diff --git a/proofs/tools.mk b/proofs/tools.mk
new file mode 100644
index 0000000000000000000000000000000000000000..35db2b0e0b4aa814e347203f8e318a128be33c12
--- /dev/null
+++ b/proofs/tools.mk
@@ -0,0 +1,36 @@
+PREFIX ?= /usr/local
+A2X ?= a2x
+EXE ?=
+MAN1 ?=
+MAN5 ?=
+
+.SUFFIXES: .1 .5 .asciidoc
+
+.asciidoc.1:
+ ${A2X} -f manpage -d manpage $<
+
+.asciidoc.5:
+ ${A2X} -f manpage -d manpage $<
+
+install: ${EXE} ${MAN}
+ cp -f ${EXE} ${PREFIX}/bin/
+ cp -f ${MAN1} ${PREFIX}/man/man1/
+ cp -f ${MAN5} ${PREFIX}/man/man5
+
+uninstall:
+.for e in ${EXE}
+ rm -f ${PREFIX}/bin/$e
+.endfor
+.for m in ${MAN1}
+ rm -f ${PREFIX}/man/man1/$m
+.endfor
+.for m in ${MAN5}
+ rm -f ${PREFIX}/man/man5/$m
+.endfor
+
+man: ${MAN1} ${MAN5}
+
+all: ${EXE} ${MAN1} ${MAN5}
+
+.MAIN: all
+.PHONY: man all install uninstall
diff --git a/tools/bootstrap.sh b/tools/bootstrap.sh
index cd208d300af415cad38b5c626e2ba38f34ef7a2d..52bd155ec10a876ba1ee96a6db30c32daa98445d 100755
--- a/tools/bootstrap.sh
+++ b/tools/bootstrap.sh
@@ -5,6 +5,8 @@ SCRIPT=$(realpath "$0")
DIR=$(dirname "$SCRIPT")
ROOT=$(realpath "${DIR}/..") # Root of personoj repo
+## Opam
+
yes | sudo apt-get -q install \
zlib1g-dev libx11-dev libgmp-dev bubblewrap m4 gcc autoconf \
make unzip pkg-config git rsync bmake gcc perl \
@@ -12,13 +14,15 @@ yes | sudo apt-get -q install \
sudo sysctl kernel.unprivileged_userns_clone=1
yes '/usr/local/bin' | sudo bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0"
+opam init --bare --no-setup -q
+
+## SBCL
+
url="https://downloads.sourceforge.net/project/sbcl/sbcl/1.4.16/sbcl-1.4.16-x86-64-linux-binary.tar.bz2"
(cd "${HOME}" || exit 1
curl "$url" -L | tar jx
ln -s sbcl* sbcl)
-opam init --bare --no-setup -q
-
gclone () {
(cd "$HOME"
git clone "$1"
@@ -26,8 +30,9 @@ gclone () {
git checkout "$3"))
}
-gclone https://github.com/gabrielhdt/lambdapi.git lambdapi aae26f2d
-gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
+# Lambdapi
+
+gclone https://github.com/gabrielhdt/lambdapi.git lambdapi 1a7031e4
(cd "${HOME}/lambdapi" || exit 1
opam switch create . --locked --deps-only --yes
@@ -35,6 +40,10 @@ gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
make install
why3 config detect)
+# PVS
+
+gclone https://github.com/SRI-CSL/PVS.git PVS pvs7.1
+
(cd "${HOME}/PVS" || exit 1
autoconf
./configure)