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

6 files changed, 52 insertions, 9 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.
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 797c25ccc..a2d908339 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -137,7 +137,7 @@ let warning_clash file dir =
       let d2 = Filename.dirname f2 in
       let dl = List.map Filename.dirname (List.rev fl) in
       eprintf
-        "*** Warning: in file %s, \n    required library %s is ambiguous!\n    (found %s.v in "
+        "*** Warning: in file %s, \n    required library %s matches several files in path\n    (found %s.v in "
         file (String.concat "." dir) f;
       List.iter (fun s -> eprintf "%s, " s) dl;
       eprintf "%s and %s; used the latter)\n" d2 d1