From 4a6dcc8afbdcab30357d2b8a4baf40ed383cacf1 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Mon, 18 Oct 2021 21:06:39 +0200
Subject: [PATCH] fewer makefiles
---
Makefile | 6 +++++-
encoding/Makefile | 3 ++-
mk/lambdapi.mk | 25 +++++++++++++++++++++++++
specs/src/dk-sig.lisp | 4 ++--
specs/tools/.gitignore | 3 +++
specs/tools/lambdapi.mk | 19 +++----------------
specs/tools/prelude/Makefile | 2 +-
tools/lambdapi.mk | 14 --------------
8 files changed, 41 insertions(+), 35 deletions(-)
create mode 100644 mk/lambdapi.mk
create mode 100644 specs/tools/.gitignore
delete mode 100644 tools/lambdapi.mk
diff --git a/Makefile b/Makefile
index df01951..1e92572 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,11 @@
.PHONY: install
install:
${MAKE} -C encoding install
- @sed 's:PVSDKPATH:${PWD}:' tools/load-personoj.lisp | cat
+ @echo "Add to ~/.pvs.lisp:"
+ @echo "--------8<----------"
+ cat tools/load-personoj.lisp
+ @echo "(load-personoj)"
+ @echo "--------8<----------"
.PHONY: encoding
encoding:
diff --git a/encoding/Makefile b/encoding/Makefile
index 662be10..43705c2 100644
--- a/encoding/Makefile
+++ b/encoding/Makefile
@@ -1,3 +1,4 @@
+LP = lambdapi
LP_SRC != find . -type f -name "*.lp"
-.include "../lambdapi.mk"
+.include "../mk/lambdapi.mk"
diff --git a/mk/lambdapi.mk b/mk/lambdapi.mk
new file mode 100644
index 0000000..6e52f01
--- /dev/null
+++ b/mk/lambdapi.mk
@@ -0,0 +1,25 @@
+# -*- mode: Makefile; tab-width: 4; -*-
+# ex:ts=4 sw=4 filetype=make:
+
+LP_SRC ?=
+LP_OBJ ?= ${LP_SRC:S/.lp$/.lpo/}
+LP_FLAGS ?= -v0 -w --gen-obj
+
+all: ${LP_OBJ}
+
+.SUFFIXES: .lp .lpo
+
+.lp.lpo:
+ ${LP} check ${LP_FLAGS} ${.IMPSRC}
+
+.PHONY: install
+install: lambdapi.pkg ${LP_SRC} ${LP_OBJ}
+ ${LP} install ${LP_SRC} ${LP_OBJ}
+
+.PHONY: uninstall
+uninstall:
+ ${LP} uninstall
+
+.PHONY: clean
+clean:
+ find . -name '*.lpo' -exec rm -f {} +
diff --git a/specs/src/dk-sig.lisp b/specs/src/dk-sig.lisp
index b3a037e..5c22f42 100644
--- a/specs/src/dk-sig.lisp
+++ b/specs/src/dk-sig.lisp
@@ -29,8 +29,8 @@ symbols as they appear in PVS to a list of variants."
(declaim (ftype (function (symbol list) integer) count-definitions))
(defun count-definitions (sym sigs)
"Count the number of definitions of symbol SYM inside signatures SIGS"
- (flet ((count (sig) (aif (gethash sym (signature-decls sig)) (length it) 0)))
- (funcall (lrec (lambda (sig f) (+ (count sig) (funcall f))) 0) sigs)))
+ (flet ((count-sig (sig) (aif (gethash sym (signature-decls sig)) (length it) 0)))
+ (funcall (lrec (lambda (sig f) (+ (count-sig sig) (funcall f))) 0) sigs)))
(declaim (ftype (function (integer) string) mksuffix))
(defun mksuffix (n)
diff --git a/specs/tools/.gitignore b/specs/tools/.gitignore
new file mode 100644
index 0000000..0b5ea42
--- /dev/null
+++ b/specs/tools/.gitignore
@@ -0,0 +1,3 @@
+*.lp
+*.lpo
+*.lisp
diff --git a/specs/tools/lambdapi.mk b/specs/tools/lambdapi.mk
index ab8efaf..066d9ff 100644
--- a/specs/tools/lambdapi.mk
+++ b/specs/tools/lambdapi.mk
@@ -1,23 +1,10 @@
LP ?= lambdapi
-LP_FLAGS ?= -v0 -w
LP_SRC ?=
-LP_OBJ ?= ${LP_SRC:S/.lp$/.lpo/}
-
-.SUFFIXES: .lpo .lp
all: ${LP_OBJ}
-.lp.lpo:
- ${LP} check ${LP_FLAGS} --gen-obj $<
-
-.PHONY: install
-install: lambdapi.pkg ${LP_SR} ${LP_OBJ}
- ${LP} install ${LP_SRC} ${LP_OBJ}
-
-.PHONY: uninstall
-uninstall:
- ${LP} uninstall
-
.PHONY: clean
clean:
- rm -f ${LP_OBJ}
+ rm -rf *.lpo *.lp *.lisp
+
+.include "../../../mk/lambdapi.mk"
diff --git a/specs/tools/prelude/Makefile b/specs/tools/prelude/Makefile
index bc89ebe..2e1b329 100644
--- a/specs/tools/prelude/Makefile
+++ b/specs/tools/prelude/Makefile
@@ -1,5 +1,5 @@
PVS2DK = ../pvs2dk.sh
-LPC = lambdapi check
+LP = lambdapi
THEORIES != grep -v -E '^-|\#' theories
PVSPATH ?=
diff --git a/tools/lambdapi.mk b/tools/lambdapi.mk
deleted file mode 100644
index f8abb2b..0000000
--- a/tools/lambdapi.mk
+++ /dev/null
@@ -1,14 +0,0 @@
-#-*- mode: Makefile; tab-width: 4; -*-
-# ex:ts=4 sw=4 filetype=make:
-
-# lambdapi check command
-LPC ?=
-
-.SUFFIXES: .lp .lpo
-
-.lp.lpo:
- ${LPC} -v0 -w --gen-obj ${.IMPSRC}
-
-.PHONY: clean
-clean:
- rm -rf *.lp *.lpo *.lisp
--
GitLab