From 6b4a57051a470436b50d53e7395ec44b52e2dc7e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 30 May 2017 15:24:31 +0200
Subject: [gitlab] Artifact test suite logs on failure.

---
 .gitlab-ci.yml          | 10 +++++++---
 test-suite/save-logs.sh |  5 +++++
 2 files changed, 12 insertions(+), 3 deletions(-)
 create mode 100755 test-suite/save-logs.sh

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9ba39abdbd..3b1ea0d1f8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -100,13 +100,17 @@ before_script:
 .test-suite-template: &test-suite-template
   stage: test
   script:
-    - set -e
     - cd test-suite
     - make clean
     # careful with the ending /
     - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all
-    - cat summary.log
-    - set +e
+  after_script:
+    - test-suite/save-logs.sh
+  artifacts:
+    name: "$CI_JOB_NAME.logs"
+    when: on_failure
+    paths:
+      - logs
 
 .validate-template: &validate-template
   stage: test
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
new file mode 100755
index 0000000000..131bcf5451
--- /dev/null
+++ b/test-suite/save-logs.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+WHERE="logs"
+
+rsync -a --from0 --files-from=<(find . -name '*.log' -print0) . "$WHERE"
-- 
cgit v1.2.3


From 7c1b6714fe73c6cd8685bccef58eb6839a57fcb9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 31 May 2017 15:56:09 +0200
Subject: [travis] print failing test suite logs on failure

---
 .gitlab-ci.yml          |  4 +---
 test-suite/Makefile     |  7 +++++++
 test-suite/save-logs.sh | 18 ++++++++++++++++--
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3b1ea0d1f8..a6a27194af 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -104,13 +104,11 @@ before_script:
     - make clean
     # careful with the ending /
     - make -j ${NJOBS} BIN=$(readlink -f ../install/bin)/ LIB=$(readlink -f ../install/lib/coq)/ all
-  after_script:
-    - test-suite/save-logs.sh
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
     paths:
-      - logs
+      - test-suite/logs
 
 .validate-template: &validate-template
   stage: test
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 285460762b..cc635dd13e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -68,6 +68,7 @@ ifeq (,$(bogomips))
   $(warning cannot run complexity tests (no bogomips found))
 endif
 
+# keep these synced with test-suite/save-logs.sh
 log_success = "==========> SUCCESS <=========="
 log_segfault = "==========> FAILURE <=========="
 log_anomaly = "==========> FAILURE <=========="
@@ -164,7 +165,13 @@ summary.log:
 	$(SHOW) BUILDING SUMMARY FILE
 	$(HIDE)$(MAKE) --quiet summary > "$@"
 
+# if not on travis we can get the log files (they're just there for a
+# local build, and downloadable on GitLab)
 report: summary.log
+	$(HIDE)./save-logs.sh
+	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi
+	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi
+	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
 
 #######################################################################
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
index 131bcf5451..fb8a1c1b0a 100755
--- a/test-suite/save-logs.sh
+++ b/test-suite/save-logs.sh
@@ -1,5 +1,19 @@
 #!/usr/bin/env bash
 
-WHERE="logs"
+SAVEDIR="logs"
 
-rsync -a --from0 --files-from=<(find . -name '*.log' -print0) . "$WHERE"
+# reset for local builds
+rm -rf "$SAVEDIR"
+mkdir "$SAVEDIR"
+
+# keep this synced with test-suite/Makefile
+FAILMARK="==========> FAILURE <=========="
+
+FAILED=$(mktemp)
+find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
+
+rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
+cp summary.log "$SAVEDIR"/
+
+# cleanup
+rm "$FAILED"
-- 
cgit v1.2.3


From 38d3aa91fb67767b9bd8aec4d14de3fd275e3c2c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 31 May 2017 16:52:38 +0200
Subject: Makefile.build: test-suite all = run + report, so don't report again

---
 Makefile.build | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index 8aedd9ceca..f86dce9ab3 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -454,7 +454,6 @@ check: validate test-suite
 test-suite: world $(ALLSTDLIB).v
 	$(MAKE) $(MAKE_TSOPTS) clean
 	$(MAKE) $(MAKE_TSOPTS) all
-	$(MAKE) $(MAKE_TSOPTS) report
 
 ###########################################################################
 # Default rules for compiling ML code
-- 
cgit v1.2.3