Attempt to build travis in stages

Hopefully this will lead to overall faster builds

Also:
- try to allow failures
- Version-specific vo caches
- Make archives stage-specific

This way, if multiple branches are running stages at the same time, they
don't have as much a chance of clobbering each others builds.

1 files changed, 70 insertions, 25 deletions

diff --git a/.travis.yml b/.travis.yml
index 6cabe6413..746f8335e 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -7,6 +7,10 @@ dist: trusty
 compiler:
   - gcc
 
+cache:
+  directories:
+    - $HOME/.cache/vos
+
 addons:
   apt:
     sources:
@@ -15,30 +19,6 @@ addons:
       - g++-7
       - libssl-dev
 
-matrix:
-  fast_finish: true
-  include:
-    - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific"               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="master" TARGETS="curves-proofs"                               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="no-curves-proofs-non-specific"               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="curves-proofs"                               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: COQ_VERSION="8.7.1"  TARGETS="no-curves-proofs-non-specific"               COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-    - env: COQ_VERSION="8.7.1"  TARGETS="curves-proofs"                               COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-    - env: COQ_VERSION="8.7.1"  TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-    - env: TARGETS="build-selected-test build-selected-bench" COQ_VERSION="8.7.1"     COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-    - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.1"                 COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-    - env: TARGETS="printlite lite" COQ_VERSION="8.7.1"                               COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-  allow_failures:
-    - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific"               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="master" TARGETS="curves-proofs"                               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="no-curves-proofs-non-specific"               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="curves-proofs"                               COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: COQ_VERSION="v8.7"   TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
-    - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.1"                 COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
-
 before_install:
   - if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
   - travis_retry sudo apt-get update -q
@@ -53,7 +33,72 @@ before_script:
   - sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60 --slave /usr/bin/g++ g++ /usr/bin/g++-7
   - ./etc/ci/remove_autogenerated.sh
 
-script: ./etc/coq-scripts/timing/make-pretty-timed.sh -j2 $TARGETS && make $TARGETS TIMED=1 -j2
+matrix:
+  fast_finish: true
+
+stages:
+  - printlite lite
+  - no-curves-proofs-non-specific
+  - curves-proofs
+  - selected-specific selected-specific-display
+  - selected-test selected-bench
+
+jobs:
+  include:
+    - stage: printlite lite
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      allow_failure: true
+      script: CUR=0 ./etc/ci/travis.sh printlite lite
+    - stage: printlite lite
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      allow_failure: true
+      script: CUR=0 ./etc/ci/travis.sh printlite lite
+    - stage: printlite lite
+      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+      script: CUR=0 ./etc/ci/travis.sh printlite lite
+
+    - stage: no-curves-proofs-non-specific
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+    - stage: no-curves-proofs-non-specific
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+    - stage: no-curves-proofs-non-specific
+      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=0 CUR=1 ./etc/ci/travis.sh no-curves-proofs-non-specific
+
+    - stage: curves-proofs
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      allow_failure: true
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+    - stage: curves-proofs
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      allow_failure: true
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+    - stage: curves-proofs
+      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=1 CUR=2 ./etc/ci/travis.sh curves-proofs
+
+    - stage: selected-specific selected-specific-display
+      env: COQ_VERSION="master" COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-master-daily"
+      allow_failure: true
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+    - stage: selected-specific selected-specific-display
+      env: COQ_VERSION="v8.7"   COQ_PACKAGE="coq"       PPA="ppa:jgross-h/coq-8.7-daily"
+      allow_failure: true
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+    - stage: selected-specific selected-specific-display
+      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=2 CUR=3 ./etc/ci/travis.sh selected-specific selected-specific-display
+
+    - stage: build-selected-test build-selected-bench
+      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+      script: PREV=3 CUR=4 ./etc/ci/travis.sh build-selected-test build-selected-bench
+
+#    - stage: selected-test selected-bench
+#      env: COQ_VERSION="8.7.1"  COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+#      allow_failure: true
+#      script: PREV=4 CUR=5 ./etc/ci/travis.sh selected-test selected-bench
 
 after_success:
   - kill $PID_KEEP_ALIVE