aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile1
-rw-r--r--Makefile.build7
-rw-r--r--Makefile.common1
-rw-r--r--test-suite/Makefile22
-rw-r--r--test-suite/misc/universes/universes.v2
5 files changed, 31 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 6ddef407a..10b102932 100644
--- a/Makefile
+++ b/Makefile
@@ -194,6 +194,7 @@ docclean:
archclean: clean-ide optclean voclean
rm -rf _build myocamlbuild_config.ml
+ rm -f $(ALLSTDLIB).*
optclean:
rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
diff --git a/Makefile.build b/Makefile.build
index 2f5b43303..b2b311a4f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -369,11 +369,16 @@ validate:: $(BESTCHICKEN) $(ALLVO)
$(SHOW)'COQCHK <theories & plugins>'
$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
+.PHONY: $(ALLSTDLIB).v
+$(ALLSTDLIB).v:
+ $(SHOW)'MAKE $(notdir $@)'
+ $(HIDE)echo "Require $(ALLMODS)." > $@
+
MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE)
check:: validate test-suite
-test-suite: world
+test-suite: world $(ALLSTDLIB).v
$(MAKE) $(MAKE_TSOPTS) clean
$(MAKE) $(MAKE_TSOPTS) all
$(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi
diff --git a/Makefile.common b/Makefile.common
index b2581776a..fa76dac60 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -321,6 +321,7 @@ PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
ALLVO:= $(THEORIESVO) $(PLUGINSVO)
VFILES:= $(ALLVO:.vo=.v)
+ALLSTDLIB := test-suite/misc/universes/all_stdlib
# convert a (stdlib) filename into a module name:
# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6c3d59dfd..8e28b0697 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -354,7 +354,7 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.
# Miscellaneous tests
#######################################################################
-misc: misc/xml.log misc/deps-order.log
+misc: misc/xml.log misc/deps-order.log misc/universes.log
# Test xml compilation
xml: misc/xml.log
@@ -400,3 +400,23 @@ misc/deps-order.log:
fi; \
rm $$tmpoutput; \
} > "$@"
+
+# Sort universes for the whole standard library
+EXPECTED_UNIVERSES := 3
+universes: misc/universes.log
+misc/universes.log:
+ @echo "TEST misc/universes"
+ $(HIDE){ \
+ $(bincoqc) -I misc/universes misc/universes/all_stdlib 2>&1; \
+ $(bincoqc) -I misc/universes misc/universes/universes 2>&1; \
+ mv universes.txt misc/universes; \
+ N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
+ times; \
+ if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \
+ echo $(log_success); \
+ echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \
+ else \
+ echo $(log_failure); \
+ echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \
+ fi; \
+ } > "$@"
diff --git a/test-suite/misc/universes/universes.v b/test-suite/misc/universes/universes.v
new file mode 100644
index 000000000..b7c7ed812
--- /dev/null
+++ b/test-suite/misc/universes/universes.v
@@ -0,0 +1,2 @@
+Require all_stdlib.
+Print Sorted Universes "universes.txt".