diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 22 | ||||
| -rw-r--r-- | test-suite/misc/universes/universes.v | 2 |
2 files changed, 23 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 6c3d59dfdd..8e28b0697c 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 0000000000..b7c7ed812f --- /dev/null +++ b/test-suite/misc/universes/universes.v @@ -0,0 +1,2 @@ +Require all_stdlib. +Print Sorted Universes "universes.txt". |