Fix and improve the test suite and Makefile

- improve an error message produced by the `check_join` tactic,
- fix the build of the test suite: `make test-suite`, and
- add a new rule `only` to build a subset of MathComp.

7 files changed, 61 insertions, 15 deletions

diff --git a/.dockerignore b/.dockerignore
index 82209d9..1d553c8 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -8,6 +8,7 @@
 !*.opam
 !plugin
 !mathcomp
+!etc/utils/hierarchy.ml
 
 **/*.d
 **/*.vo
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5e996b9..9593f38 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -32,3 +32,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Generalized the `allpairs_catr` lemma to the case where the types of `s`,
   `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`.
 
+### Infrastructure
+
+- `Makefile` now supports the `test-suite` and `only` targets. Currently,
+  `make test-suite` will verify the implementation of mathematical structures
+  and their inheritances of MathComp automatically, by using the `hierarchy.ml`
+  utility. One can use the `only` target to build the sub-libraries of MathComp
+  specified by the `TGTS` variable, e.g.,
+  `make only TGTS="ssreflect/all_ssreflect.vo fingroup/all_fingroup.vo"`.
+
diff --git a/Dockerfile.make b/Dockerfile.make
index 7972ad7..1a1dfc2 100644
--- a/Dockerfile.make
+++ b/Dockerfile.make
@@ -26,4 +26,5 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && cd mathcomp \
   && make Makefile.coq \
   && make -f Makefile.coq -j ${NJOBS} all \
-  && make -f Makefile.coq install"]
+  && make -f Makefile.coq install \
+  && make test-suite"]
diff --git a/etc/utils/hierarchy.ml b/etc/utils/hierarchy.ml
index 33d598a..2bb7f6f 100644
--- a/etc/utils/hierarchy.ml
+++ b/etc/utils/hierarchy.ml
@@ -159,7 +159,13 @@ Tactic Notation "check_join"
       _ (_ ?Tjoin) => Tjoin | _ ?Tjoin => Tjoin | ?Tjoin => Tjoin
     end
   in
-  is_evar Tjoin;
+  match tt with
+    | _ => is_evar Tjoin
+    | _ =>
+      let Tjoin := eval simpl in (Tjoin : Type) in
+      fail "The join of" t1 "and" t2 "is a concrete type" Tjoin
+           "but is expected to be" tjoin
+  end;
   let tjoin' := type of Tjoin in
   lazymatch tjoin' with
     | tjoin => idtac
diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite
new file mode 100644
index 0000000..bca6ed9
--- /dev/null
+++ b/mathcomp/Make.test-suite
@@ -0,0 +1,7 @@
+test_suite/hierarchy_test.v
+
+-I .
+-R . mathcomp
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index c523410..8e84ccc 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -2,8 +2,15 @@
 
 ######################################################################
 # USAGE:                                                             #
-# The rules this-config::, this-build::, this-distclean::,           #
-# pre-makefile::, this-clean:: and __always__:: may be extended      #
+#                                                                    #
+# make all: Build the MathComp library entirely,                     #
+# make test-suite: Run the test suite,                               #
+# make only TGTS="...vo": Build the selected libraries of MathComp.  #
+#                                                                    #
+# The rules this-config::, this-build::, this-only::,                #
+# this-test-suite::, this-distclean::, pre-makefile::, this-clean::  #
+# and __always__:: may be extended.                                  #
+#                                                                    #
 # Additionally, the following variables may be customized:           #
 SUBDIRS?=
 COQBIN?=$(dir $(shell which coqtop))
@@ -14,15 +21,17 @@ COQMAKEOPTIONS?=
 COQMAKEFILEOPTIONS?=
 V?=
 VERBOSE?=V
+TGTS?=
 ######################################################################
 
 # local context: -----------------------------------------------------
-.PHONY: all config build clean distclean __always__
+.PHONY: all config build only test-suite clean distclean __always__
 .SUFFIXES:
 
 H:= $(if $(VERBOSE),,@)  # not used yet
 TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
 COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
+COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq VDFILE=".coqdeps.test-suite" $(COQMAKEOPTIONS)
 BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
 	      | wc -l | sed 's/ *//g')
 
@@ -45,28 +54,49 @@ all: config build
 Makefile.coq: pre-makefile $(COQPROJECT) Makefile
 	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
 
+# Test suite ---------------------------------------------------------
+
+test_suite/hierarchy_test.v: build
+	mkdir -p test_suite
+	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify -R . mathcomp -lib all.all > test_suite/hierarchy_test.v
+
+Makefile.test-suite.coq: test_suite/hierarchy_test.v
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f Make.test-suite -o Makefile.test-suite.coq
+
 # Global config, build, clean and distclean --------------------------
 config: sub-config this-config
 
 build: sub-build this-build
 
+only: sub-only this-only
+
+test-suite: sub-test-suite this-test-suite
+
 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
+.PHONY: this-config this-build this-only this-test-suite this-distclean this-clean
 
 this-config:: __always__
 
 this-build:: this-config Makefile.coq
 	+$(COQMAKE)
 
+this-only:: this-config Makefile.coq
+	+$(COQMAKE) only "TGTS=$(TGTS)"
+
+this-test-suite:: Makefile.test-suite.coq
+	+$(COQMAKE_TESTSUITE)
+
 this-distclean:: this-clean
-	rm -f Makefile.coq Makefile.coq.conf Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf
+	rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf
 
 this-clean:: __always__
 	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+	@if [ -f Makefile.test-suite.coq ]; then $(COQMAKE_TESTSUITE) cleanall; fi
 
 # Install target -----------------------------------------------------
 .PHONY: install
diff --git a/mathcomp/Makefile.coq.local b/mathcomp/Makefile.coq.local
deleted file mode 100644
index a5bbf9d..0000000
--- a/mathcomp/Makefile.coq.local
+++ /dev/null
@@ -1,8 +0,0 @@
-VOFILES += test_suite/hierarchy_test.vo
-
-test_suite/hierarchy_test.vo: test_suite/hierarchy_test.v all/all.vo
-
-test_suite/hierarchy_test.v: all/all.vo
-	mkdir -p test_suite/
-	COQBIN=$(COQBIN) ocaml ../etc/utils/hierarchy.ml -verify \
-	  -R . mathcomp -lib all.all > test_suite/hierarchy_test.v