From 551f8e766b6556d9f206729af038aa4cf19499b4 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Thu, 25 Nov 2021 14:10:17 +0100
Subject: [PATCH] dune makefile, pipeline directory
---
proofs/Makefile | 26 --------------------
proofs/appaxiom/Makefile | 19 +++-----------
proofs/chainprops/Makefile | 19 +++-----------
proofs/dopth/Makefile | 16 ++----------
proofs/dune-exe.mk | 30 +++++++++++++++++++++++
proofs/{ => pipeline}/examples/.gitignore | 4 +++
proofs/{ => pipeline}/examples/hello.prf | 0
proofs/{ => pipeline}/examples/hello.pvs | 0
proofs/pipeline/examples/lambdapi.pkg | 2 ++
proofs/tools.mk | 6 ++++-
10 files changed, 49 insertions(+), 73 deletions(-)
delete mode 100644 proofs/Makefile
create mode 100644 proofs/dune-exe.mk
rename proofs/{ => pipeline}/examples/.gitignore (51%)
rename proofs/{ => pipeline}/examples/hello.prf (100%)
rename proofs/{ => pipeline}/examples/hello.pvs (100%)
create mode 100644 proofs/pipeline/examples/lambdapi.pkg
diff --git a/proofs/Makefile b/proofs/Makefile
deleted file mode 100644
index eb3bce6..0000000
--- a/proofs/Makefile
+++ /dev/null
@@ -1,26 +0,0 @@
-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
diff --git a/proofs/appaxiom/Makefile b/proofs/appaxiom/Makefile
index 8dfc4f4..a5a2240 100644
--- a/proofs/appaxiom/Makefile
+++ b/proofs/appaxiom/Makefile
@@ -1,18 +1,5 @@
-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"
diff --git a/proofs/chainprops/Makefile b/proofs/chainprops/Makefile
index ff59596..e9f658e 100644
--- a/proofs/chainprops/Makefile
+++ b/proofs/chainprops/Makefile
@@ -1,18 +1,5 @@
-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"
diff --git a/proofs/dopth/Makefile b/proofs/dopth/Makefile
index 6096f16..272bda4 100644
--- a/proofs/dopth/Makefile
+++ b/proofs/dopth/Makefile
@@ -1,16 +1,4 @@
-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"
diff --git a/proofs/dune-exe.mk b/proofs/dune-exe.mk
new file mode 100644
index 0000000..bc595aa
--- /dev/null
+++ b/proofs/dune-exe.mk
@@ -0,0 +1,30 @@
+# 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
diff --git a/proofs/examples/.gitignore b/proofs/pipeline/examples/.gitignore
similarity index 51%
rename from proofs/examples/.gitignore
rename to proofs/pipeline/examples/.gitignore
index 6ddd9b7..634104e 100644
--- a/proofs/examples/.gitignore
+++ b/proofs/pipeline/examples/.gitignore
@@ -3,3 +3,7 @@
*.summary
pvsbin/
.pvscontext
+*.json
+*.lp
+orphaned-proof.prf
+*.dep
diff --git a/proofs/examples/hello.prf b/proofs/pipeline/examples/hello.prf
similarity index 100%
rename from proofs/examples/hello.prf
rename to proofs/pipeline/examples/hello.prf
diff --git a/proofs/examples/hello.pvs b/proofs/pipeline/examples/hello.pvs
similarity index 100%
rename from proofs/examples/hello.pvs
rename to proofs/pipeline/examples/hello.pvs
diff --git a/proofs/pipeline/examples/lambdapi.pkg b/proofs/pipeline/examples/lambdapi.pkg
new file mode 100644
index 0000000..5fdd611
--- /dev/null
+++ b/proofs/pipeline/examples/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name = lpvs
+root_path = lpvs
diff --git a/proofs/tools.mk b/proofs/tools.mk
index 35db2b0..5a16eb8 100644
--- a/proofs/tools.mk
+++ b/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}
--
GitLab