dune makefile, pipeline directory

proofs/Makefile

-PREFIX ?= /usr/local
-
-_EXE = psnj-split
-
-install: ${_EXE:S!^!bin/!} man
-.for e in ${_EXE}
-	cp bin/$e ${PREFIX}/bin/$e
-	cp man/${e}.1 ${PREFIX}/man/man1/${e}.1
-.endfor
-	(cd dopth && eval $(opam env) && ${MAKE} install)
-	(cd chainprops && eval $(opam env) && ${MAKE} install)
-
-uninstall:
-.for e in ${_EXE}
-	rm -f ${PREFIX}/bin/$e
-	rm -f ${PREFIX}/man/man1/${e}.1
-.endfor
-	@(cd dopth && ${MAKE} uninstall)
-	@(cd chainprops && ${MAKE} uninstall)
-
-man:
-	@(cd man && ${MAKE})
-	@(cd dopth && ${MAKE} man)
-	@(cd chainprops && ${MAKE} man)
-
-.PHONY: man install uninstall

proofs/appaxiom/Makefile

-EXE = psnj-appaxiom
-MAN1 = psnj-appaxiom.1
-
-DUNE ?= dune
-
-_build/default/appaxiom.exe: appaxiom.ml
-	@${DUNE} build
-
-psnj-appaxiom: _build/default/appaxiom.exe
-	@cp -f _build/default/appaxiom.exe $@
-
-psnj-appaxiom.1: psnj-appaxiom
-	@./psnj-appaxiom --help=groff > $@
-
-tests:
-	@${DUNE} runtest
+ROOT     = appaxiom
+CMDLINER = true
 
+.include "../dune-exe.mk"
 .include "../tools.mk"

proofs/chainprops/Makefile

-EXE = psnj-chainprops
-MAN1 = psnj-chainprops.1
-
-DUNE ?= dune
-
-_build/default/chainprops.exe: chainprops.ml
-	@${DUNE} build
-
-psnj-chainprops: _build/default/chainprops.exe
-	@cp -f _build/default/chainprops.exe $@
-
-psnj-chainprops.1: psnj-chainprops
-	@./psnj-chainprops --help=groff > $@
-
-tests:
-	@${DUNE} runtest
+ROOT     = chainprops
+CMDLINER = true
 
+.include "../dune-exe.mk"
 .include "../tools.mk"

proofs/dopth/Makefile

-DUNE ?= dune
-
-EXE  = psnj-dopth
-MAN1 = psnj-dopth.1
-
-_build/default/dopth.exe: dopth.ml
-	${DUNE} build
-
-psnj-dopth: _build/default/dopth.exe
-	@cp -f _build/default/dopth.exe $@
-
-.PHONY: tests
-tests: _build/default/dopth.exe
-	@${DUNE} runtest
+ROOT = dopth
 
+.include "../dune-exe.mk"
 .include "../tools.mk"

proofs/dune-exe.mk

+# Dune targets for executables
+# Include *before* tools.mk
+
+DUNE     ?= dune
+OPAM     ?= opam
+ROOT     ?= # Name of the source file (without extension)
+CMDLINER ?= # Set to something if cmdliner is used to generate documentation
+EXE   = psnj-${ROOT}
+MAN1  = psnj-${ROOT}.1
+
+_build/default/${ROOT}.exe: ${ROOT}.ml
+	@${OPAM} exec -- ${DUNE} build
+
+psnj-${ROOT}: _build/default/${ROOT}.exe
+	@cp -f _build/default/${ROOT}.exe $@
+
+tests: _build/default/${ROOT}.exe
+	@${OPAM} exec -- ${DUNE} runtest
+
+.if ${CMDLINER}
+${EXE}.1: ${EXE}
+	@./${EXE} --help=groff > $@
+.endif
+
+clean:
+	@${OPAM} exec -- ${DUNE} clean
+	@rm -f ${EXE}
+	@rm -f ${MAN1}
+
+.PHONY: tests clean

proofs/examples/.gitignore → proofs/pipeline/examples/.gitignore

@@ -3,3 +3,7 @@
 *.summary
 pvsbin/
 .pvscontext
+*.json
+*.lp
+orphaned-proof.prf
+*.dep

proofs/pipeline/examples/lambdapi.pkg

+package_name = lpvs
+root_path = lpvs

proofs/tools.mk

@@ -14,8 +14,12 @@ MAN5   ?=
 
 install: ${EXE} ${MAN}
 	cp -f ${EXE} ${PREFIX}/bin/
+.if ${MAN1}
 	cp -f ${MAN1} ${PREFIX}/man/man1/
-	cp -f ${MAN5} ${PREFIX}/man/man5
+.endif
+.if ${MAN5}
+	cp -f ${MAN5} ${PREFIX}/man/man5/
+.endif
 
 uninstall:
 .for e in ${EXE}