Merge PR#477: [travis] Basic support for overlays.

17 files changed, 130 insertions, 36 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
new file mode 100644
index 000000000..da5b42579
--- /dev/null
+++ b/dev/ci/ci-basic-overlay.sh
@@ -0,0 +1,103 @@
+#!/usr/bin/env bash
+
+# This is the basic overlay set for repositories in the CI.
+
+# Maybe we should just use Ruby to have real objects...
+
+########################################################################
+# MathComp
+########################################################################
+: ${mathcomp_CI_BRANCH:=master}
+: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}
+
+########################################################################
+# UniMath
+########################################################################
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
+
+########################################################################
+# Unicoq + Metacoq
+########################################################################
+: ${unicoq_CI_BRANCH:=master}
+: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}
+
+: ${metacoq_CI_BRANCH:=master}
+: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}
+
+########################################################################
+# Mathclasses + Corn
+########################################################################
+: ${math_classes_CI_BRANCH:=v8.6}
+: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+
+: ${Corn_CI_BRANCH:=v8.6}
+: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+
+########################################################################
+# Iris
+########################################################################
+: ${stdpp_CI_BRANCH:=master}
+: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}
+
+: ${Iris_CI_BRANCH:=master}
+: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}
+
+########################################################################
+# HoTT
+########################################################################
+: ${HoTT_CI_BRANCH:=mz-8.7}
+: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
+
+########################################################################
+# GeoCoq
+########################################################################
+: ${GeoCoq_CI_BRANCH:=master}
+: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}
+
+########################################################################
+# Flocq
+########################################################################
+: ${Flocq_CI_BRANCH:=master}
+: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}
+
+########################################################################
+# Coquelicot
+########################################################################
+: ${Coquelicot_CI_BRANCH:=master}
+: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
+
+########################################################################
+# Coquelicot
+########################################################################
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+
+########################################################################
+# fiat_parsers
+########################################################################
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+
+########################################################################
+# fiat_crypto
+########################################################################
+: ${fiat_crypto_CI_BRANCH:=master}
+: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+
+########################################################################
+# CoLoR
+########################################################################
+: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
+
+########################################################################
+# SF
+########################################################################
+: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz}
+
+########################################################################
+# TLC
+########################################################################
+: ${tlc_CI_BRANCH:=master}
+: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index fbcf9be1d..3f0716511 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,7 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
 svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 6f624ab6e..c94f15026 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -11,9 +11,9 @@ ls `pwd`/bin
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-# Maybe we should just use Ruby...
-mathcomp_CI_BRANCH=master
-mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+source ${ci_dir}/ci-user-overlay.sh
+source ${ci_dir}/ci-basic-overlay.sh
+
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
 
 # git_checkout branch url dest will create a git repository
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 111222ac7..c78ffdc2c 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-CompCert_CI_BRANCH=master
-CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
 CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
 
 opam install -j ${NJOBS} -y menhir
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 9dfdb8745..40eff03b7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Coquelicot_CI_BRANCH=master
-Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
 Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
 
 install_ssreflect
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 7fc0dae2c..93d39aab0 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-fiat_crypto_CI_BRANCH=master
-fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git
 fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 
 git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 0b3312e87..c62aa1d85 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-fiat_parsers_CI_BRANCH=master
-fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
 fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
 
 git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 30eca7a3e..ec19bd993 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-Flocq_CI_BRANCH=master
-Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
 Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
 
 git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 7b5950c88..4e5aa2687 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-GeoCoq_CI_BRANCH=master
-GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
 GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
 
 git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 62733c945..1bf6e9a87 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-HoTT_CI_BRANCH=mz-8.7
-HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git
 HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 10f2c2b4b..eb1d1be07 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -3,12 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-stdpp_CI_BRANCH=master
-stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
 stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
 
-Iris_CI_BRANCH=master
-Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git
 Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
 
 install_ssreflect
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index e6a57404f..beb75773b 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -3,12 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-math_classes_CI_BRANCH=v8.6
-math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git
 math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-Corn_CI_BRANCH=v8.6
-Corn_CI_GITURL=https://github.com/c-corn/corn.git
 Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 # Setup Math-Classes
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 1ea56af29..e31691179 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -3,12 +3,7 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-unicoq_CI_BRANCH=master
-unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
 unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-
-metacoq_CI_BRANCH=master
-metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
 metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
 # Setup UniCoq
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index c451bf26a..7d23ccad9 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,7 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz
+# XXX: Needs fixing to properly set the build directory.
+wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 415f9b38f..ce2639937 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-tlc_CI_BRANCH=master
-tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git
 tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
 git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 4c4b4f1ce..175b82b5f 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-UniMath_CI_BRANCH=master
-UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
 UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
 
 git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
new file mode 100644
index 000000000..028574743
--- /dev/null
+++ b/dev/ci/ci-user-overlay.sh
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+# Add user overlays here. You can use some logic to detect if you are
+# in your travis branch and conditionally enable the overlay.
+
+# Some useful Travis variables:
+# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
+#
+# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
+#   the name of the branch currently being built; whereas for builds
+#   triggered by a pull request this is the name of the branch
+#   targeted by the pull request (in many cases this will be master).
+#
+# - TRAVIS_COMMIT: The commit that the current build is testing.
+#
+# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
+#   a pull request, “false” if it’s not a pull request.
+#
+# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
+#   the name of the branch from which the PR originated. "" if the
+#   current job is a push build.
+