diff options
| -rw-r--r-- | .travis.yml | 95 | ||||
| -rwxr-xr-x | etc/ci/travis.sh | 19 |
2 files changed, 89 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 diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh new file mode 100755 index 000000000..22b6fdbf5 --- /dev/null +++ b/etc/ci/travis.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +set -x + +CACHE_DIR="$HOME/.cache/vos" +PREV_ARCHIVE="${CACHE_DIR}/vos-${COQ_VERSION}-${PREV}.tar.gz" +CUR_ARCHIVE="${CACHE_DIR}/vos-${COQ_VERSION}-${CUR}.tar.gz" + +tar -xzf "${PREV_ARCHIVE}" || true +mkdir -p "${CACHE_DIR}" +shift + +make "$@" -j2 TIMED=1 2>&1 | tee -a time-of-build.log +python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "time-of-build-pretty.log" || exit $? +rm -f "${CUR_ARCHIVE}" +tar -czf "${CUR_ARCHIVE}" time-of-build.log src Bedrock coqprime + +cat time-of-build-pretty.log +make "$@" -j2 TIMED=1 || exit $? |