diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-25 07:02:13 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-25 07:02:13 +0000 |
| commit | 8966d6291e76dba17bedd5f04402d4cd5f4e9da7 (patch) | |
| tree | e46dd0d4b47f887ff34ae6e238effdf178c4299f | |
| parent | d2158a37af31ade57496fd846312bc63a0547ad3 (diff) | |
Add a test for sorting all universes of stdlib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | Makefile.build | 7 | ||||
| -rw-r--r-- | Makefile.common | 1 | ||||
| -rw-r--r-- | test-suite/Makefile | 22 | ||||
| -rw-r--r-- | test-suite/misc/universes/universes.v | 2 |
5 files changed, 31 insertions, 2 deletions
@@ -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". |