From 23d1504de4111223dc4805c6f4176a4d9e028b79 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 15 Aug 2017 12:00:18 -0400
Subject: Better error messages on the CI

This makes it so that when a ci target fails, we don't get red herring
error messages about .ok files not existing.

Since this requires bash, we make a helper script that invokes bash, so
as to not depend on bash in general.
---
 dev/ci/ci-pipe-tee.sh | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100755 dev/ci/ci-pipe-tee.sh

(limited to 'dev')

diff --git a/dev/ci/ci-pipe-tee.sh b/dev/ci/ci-pipe-tee.sh
new file mode 100755
index 0000000000..7b1ccddf23
--- /dev/null
+++ b/dev/ci/ci-pipe-tee.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+# Use this script to preserve the exit code of $1 when piping it to
+# `tee $2`.  We have a separate script, because this only works in
+# bash, which we don't require project-wide.
+
+"$1" 2>&1 | tee "$2"
+exit ${PIPESTATUS[0]}
-- 
cgit v1.2.3


From 26b0fc20bba2d9d79e176620141697beb3f307a2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 15 Aug 2017 14:15:40 -0400
Subject: Move the rest of the ci target to a bash file

---
 dev/ci/ci-pipe-tee.sh |  8 --------
 dev/ci/ci-wrapper.sh  | 17 +++++++++++++++++
 2 files changed, 17 insertions(+), 8 deletions(-)
 delete mode 100755 dev/ci/ci-pipe-tee.sh
 create mode 100755 dev/ci/ci-wrapper.sh

(limited to 'dev')

diff --git a/dev/ci/ci-pipe-tee.sh b/dev/ci/ci-pipe-tee.sh
deleted file mode 100755
index 7b1ccddf23..0000000000
--- a/dev/ci/ci-pipe-tee.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-# Use this script to preserve the exit code of $1 when piping it to
-# `tee $2`.  We have a separate script, because this only works in
-# bash, which we don't require project-wide.
-
-"$1" 2>&1 | tee "$2"
-exit ${PIPESTATUS[0]}
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
new file mode 100755
index 0000000000..63bff6778f
--- /dev/null
+++ b/dev/ci/ci-wrapper.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+# Use this script to preserve the exit code of $CI_SCRIPT when piping
+# it to `tee time-of-build.log`.  We have a separate script, because
+# this only works in bash, which we don't require project-wide.
+
+set -eo pipefail
+
+CI_SCRIPT="$1"
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+# assume this script is in dev/ci/, cd to the root Coq directory
+cd "${DIR}/../.."
+
+"${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
+echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r'
+python ./tools/make-one-time-file.py time-of-build.log
+echo -en 'travis_fold:end:coq.test.timing\\r'
-- 
cgit v1.2.3


From ed29da3f95056dd92b4d1059371afd7ebf05bd2c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 24 Aug 2017 12:45:37 -0400
Subject: Only display travis_fold: on travis

---
 dev/ci/ci-wrapper.sh | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 63bff6778f..789dbed07c 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,12 +6,19 @@
 
 set -eo pipefail
 
+function travis_fold {
+    if [ -n "${TRAVIS}" ];
+    then
+	echo -n "travis_fold:$1:$2\\r"
+    fi
+}
+
 CI_SCRIPT="$1"
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 # assume this script is in dev/ci/, cd to the root Coq directory
 cd "${DIR}/../.."
 
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r'
+echo 'Aggregating timing log...' && travis_fold 'start' 'coq.test.timing'
 python ./tools/make-one-time-file.py time-of-build.log
-echo -en 'travis_fold:end:coq.test.timing\\r'
+travis_fold 'end' 'coq.test.timing'
-- 
cgit v1.2.3


From 85fdc6f58099d7bd605eb1f10d2a250a87e43771 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 24 Aug 2017 15:46:22 -0400
Subject: Swap order of "aggregating..." message and travis_fold

Now the folded line starts with "Aggregating..." and not with
"---------"
---
 dev/ci/ci-wrapper.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 789dbed07c..7f22d0e48d 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -19,6 +19,6 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 cd "${DIR}/../.."
 
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-echo 'Aggregating timing log...' && travis_fold 'start' 'coq.test.timing'
+travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
 travis_fold 'end' 'coq.test.timing'
-- 
cgit v1.2.3


From 7ac81ccfad04b1f0d3bad8f3b596e579b5f37224 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 24 Aug 2017 15:50:51 -0400
Subject: Don't strip the newline, don't use \r

Not sure entirely what it was supposed to do, but stripping the newline
erased the following line
---
 dev/ci/ci-wrapper.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 7f22d0e48d..96acc5a11c 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -9,7 +9,7 @@ set -eo pipefail
 function travis_fold {
     if [ -n "${TRAVIS}" ];
     then
-	echo -n "travis_fold:$1:$2\\r"
+	echo "travis_fold:$1:$2"
     fi
 }
 
-- 
cgit v1.2.3