From b83fe0ed8a8e7258c8cf55178dd619b743c8342e Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 1 Aug 2018 13:14:39 +0200
Subject: simplified, cleaned and documented Makefile.common

---
 mathcomp/Makefile                              |  2 +-
 mathcomp/Makefile.common                       | 62 ++++++++++++++------------
 mathcomp/ssreflect/Makefile                    |  3 +-
 mathcomp/ssreflect/Makefile.detect-coq-version | 18 ++++----
 4 files changed, 44 insertions(+), 41 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/Makefile b/mathcomp/Makefile
index 9064020..c631c7b 100644
--- a/mathcomp/Makefile
+++ b/mathcomp/Makefile
@@ -8,7 +8,7 @@ COQMAKEOPTIONS=--no-print-directory
 include Makefile.common
 
 # --------------------------------------------------------------------
-# this sets variable V (coq version) and MLLIBEXTRA
+# this sets variables COQVERSION 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
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index 557a05b..3f45682 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -1,36 +1,40 @@
 # -*- Makefile -*-
-V?=
-VERBOSE?=V
-H:= $(if $(VERBOSE),,@)
-# Options
+
+######################################################################
+# USAGE:                                                             #
+# The rules this-config::, this-build::, this-distclean::,           #
+# pre-makefile::, this-clean:: and __always__:: may be extended      #
+# Additionally, the following variables may be customized:           #
+SUBDIRS?=
 COQBIN?=$(dir $(shell which coqtop))
 COQMAKEFILE?=$(COQBIN)coq_makefile
 COQDEP?=$(COQBIN)coqdep
 COQPROJECT?=_CoqProject
 COQMAKEOPTIONS?=
 COQMAKEFILEOPTIONS?=
-BEFOREMAKEFILE?=
+V?=
+VERBOSE?=V
+######################################################################
 
-# --------------------------------------------------------------------
+# local context: -----------------------------------------------------
 .PHONY: all config build clean distclean __always__
 .SUFFIXES:
 
+H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
-COQMAKE = $(MAKE) -f Makefile.this $(COQMAKEOPTIONS)
+COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
 
-# --------------------------------------------------------------------
+# all: ---------------------------------------------------------------
 all: config build
 
-# --------------------------------------------------------------------
-Makefile.coq: $(BEFOREMAKEFILE) Makefile
-	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+# Makefile.coq: ------------------------------------------------------
+.PHONY: pre-makefile
 
-Makefile.this: $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES)
-	cat $(BEFOREMAKEFILES) Makefile.coq $(AFTERMAKEFILES) > Makefile.this
+Makefile.coq: pre-makefile Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
 
-__always__: Makefile.this
-# --------------------------------------------------------------------
-config: sub-config this-config Makefile.this
+# Global config, build, clean and distclean --------------------------
+config: sub-config this-config
 
 build: sub-build this-build
 
@@ -38,24 +42,26 @@ clean: sub-clean this-clean
 
 distclean: sub-distclean this-distclean
 
-# --------------------------------------------------------------------
+# Local config, build, clean and distclean ---------------------------
 .PHONY: this-config this-build this-distclean this-clean
 
-this-build:: __always__
+this-config:: __always__
+
+this-build:: this-config Makefile.coq
 	+$(COQMAKE)
 
 this-distclean:: this-clean $(OTHERCLEAN)
-	rm -f Makefile.coq Makefile.coq.conf Makefile.this
+	rm -f Makefile.coq Makefile.coq.conf Makefile.coq
 
-this-clean::
-	@if [ -f Makefile.this ]; then $(COQMAKE) cleanall; fi
+this-clean:: __always__
+	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
 
-# --------------------------------------------------------------------
+# Install target -----------------------------------------------------
 .PHONY: install
 
-install: __always__
+install: __always__ Makefile.coq
 	$(COQMAKE) install
-# --------------------------------------------------------------------
+# counting lines of Coq code -----------------------------------------
 .PHONY: count
 
 COQFILES := $(shell grep '.v$$' Make)
@@ -63,11 +69,11 @@ COQFILES := $(shell grep '.v$$' Make)
 count:
 	@coqwc $(COQFILES) | tail -1 | \
 	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
-# --------------------------------------------------------------------
+# Additionally cleaning backup (*~) files ----------------------------
 this-distclean::
 	rm -f $(shell find . -name '*~')
 
-# --------------------------------------------------------------------
+# Make in SUBDIRS ----------------------------------------------------
 ifdef SUBDIRS
 sub-%: __always__
 	@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
@@ -76,6 +82,6 @@ sub-%: __always__
 	@true
 endif
 
-# --------------------------------------------------------------------
-%.vo: __always__
+# Make of individual .vo ---------------------------------------------
+%.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index c3092fc..76b8c2c 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -8,10 +8,9 @@ COQMAKEOPTIONS=--no-print-directory
 include ../Makefile.common
 
 # --------------------------------------------------------------------
-# this sets variable V (coq version) and MLLIBEXTRA
+# this sets variables COQVERSION and MLLIBEXTRA
 # assuming PLUGIN is set to the directory which contains the plugins
 PLUGIN=../../plugin/
 SSR=.
 include Makefile.detect-coq-version
-
 COQMAKEFILEOPTIONS=$(MLLIBEXTRA)
diff --git a/mathcomp/ssreflect/Makefile.detect-coq-version b/mathcomp/ssreflect/Makefile.detect-coq-version
index 0f7d9de..c6a981a 100644
--- a/mathcomp/ssreflect/Makefile.detect-coq-version
+++ b/mathcomp/ssreflect/Makefile.detect-coq-version
@@ -2,19 +2,17 @@ BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	     | wc -l | sed 's/ *//g')
 
 ifneq "$(BRANCH_coq)" "0"
-BRANCH_coq:= master
+COQVERSION:= master
 else
-BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 \
+COQVERSION:= $(shell $(COQBIN)coqtop -v | head -1 \
 	     | sed 's/.*version \([0-9]\.[0-9]\)[^ ]* .*/\1/')
 endif
 
-V:=$(BRANCH_coq)
-
 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)/;\
+	if [ $(COQVERSION) = "8.6" ];\
+	   then cp $(PLUGIN)/v$(COQVERSION)/ssreflect_plugin.mlpack .;\
+		cp $(PLUGIN)/v$(COQVERSION)/ssreflect.ml4 .;\
+		cp $(PLUGIN)/v$(COQVERSION)/ssrbool.v $(SSR)/;\
+		cp $(PLUGIN)/v$(COQVERSION)/ssrfun.v $(SSR)/;\
+		cp $(PLUGIN)/v$(COQVERSION)/ssreflect.v $(SSR)/;\
 		echo "ssreflect_plugin.mlpack ssreflect.ml4"; fi)
-- 
cgit v1.2.3