Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)

24 files changed, 41 insertions, 76 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5ab4cacda..beb80a3df 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -27,8 +27,8 @@
 
 # Default value when called from a freshly compiled Coq, but can be
 # easily overridden
-LIB := $(shell cd ..; pwd)
-BIN := $(LIB)/bin/
+LIB := ..
+BIN := $(shell cd ..; pwd)/bin/
 
 coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
 coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
@@ -170,6 +170,7 @@ summary.log:
 report: summary.log
 	$(HIDE)./save-logs.sh
 	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi
+	$(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
 
 #######################################################################
@@ -293,7 +294,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	    | grep -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$tmpoutput; \
-	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
+	  diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -328,7 +329,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 		-e 's/\s*[-+]inf\s*//g' \
 		-e 's/^[^a-zA-Z]*//' \
 	       $*.out | sort > $$tmpexpected; \
-	  diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
+	  diff  --strip-trailing-cr -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -445,7 +446,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
+	  $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh
index e98da17c7..e7de90ff2 100755
--- a/test-suite/coq-makefile/arg/run.sh
+++ b/test-suite/coq-makefile/arg/run.sh
@@ -1,9 +1,7 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh
index 28d9878f9..221dcd7bf 100755
--- a/test-suite/coq-makefile/compat-subdirs/run.sh
+++ b/test-suite/coq-makefile/compat-subdirs/run.sh
@@ -1,9 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
+
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 exec test -f "subdir/done"
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index e8291c89d..1feff7479 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index e8291c89d..1feff7479 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh
index ea5792a93..221dcd7bf 100755
--- a/test-suite/coq-makefile/extend-subdirs/run.sh
+++ b/test-suite/coq-makefile/extend-subdirs/run.sh
@@ -1,10 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 exec test -f "subdir/done"
diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh
index 214a9d5b2..b2c5d5669 100755
--- a/test-suite/coq-makefile/latex1/run.sh
+++ b/test-suite/coq-makefile/latex1/run.sh
@@ -1,13 +1,11 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 if which pdflatex; then
 
 . ../template/init.sh
 	
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 exec make all.pdf
 
diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh
index 752c0c2ce..1f262a939 100755
--- a/test-suite/coq-makefile/merlin1/run.sh
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make .merlin
 cat > desired <<EOT
 B src
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 10a200dde..51669f28f 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -1,16 +1,14 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 10a200dde..51669f28f 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -1,16 +1,14 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 3cd1ac305..d3bb53106 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -1,19 +1,17 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 cp -r theories theories2
 mv src/test_plugin.mlpack src/test_plugin.mllib
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 9f6295d64..3bec11cb7 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -1,19 +1,17 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true
 if [[ `which ocamlopt` && $NATIVECOMP ]]; then
 
 . ../template/init.sh
 	
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh
index 2ea3deffb..8cf04bf2c 100755
--- a/test-suite/coq-makefile/only/run.sh
+++ b/test-suite/coq-makefile/only/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make only TGTS="src/test.cmi src/test_aux.cmi" -j2
 test -f src/test.cmi
 test -f src/test_aux.cmi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
index 6301aa03c..88606cd47 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -27,6 +27,7 @@ let _ = Pre_env.empty_env
 EOT
 
 ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 
 if make VERBOSE=1; then
   # make command should have failed (but didn't)
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
index 991fb4a61..939ef9c7b 100755
--- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -28,5 +28,6 @@ let _ = Pre_env.empty_env
 EOT
 
 ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 
 make VERBOSE=1
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index c2d47166f..5433d9e92 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 mv src/test_plugin.mlpack src/test_plugin.mllib
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index c2d47166f..5433d9e92 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 mv src/test_plugin.mlpack src/test_plugin.mllib
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index c2d47166f..5433d9e92 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 mv src/test_plugin.mlpack src/test_plugin.mllib
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index c952d41a3..803fe8029 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -1,3 +1,5 @@
+set -e
+set -o pipefail
 
 export PATH=$COQBIN:$PATH
 
diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
index e525e1208..5354f794f 100755
--- a/test-suite/coq-makefile/uninstall1/run.sh
+++ b/test-suite/coq-makefile/uninstall1/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
@@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp"
 make uninstall DSTROOT="$PWD/tmp"
 make uninstall-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 EOT
diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh
index e525e1208..5354f794f 100755
--- a/test-suite/coq-makefile/uninstall2/run.sh
+++ b/test-suite/coq-makefile/uninstall2/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
@@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp"
 make uninstall DSTROOT="$PWD/tmp"
 make uninstall-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 EOT
diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh
index aaa4194b3..43bf39de1 100755
--- a/test-suite/coq-makefile/validate1/run.sh
+++ b/test-suite/coq-makefile/validate1/run.sh
@@ -1,10 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 exec make validate
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 00c5eb1bd..299f49469 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -4,7 +4,7 @@
 rm -f misc/deps/lib/*.vo misc/deps/client/*.vo
 tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
 $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput
-diff -u misc/deps/deps.out $tmpoutput 2>&1
+diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1
 R=$?
 times
 $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 1abe14774..6962e43e7 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -37,7 +37,6 @@ Hint Resolve predf | 0 : predconv.
 
 Goal exists n, pred n.
   eexists.
-  Fail Timeout 1 typeclasses eauto with pred.
   Set Typeclasses Filtered Unification.
   Set Typeclasses Debug Verbosity 2.
   (* predf is not tried as it doesn't match the goal *)
@@ -80,8 +79,6 @@ Qed.
 (** The other way around: goal contains redexes instead of instances *)
 Goal exists n, pred (0 + n).
   eexists.
-  (* predf is applied indefinitely *)
-  Fail Timeout 1 typeclasses eauto with pred.
   (* pred0 (pred _) matches the goal *)
   typeclasses eauto with predconv.
 Qed.
@@ -169,8 +166,6 @@ Instance foo f :
   E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘
      id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id).
 Proof.
-  Fail Timeout 1 apply _. (* 3.7s *)
-  
 Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
                  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.