diff options
| -rw-r--r-- | .dockerignore | 1 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 9 | ||||
| -rw-r--r-- | Dockerfile.make | 3 | ||||
| -rw-r--r-- | etc/utils/hierarchy.ml | 8 | ||||
| -rw-r--r-- | mathcomp/Make.test-suite | 7 | ||||
| -rw-r--r-- | mathcomp/Makefile.common | 40 | ||||
| -rw-r--r-- | mathcomp/Makefile.coq.local | 8 |
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 |