From e9156da20ec5332b1b53a6c44127e0f822891d16 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 Jan 2017 17:18:39 +0100
Subject: test suite for coq_makefile

---
 test-suite/Makefile | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'test-suite/Makefile')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index afaa48463..8a3d383cb 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -87,7 +87,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -151,6 +151,7 @@ summary:
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
+	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -481,3 +482,19 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
+
+coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
+
+coq-makefile/%.log : coq-makefile/%/run.sh
+	@echo "TEST      $*"
+	$(HIDE)(\
+	  cd coq-makefile/$* && \
+	  ./run.sh 2>&1; \
+       	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	  fi; \
+	) > "$@"
-- 
cgit v1.2.3