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.

10 files changed, 87 insertions, 77 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 7c250c667..c49bc3b08 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -166,7 +166,7 @@ opam-switch: &opam-switch
         name: Test
         command: |
           source ~/.profile
-          make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB}
+          dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
     - persist_to_workspace:
         root: *workspace
         paths:
@@ -255,85 +255,85 @@ jobs:
       COMPILER: *compiler-be
       EXTRA_PACKAGES: *timing-packages
 
-  ci-bignums:
+  bignums:
     <<: *ci-template
 
-  ci-color:
+  color:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: *timing-packages
 
-  ci-compcert:
+  compcert:
     <<: *ci-template
 
-  ci-coq-dpdgraph:
+  coq-dpdgraph:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
-  ci-coquelicot:
+  coquelicot:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
-  ci-equations:
+  equations:
     <<: *ci-template
 
-  ci-geocoq:
+  geocoq:
     <<: *ci-template
 
-  ci-fiat-crypto:
+  fiat-crypto:
     <<: *ci-template
 
-  ci-fiat-parsers:
+  fiat-parsers:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: *timing-packages
 
-  ci-flocq:
+  flocq:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
-  ci-math-classes:
+  math-classes:
     <<: *ci-template
 
-  ci-corn:
+  corn:
     <<: *ci-template
 
-  ci-formal-topology:
+  formal-topology:
     <<: *ci-template
 
-  ci-hott:
+  hott:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
-  ci-iris-lambda-rust:
+  iris-lambda-rust:
     <<: *ci-template
 
-  ci-ltac2:
+  ltac2:
     <<: *ci-template
 
-  ci-math-comp:
+  math-comp:
     <<: *ci-template
 
-  ci-sf:
+  sf:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python wget"
 
-  ci-unimath:
+  unimath:
     <<: *ci-template
 
-  ci-vst:
+  vst:
     <<: *ci-template
 
 workflows:
@@ -354,38 +354,38 @@ workflows:
       - test-suite: *req-main
       - documentation: *req-main
 
-      - ci-bignums: *req-main
-      - ci-color:
+      - bignums: *req-main
+      - color:
           requires:
             - build
-            - ci-bignums
-      - ci-compcert: *req-main
-      - ci-coq-dpdgraph: *req-main
-      - ci-coquelicot: *req-main
-      - ci-equations: *req-main
-      - ci-geocoq: *req-main
-      - ci-fiat-crypto: *req-main
-      - ci-fiat-parsers: *req-main
-      - ci-flocq: *req-main
-      - ci-math-classes:
+            - bignums
+      - compcert: *req-main
+      - coq-dpdgraph: *req-main
+      - coquelicot: *req-main
+      - equations: *req-main
+      - geocoq: *req-main
+      - fiat-crypto: *req-main
+      - fiat-parsers: *req-main
+      - flocq: *req-main
+      - math-classes:
           requires:
             - build
-            - ci-bignums
-      - ci-corn:
+            - bignums
+      - corn:
           requires:
             - build
-            - ci-math-classes
-      - ci-formal-topology:
+            - math-classes
+      - formal-topology:
           requires:
             - build
-            - ci-corn
-      - ci-hott: *req-main
-      - ci-iris-lambda-rust: *req-main
-      - ci-ltac2: *req-main
-      - ci-math-comp: *req-main
-      - ci-sf: *req-main
-      - ci-unimath: *req-main
-      - ci-vst: *req-main
+            - corn
+      - hott: *req-main
+      - iris-lambda-rust: *req-main
+      - ltac2: *req-main
+      - math-comp: *req-main
+      - sf: *req-main
+      - unimath: *req-main
+      - vst: *req-main
 
       - build-32bit:
           requires:
diff --git a/.travis.yml b/.travis.yml
index 54e7754f2..0bc43c110 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -46,29 +46,29 @@ env:
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}"
-  - TEST_TARGET="ci-bignums TIMED=1"
-  - TEST_TARGET="ci-color TIMED=1"
-  - TEST_TARGET="ci-compcert TIMED=1"
+  - TEST_TARGET="ci-bignums"
+  - TEST_TARGET="ci-color"
+  - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
-  - TEST_TARGET="ci-coquelicot TIMED=1"
-  - TEST_TARGET="ci-equations TIMED=1"
-  - TEST_TARGET="ci-geocoq TIMED=1"
-  - TEST_TARGET="ci-fiat-crypto TIMED=1"
-  - TEST_TARGET="ci-fiat-parsers TIMED=1"
-  - TEST_TARGET="ci-flocq TIMED=1"
-  - TEST_TARGET="ci-formal-topology TIMED=1"
-  - TEST_TARGET="ci-hott TIMED=1"
-  - TEST_TARGET="ci-iris-lambda-rust TIMED=1"
-  - TEST_TARGET="ci-ltac2 TIMED=1"
-  - TEST_TARGET="ci-math-classes TIMED=1"
-  - TEST_TARGET="ci-math-comp TIMED=1"
-  - TEST_TARGET="ci-sf TIMED=1"
-  - TEST_TARGET="ci-unimath TIMED=1"
-  - TEST_TARGET="ci-vst TIMED=1"
+  - TEST_TARGET="ci-coquelicot"
+  - TEST_TARGET="ci-equations"
+  - TEST_TARGET="ci-geocoq"
+  - TEST_TARGET="ci-fiat-crypto"
+  - TEST_TARGET="ci-fiat-parsers"
+  - TEST_TARGET="ci-flocq"
+  - TEST_TARGET="ci-formal-topology"
+  - TEST_TARGET="ci-hott"
+  - TEST_TARGET="ci-iris-lambda-rust"
+  - TEST_TARGET="ci-ltac2"
+  - TEST_TARGET="ci-math-classes"
+  - TEST_TARGET="ci-math-comp"
+  - TEST_TARGET="ci-sf"
+  - TEST_TARGET="ci-unimath"
+  - TEST_TARGET="ci-vst"
   # Not ready yet for 8.7
-  # - TEST_TARGET="ci-cpdt TIMED=1"
-  # - TEST_TARGET="ci-metacoq TIMED=1"
-  # - TEST_TARGET="ci-tlc TIMED=1"
+  # - TEST_TARGET="ci-cpdt"
+  # - TEST_TARGET="ci-metacoq"
+  # - TEST_TARGET="ci-tlc"
 
 matrix:
 
diff --git a/Makefile.ci b/Makefile.ci
index 2a6222e22..334827a93 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -25,9 +25,6 @@ CI_TARGETS=ci-all \
 
 .PHONY: $(CI_TARGETS)
 
-_build_ci/.ci-%.done:
-	+./dev/ci/ci-wrapper.sh $*
-
 ci-color: ci-bignums
 
 ci-math-classes: ci-bignums
@@ -37,7 +34,8 @@ ci-corn: ci-math-classes
 ci-formal-topology: ci-corn
 
 # Generic rule, we use make to ease travis integration with mixed rules
-$(CI_TARGETS): ci-%: _build_ci/.ci-%.done
+$(CI_TARGETS): ci-%:
+	+./dev/ci/ci-wrapper.sh $*
 
 # For emacs:
 # Local Variables:
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"