Fix CI with parallel make (messed up dependencies)

When invoking through Makefile we always rebuild dependencies. To skip
dependencies, invoke ci-wrapper directly. We make Circle CI do this.

In order to properly support invoking ci-wrapper directly we replace
"make" in ci-common by a bash function which adds -j to the make
invocation outside submakes. We also set TIMED in the ci-wrapper.

7 files changed, 19 insertions, 7 deletions

diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index d68674381..c90e516ae 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -13,4 +13,4 @@ bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
 
 git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
 
-( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install)
+( cd ${bignums_CI_DIR} && make && make install)
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 1bfdf7dfb..23131c94c 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -53,6 +53,18 @@ checkout_mathcomp()
   git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
 }
 
+make()
+{
+    # +x: add x only if defined
+    if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ];
+    then
+        # Not submake and parallel make requested
+        command make -j "$NJOBS" "$@"
+    else
+        command make "$@"
+    fi
+}
+
 # this installs just the ssreflect library of math-comp
 install_ssreflect()
 {
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index b610f7000..5d6bd6a36 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
 
 git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
 
-( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite )
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make && make test-suite )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index f7470463d..62854afac 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -7,4 +7,4 @@ Equations_CI_DIR=${CI_BUILD_DIR}/Equations
 
 git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR}
 
-( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install)
+( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install)
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 1bf6e9a87..693135a4c 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
 
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index ed4003601..820ff89ee 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -7,4 +7,4 @@ ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2
 
 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
 
-( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install )
+( cd ${ltac2_CI_DIR} && make && make tests && make install )
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index a21bf9f38..12a70176c 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -15,13 +15,13 @@ function travis_fold {
 
 CI_NAME="$1"
 CI_SCRIPT="ci-${CI_NAME}.sh"
+
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 # assume this script is in dev/ci/, cd to the root Coq directory
 cd "${DIR}/../.."
 
+export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
 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'
-
-touch "_build_ci/.ci-${CI_NAME}.done"