From 7f17e151c0a2666263d3854c064acdfea29edf53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 May 2017 17:19:22 +0200
Subject: Adding tests for testing exit status and #use"include".

---
 test-suite/Makefile | 30 +++++++++++++++++++++++++++++-
 1 file changed, 29 insertions(+), 1 deletion(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index c10cd4ed44..779f5455ae 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,6 +33,7 @@ LIB := $(shell cd ..; pwd)
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
 bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqtopbyte := $(BIN)coqtop.byte
 
 command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
 coqc := $(coqtop) -compile
@@ -405,7 +406,7 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log
+misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log
 
 # Check that both coqdep and coqtop/coqc supports -R
 # Check that both coqdep and coqtop/coqc takes the later -R
@@ -477,6 +478,33 @@ misc/universes.log: misc/universes/all_stdlib.v
 misc/universes/all_stdlib.v:
 	cd .. && $(MAKE) test-suite/$@
 
+misc/printers.log:
+	@echo "TEST      printers"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/printers...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/printers...Error!"; \
+	  fi; \
+	} > "$@"
+
+misc/exitstatus.log:
+	@echo "TEST      exitstatus"
+	$(HIDE){ \
+	  echo $(call log_intro,$<); \
+	  $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \
+	  if [ $$R != 0 ]; then \
+	    echo $(log_success); \
+	    echo "    misc/exitstatus...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    misc/exitstatus...Error!"; \
+	  fi; \
+	} > "$@"
 
 # IDE : some tests of backtracking for coqtop -ideslave
 
-- 
cgit v1.2.3


From 63510329fae28f7a9d18935f24e3ebf0485dabc8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 May 2017 18:28:55 +0200
Subject: A more regular naming of variables in test-suite Makefile.

---
 test-suite/Makefile | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 779f5455ae..5d3c118445 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -31,12 +31,12 @@ BIN := ../bin/
 LIB := $(shell cd ..; pwd)
 
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
-bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
-bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 coqtopbyte := $(BIN)coqtop.byte
 
-command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
-coqc := $(coqtop) -compile
+coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
+coqtopcompile := $(coqtop) -compile
 coqdep := $(BIN)coqdep -coqlib $(LIB)
 
 SHOW := $(if $(VERBOSE),@true,@echo)
@@ -53,7 +53,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
 has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
 has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
-get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
+get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload))
 
 
 bogomips:=
@@ -220,7 +220,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...could not be prepared" ; \
@@ -250,7 +250,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
+	  $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
 	    $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
@@ -421,8 +421,8 @@ misc/deps-order.log:
 	  $(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; R=$$?; times; \
-	  $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
-	  $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
+	  $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
+	  $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
 	  $(coqtop) -R misc/deps/lib 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 \
@@ -441,9 +441,9 @@ misc/deps-checksum.log:
 	$(HIDE){ \
 	  echo $(call log_intro,deps-checksum); \
 	  rm -f misc/deps/*/*.vo; \
-	  $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \
-	  $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \
-	  $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \
+	  $(coqc) -R misc/deps/A A misc/deps/A/A.v; \
+	  $(coqc) -R misc/deps/B A misc/deps/B/A.v; \
+	  $(coqc) -R misc/deps/B A misc/deps/B/B.v; \
 	  $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
@@ -461,8 +461,8 @@ universes: misc/universes.log
 misc/universes.log: misc/universes/all_stdlib.v
 	@echo "TEST      misc/universes"
 	$(HIDE){ \
-	  $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
-	  $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \
+	  $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
+	  $(coqc) -R misc/universes Universes misc/universes/universes 2>&1; \
 	  mv universes.txt misc/universes; \
 	  N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \
 	  times; \
@@ -529,9 +529,9 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 %.vio.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(bincoqc) -quick -R vio vio $* 2>&1 && \
+	  $(coqc) -quick -R vio vio $* 2>&1 && \
 	  $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
-	  $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
+	  $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
@@ -546,8 +546,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 %.chk.log:%.v
 	@echo "TEST      $<"
 	$(HIDE){ \
-	  $(bincoqc) -R coqchk coqchk $* 2>&1 && \
-	  $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \
+	  $(coqc) -R coqchk coqchk $* 2>&1 && \
+	  $(coqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
-- 
cgit v1.2.3


From 98a927aefb6df05a957d94cf2fd22d88e9e6c6b6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 May 2017 21:48:43 +0200
Subject: Moving code for miscellaneous tests to specific files.

The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.

This avoids making the main Makefile more or more complex.

We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.

Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
---
 test-suite/Makefile | 102 ++++++----------------------------------------------
 1 file changed, 11 insertions(+), 91 deletions(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5d3c118445..39ef05269f 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -406,103 +406,23 @@ modules/%.vo: modules/%.v
 # Miscellaneous tests
 #######################################################################
 
-misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log misc/printers.log misc/exitstatus.log
-
-# Check that both coqdep and coqtop/coqc supports -R
-# Check that both coqdep and coqtop/coqc takes the later -R
-# 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) -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; R=$$?; times; \
-	  $(coqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \
-	  $(coqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \
-	  $(coqtop) -R misc/deps/lib 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; \
-	} > "$@"
-
-deps-checksum: misc/deps-checksum.log
-misc/deps-checksum.log:
-	@echo "TEST      misc/deps-checksum"
-	$(HIDE){ \
-	  echo $(call log_intro,deps-checksum); \
-	  rm -f misc/deps/*/*.vo; \
-	  $(coqc) -R misc/deps/A A misc/deps/A/A.v; \
-	  $(coqc) -R misc/deps/B A misc/deps/B/A.v; \
-	  $(coqc) -R misc/deps/B A misc/deps/B/B.v; \
-	  $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \
-	  if [ $$? = 0 ]; then \
-	    echo $(log_success); \
-	    echo "    misc/deps-checksum...Ok"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/deps-checksum...Error!"; \
-	  fi; \
-	} > "$@"
-
+misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
 
-# Sort universes for the whole standard library
-EXPECTED_UNIVERSES := 4 # Prop is not counted
-universes: misc/universes.log
-misc/universes.log: misc/universes/all_stdlib.v
-	@echo "TEST      misc/universes"
-	$(HIDE){ \
-	  $(coqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \
-	  $(coqc) -R misc/universes 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; \
-	} > "$@"
-
-misc/universes/all_stdlib.v:
-	cd .. && $(MAKE) test-suite/$@
-
-misc/printers.log:
-	@echo "TEST      printers"
-	$(HIDE){ \
-	  echo $(call log_intro,$<); \
-	  printf "Drop. #use\"include\";; #quit;;" | $(coqtopbyte) 2>&1 | grep Unbound; R=$$?; times; \
-	  if [ $$R != 0 ]; then \
-	    echo $(log_success); \
-	    echo "    misc/printers...Ok"; \
-	  else \
-	    echo $(log_failure); \
-	    echo "    misc/printers...Error!"; \
-	  fi; \
-	} > "$@"
-
-misc/exitstatus.log:
-	@echo "TEST      exitstatus"
+$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
+	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) misc/exitstatus/illtyped.v 2>&1; R=$$?; times; \
-	  if [ $$R != 0 ]; then \
+	  export coqc="$(coqc)"; \
+	  export coqtop="$(coqtop)"; \
+	  export coqdep="$(coqdep)"; \
+	  export coqtopbyte="$(coqtopbyte)"; \
+	  "$<" 2>&1; R=$$?; times; \
+	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
-	    echo "    misc/exitstatus...Ok"; \
+	    echo "    $<...Ok"; \
 	  else \
 	    echo $(log_failure); \
-	    echo "    misc/exitstatus...Error!"; \
+	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
 
-- 
cgit v1.2.3