ci for tools

.github/workflows/proof_tools.yml

+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)

proofs/asciidoc.mk

-A2X ?= a2x
-
-.SUFFIXES: .1 .asciidoc
-
-.asciidoc.1:
-	${A2X} -f manpage -d manpage $<

proofs/chainprops/Makefile

-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"

proofs/dopth/Makefile

 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"

proofs/man/Makefile

-all: psnj-split.1
-	
-.include "../asciidoc.mk"

proofs/split/Makefile

+EXE  = psnj-split
+MAN1 = psnj-split.1
+
+.include "../tools.mk"

proofs/tools.mk

+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

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)