aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Makefile.common
diff options
context:
space:
mode:
authorCyril Cohen2018-07-31 10:37:25 +0200
committerCyril Cohen2018-07-31 11:38:53 +0200
commit4199c23da311e612cb1ae45cf5519b5f3947c3b3 (patch)
tree4e887d501dd9d1f5d983ca236cbadcd803c8a091 /mathcomp/Makefile.common
parent6c6c907438f4179ac335e7daa9f1ed030c0c8259 (diff)
Rework the whole Makefile architecture
- Cleanup, refactoring and generalize the makefile architecture - Reuses @strub math-comp/analysis Makefile / Makefile.common organization - As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
Diffstat (limited to 'mathcomp/Makefile.common')
-rw-r--r--mathcomp/Makefile.common78
1 files changed, 78 insertions, 0 deletions
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
new file mode 100644
index 0000000..b07b78d
--- /dev/null
+++ b/mathcomp/Makefile.common
@@ -0,0 +1,78 @@
+# -*- Makefile -*-
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+ifeq "$(COQMAKEFILE)" ""
+COQMAKEFILE=$(COQBIN)coq_makefile
+endif
+COQDEP=$(COQBIN)coqdep
+
+ifeq "$(COQPROJECT)" ""
+COQPROJECT="_CoqProject"
+endif
+
+# --------------------------------------------------------------------
+.PHONY: all config build clean distclean __always__
+.SUFFIXES:
+
+TOP = $(dir $(lastword $(MAKEFILE_LIST)))
+COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
+
+# --------------------------------------------------------------------
+all: config build
+
+# --------------------------------------------------------------------
+Makefile.coq: Makefile $(BEFOREMAKEFILE)
+ $(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+
+# --------------------------------------------------------------------
+config: sub-config this-config Makefile.coq
+
+build: sub-build this-build
+
+clean: sub-clean this-clean
+
+distclean: sub-distclean this-distclean
+
+# --------------------------------------------------------------------
+.PHONY: this-config this-build this-distclean this-clean
+
+this-build::
+ +$(COQMAKE)
+
+this-distclean:: this-clean
+ rm -f Makefile.coq Makefile.coq.conf
+
+this-clean::
+ @if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+
+# --------------------------------------------------------------------
+.PHONY: install
+
+install:
+ $(COQMAKE) install
+# --------------------------------------------------------------------
+.PHONY: count
+
+COQFILES := $(shell grep '.v$$' Make)
+
+count:
+ @coqwc $(COQFILES) | tail -1 | \
+ awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
+# --------------------------------------------------------------------
+this-distclean::
+ rm -f $(shell find . -name '*~')
+
+# --------------------------------------------------------------------
+ifdef SUBDIRS
+sub-%: __always__
+ @set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
+else
+sub-%: __always__
+ @true
+endif
+
+# --------------------------------------------------------------------
+%.vo: __always__
+ +$(COQMAKE) $@