aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-18 16:42:43 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-18 16:42:43 +0000
commita66a16e2e1d3264d87eaac66a809ec5e26849044 (patch)
treea76c0722da5be97c388baba8c0b864de8c1e1b7c /test-suite
parentf418ecb6a2915a8b8b9fd5598ced5376cbcb75bc (diff)
Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in
coqdep since it is now deterministic (later -R's overwriting former ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile45
-rw-r--r--test-suite/misc/deps/client/bar.v11
-rw-r--r--test-suite/misc/deps/client/foo.v1
-rw-r--r--test-suite/misc/deps/deps.out1
-rw-r--r--test-suite/misc/deps/lib/foo.v1
5 files changed, 51 insertions, 8 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2503368f6..62d443d09 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -40,6 +40,7 @@ endif
command := $(coqtop) -top Top -load-vernac-source
coqc := $(coqtop) -compile
+coqdep := $(BIN)coqdep
SHOW := $(if $(VERBOSE),@true,@echo)
HIDE := $(if $(VERBOSE),,@)
@@ -74,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
interactive micromega $(COMPLEXITY) modules
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) xml bugs
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs
#######################################################################
# Phony targets
@@ -114,7 +115,6 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S))))
# Summary
#######################################################################
-summary_one = echo $(1); if [ -f $(2).log ]; then tail -n1 $(2).log; fi | sort -g
summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g
.PHONY: summary summary.log
@@ -128,7 +128,7 @@ summary:
$(call summary_dir, "Output tests", output); \
$(call summary_dir, "Interactive tests", interactive); \
$(call summary_dir, "Micromega tests", micromega); \
- $(call summary_one, "Miscellaneous tests", xml); \
+ $(call summary_dir, "Miscellaneous tests", misc); \
$(call summary_dir, "Complexity tests", complexity); \
$(call summary_dir, "Module tests", modules); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
@@ -354,10 +354,12 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.
# Miscellaneous tests
#######################################################################
+misc: misc/xml.log misc/deps-order.log
+
# Test xml compilation
-xml: xml.log
-xml.log:
- @echo "TEST xml"
+xml: misc/xml.log
+misc/xml.log:
+ @echo "TEST misc/xml"
$(HIDE){ \
echo $(call log_intro,xml); \
rm -rf misc/xml; \
@@ -365,9 +367,36 @@ xml.log:
$(bincoqc) -xml misc/berardi_test 2>&1; times; \
if [ ! -d misc/xml ]; then \
echo $(log_failure); \
- echo " xml... failed"; \
+ echo " misc/xml... failed"; \
else \
echo $(log_success); \
- echo " xml...apparently ok"; \
+ echo " misc/xml...apparently ok"; \
fi; rm -r misc/xml; \
} > "$@"
+
+# Check that both coqdep and coqtop/coqc takes the later -I/-R
+# Check that both coqdep and coqtop/coqc supports both -R and -I dir -as lib
+# See bugs 2242, 2337, 2339
+deps-order: misc/deps-order.log
+misc/deps-order.log:
+ @echo "TEST misc/deps-order"
+ $(HIDE){ \
+ echo $(call log_intro,deps-order); \
+ rm -f misc/deps/*/*.vo; \
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+ $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \
+ | head -n 1 > $$tmpoutput; \
+ diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \
+ $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \
+ $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
+ $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \
+ S=$$?; times; \
+ if [ $$R = 0 -a $$S = 0 ]; then \
+ echo $(log_success); \
+ echo " misc/deps-order...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " misc/deps-order...Error! (unexpected order)"; \
+ fi; \
+ rm $$tmpoutput; \
+ } > "$@"
diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v
new file mode 100644
index 000000000..629694186
--- /dev/null
+++ b/test-suite/misc/deps/client/bar.v
@@ -0,0 +1,11 @@
+(* We assume the file compiled with -R ../lib lib -R . client *)
+(* foo alone should refer to client.foo because -R . client comes last *)
+
+Require Import foo.
+Goal a = 1.
+reflexivity.
+Qed.
+Require Import lib.foo.
+Goal a = 0.
+reflexivity.
+Qed.
diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v
new file mode 100644
index 000000000..fc82069e5
--- /dev/null
+++ b/test-suite/misc/deps/client/foo.v
@@ -0,0 +1 @@
+Definition a := 1.
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
new file mode 100644
index 000000000..68b48d604
--- /dev/null
+++ b/test-suite/misc/deps/deps.out
@@ -0,0 +1 @@
+misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v
new file mode 100644
index 000000000..b745fbd48
--- /dev/null
+++ b/test-suite/misc/deps/lib/foo.v
@@ -0,0 +1 @@
+Definition a := 0.