Merge pull request #213 from CohenCyril/Makefile

Rework the whole Makefile architecture

16 files changed, 170 insertions, 221 deletions

diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index 07f1869..9064020 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -1,30 +1,17 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+# setting variables
+COQPROJECT?=Make
+COQMAKEOPTIONS=--no-print-directory
 
-# this sets variable V
-include ssreflect/Makefile.detect-coq-version
-# this defined coqmakefile
-include ssreflect/Makefile.coq-makefile
-
-COQDEP=$(COQBIN)coqdep
-
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# Main Makefile
+include Makefile.common
 
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,ssreflect)
-	# Override COQDEP to find only the "right" copy .ml files
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -exclude-dir plugin -c'
-
-clean: 
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,ssreflect)
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+# this sets variable V (coq version) and MLLIBEXTRA
+# assuming PLUGIN is set to the directory which contains the plugins
+# and SSR is set to the directory of the ssreflect package
+PLUGIN=../plugin
+SSR=ssreflect
+include ssreflect/Makefile.detect-coq-version
+COQMAKEFILEOPTIONS=$(MLLIBEXTRA)
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
new file mode 100644
index 0000000..557a05b
--- /dev/null
+++ b/mathcomp/Makefile.common
@@ -0,0 +1,81 @@
+# -*- Makefile -*-
+V?=
+VERBOSE?=V
+H:= $(if $(VERBOSE),,@)
+# Options
+COQBIN?=$(dir $(shell which coqtop))
+COQMAKEFILE?=$(COQBIN)coq_makefile
+COQDEP?=$(COQBIN)coqdep
+COQPROJECT?=_CoqProject
+COQMAKEOPTIONS?=
+COQMAKEFILEOPTIONS?=
+BEFOREMAKEFILE?=
+
+# --------------------------------------------------------------------
+.PHONY: all config build clean distclean __always__
+.SUFFIXES:
+
+TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
+COQMAKE = $(MAKE) -f Makefile.this $(COQMAKEOPTIONS)
+
+# --------------------------------------------------------------------
+all: config build
+
+# --------------------------------------------------------------------
+Makefile.coq: $(BEFOREMAKEFILE) Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+
+Makefile.this: $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES)
+	cat $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES) > Makefile.this
+
+__always__: Makefile.this
+# --------------------------------------------------------------------
+config: sub-config this-config Makefile.this
+
+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:: __always__
+	+$(COQMAKE)
+
+this-distclean:: this-clean $(OTHERCLEAN)
+	rm -f Makefile.coq Makefile.coq.conf Makefile.this
+
+this-clean::
+	@if [ -f Makefile.this ]; then $(COQMAKE) cleanall; fi
+
+# --------------------------------------------------------------------
+.PHONY: install
+
+install: __always__
+	$(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) $@
diff --git a/mathcomp/algebra/Makefile b/mathcomp/algebra/Makefile
index d4e1bca..47dd8b4 100644
--- a/mathcomp/algebra/Makefile
+++ b/mathcomp/algebra/Makefile
@@ -1,24 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/all/Makefile b/mathcomp/all/Makefile
index a58be7b..30204d2 100644
--- a/mathcomp/all/Makefile
+++ b/mathcomp/all/Makefile
@@ -1,22 +1,25 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# --------------------------------------------------------------------
+include Makefile.common
 
-.DEFAULT_GOAL := all
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+# --------------------------------------------------------------------
+.PHONY: install
 
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+install:
+	$(MAKE) -f Makefile.coq 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)}'
 
diff --git a/mathcomp/character/Makefile b/mathcomp/character/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/character/Makefile
+++ b/mathcomp/character/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/field/Makefile b/mathcomp/field/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/field/Makefile
+++ b/mathcomp/field/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/fingroup/Makefile b/mathcomp/fingroup/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/fingroup/Makefile
+++ b/mathcomp/fingroup/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/solvable/Makefile b/mathcomp/solvable/Makefile
index 14acb5c..47dd8b4 100644
--- a/mathcomp/solvable/Makefile
+++ b/mathcomp/solvable/Makefile
@@ -1,25 +1,10 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+COQPROJECT="Make"
 
-COQDEP=$(COQBIN)/coqdep
+# --------------------------------------------------------------------
+include ../Makefile.common
 
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
-
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -c'
-
-.PHONY: clean
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+# --------------------------------------------------------------------
+COQMAKEOPTIONS=--no-print-directory
 
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index e4474c2..c3092fc 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -1,28 +1,17 @@
-H=@
+# -*- Makefile -*-
 
-ifeq "$(COQBIN)" ""
-COQBIN=$(dir $(shell which coqtop))/
-endif
+# setting variables
+COQPROJECT?=Make
+COQMAKEOPTIONS=--no-print-directory
 
-# this sets variable V
-include Makefile.detect-coq-version
-# this defined coqmakefile
-include Makefile.coq-makefile
-
-COQDEP=$(COQBIN)coqdep
-
-OLD_MAKEFLAGS:=$(MAKEFLAGS)
-MAKEFLAGS+=-B
+# Main Makefile
+include ../Makefile.common
 
-.DEFAULT_GOAL := all
-
-%:
-	$(H)[ -e Makefile.coq ] || $(call coqmakefile,.)
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq $* \
-		COQDEP='$(COQDEP) -exclude-dir plugin -c'
+# --------------------------------------------------------------------
+# this sets variable V (coq version) and MLLIBEXTRA
+# assuming PLUGIN is set to the directory which contains the plugins
+PLUGIN=../../plugin/
+SSR=.
+include Makefile.detect-coq-version
 
-clean:
-	$(H)MAKEFLAGS="$(OLD_MAKEFLAGS)" $(MAKE) --no-print-directory \
-		-f Makefile.coq clean
-	$(H)rm -f Makefile.coq
+COQMAKEFILEOPTIONS=$(MLLIBEXTRA)
diff --git a/mathcomp/ssreflect/Makefile.coq-makefile b/mathcomp/ssreflect/Makefile.coq-makefile
deleted file mode 100644
index ba0e5d7..0000000
--- a/mathcomp/ssreflect/Makefile.coq-makefile
+++ /dev/null
@@ -1,32 +0,0 @@
-define coqmakefile
-	(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
-	if [ "$$OS" = "Windows_NT" ]; then LN=cp; else LN="ln -sfr"; fi;\
-	MLLIB=;\
-	EXTRA=;\
-	case $(V) in\
-	v8.5*|v8.4*)\
-		$$LN $(1)/plugin/$(V)/ssrmatching_plugin.mllib .;\
-		$$LN $(1)/plugin/$(V)/ssrmatching.mli .;\
-		$$LN $(1)/plugin/$(V)/ssrmatching.ml4 .;\
-		$$LN $(1)/plugin/$(V)/ssrmatching.v $(1)/;\
-		$$LN $(1)/plugin/$(V)/ssreflect_plugin.mllib .;\
-		$$LN $(1)/plugin/$(V)/ssreflect.ml4 .;\
-		$$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\
-		$$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\
-		$$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\
-		MLLIB="ssrmatching_plugin.mllib ssreflect_plugin.mllib";\
-		EXTRA="ssrmatching.mli ssrmatching.ml4 ssreflect.ml4";\
-	;;\
-	v8.6*)\
-		$$LN $(1)/plugin/$(V)/ssreflect_plugin.mlpack .;\
-		$$LN $(1)/plugin/$(V)/ssreflect.ml4 .;\
-		$$LN $(1)/plugin/$(V)/ssrbool.v $(1)/;\
-		$$LN $(1)/plugin/$(V)/ssrfun.v $(1)/;\
-		$$LN $(1)/plugin/$(V)/ssreflect.v $(1)/;\
-		MLLIB=ssreflect_plugin.mlpack;\
-		EXTRA="ssreflect.ml4";\
-	;;\
-	esac;\
-	$(COQBIN)coq_makefile -f Make $$MLLIB $$EXTRA -o Makefile.coq)
-endef
-
diff --git a/mathcomp/ssreflect/Makefile.detect-coq-version b/mathcomp/ssreflect/Makefile.detect-coq-version
index 9c00aa3..0f7d9de 100644
--- a/mathcomp/ssreflect/Makefile.detect-coq-version
+++ b/mathcomp/ssreflect/Makefile.detect-coq-version
@@ -1,25 +1,20 @@
-BRANCH_coq = $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
+BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	     | wc -l | sed 's/ *//g')
 
 ifneq "$(BRANCH_coq)" "0"
-BRANCH_coq = trunk
+BRANCH_coq:= master
 else
-BRANCH_coq = $(shell $(COQBIN)coqtop -v | head -1 \
-	     | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/v\1/')
+BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 \
+	     | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/\1/')
 endif
 
-HASH_coq = $(shell echo Quit. | $(COQBIN)coqtop 2>/dev/null | head -1 \
-	   | sed 's/^.*(\([a-f0-9]*\)).*/\1/' )
+V:=$(BRANCH_coq)
 
-HASH_coq_v85beta1 = eaa3d0b15adf4eb11ffb00ab087746a5b15c4d5d
-HASH_coq_v85beta2 = 94afd8996251c30d2188a75934487009538e1303
-
-V=$(BRANCH_coq)
-ifeq "$(HASH_coq)" "$(HASH_coq_v85beta1)"
-V=v8.5beta1
-$(error "$(V) not supported: From X Require Y does not find X.Z.Y, use 8.4 or 8.5 > beta2")
-endif
-ifeq "$(HASH_coq)" "$(HASH_coq_v85beta2)"
-V=v8.5beta2
-$(error "$(V) not supported: From X Require Y does not find X.Z.Y (in coqdep), use 8.4 or 8.5 > beta2")
-endif
+MLLIBEXTRA:=$(shell \
+	if [ $(V) = "8.6" ];\
+	   then cp $(PLUGIN)/v$(V)/ssreflect_plugin.mlpack .;\
+		cp $(PLUGIN)/v$(V)/ssreflect.ml4 .;\
+		cp $(PLUGIN)/v$(V)/ssrbool.v $(SSR)/;\
+		cp $(PLUGIN)/v$(V)/ssrfun.v $(SSR)/;\
+		cp $(PLUGIN)/v$(V)/ssreflect.v $(SSR)/;\
+		echo "ssreflect_plugin.mlpack ssreflect.ml4"; fi)
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/plugin/v8.6/ssrbool.v
index 2342ec6..2342ec6 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
+++ b/plugin/v8.6/ssrbool.v
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4 b/plugin/v8.6/ssreflect.ml4
index 25d3287..25d3287 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.ml4
+++ b/plugin/v8.6/ssreflect.ml4
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/plugin/v8.6/ssreflect.v
index e63b45b..e63b45b 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
+++ b/plugin/v8.6/ssreflect.v
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect_plugin.mlpack b/plugin/v8.6/ssreflect_plugin.mlpack
index 006b70f..006b70f 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect_plugin.mlpack
+++ b/plugin/v8.6/ssreflect_plugin.mlpack
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v b/plugin/v8.6/ssrfun.v
index 7cb30ff..7cb30ff 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v
+++ b/plugin/v8.6/ssrfun.v