From 56dc3e331c6b4b2bfa5ac072db57db8250884ce3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 Mar 2017 12:33:37 +0100
Subject: Improve build of travis target on local machine.

- Move the git clones to a specific subfolder to avoid pollution.
- Do not fail when git clone already exist (but make sure it is up-to-date).
---
 dev/ci/ci-common.sh | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 412da626fd..cc34bc2957 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -12,6 +12,9 @@ ls `pwd`/bin
 mathcomp_CI_BRANCH=master
 mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
 
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
 # git_checkout branch
 git_checkout()
 {
@@ -19,9 +22,15 @@ git_checkout()
   local _URL=${2}
   local _DEST=${3}
 
-  echo "Checking out ${_DEST}"
-  git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
-  ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+  mkdir -p ${CI_BUILD_DIR}
+  cd ${CI_BUILD_DIR}
+
+  if [ ! -d ${_DEST} ] ; then
+    echo "Checking out ${_DEST}"
+    git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
+  fi
+  ( cd ${_DEST} && git pull &&
+    echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
 }
 
 checkout_mathcomp()
-- 
cgit v1.2.3


From ba36aab9ad9a3d210211e1d4527dd0f6f493ca05 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 Mar 2017 16:14:39 +0100
Subject: [travis] Change headband for wider compatibility.

---
 dev/ci/ci-color.sh        | 2 +-
 dev/ci/ci-common.sh       | 2 +-
 dev/ci/ci-compcert.sh     | 2 +-
 dev/ci/ci-coquelicot.sh   | 2 +-
 dev/ci/ci-cpdt.sh         | 2 +-
 dev/ci/ci-fiat-crypto.sh  | 2 +-
 dev/ci/ci-fiat-parsers.sh | 2 +-
 dev/ci/ci-flocq.sh        | 2 +-
 dev/ci/ci-geocoq.sh       | 2 +-
 dev/ci/ci-hott.sh         | 2 +-
 dev/ci/ci-iris-coq.sh     | 2 +-
 dev/ci/ci-math-classes.sh | 2 +-
 dev/ci/ci-math-comp.sh    | 2 +-
 dev/ci/ci-metacoq.sh      | 2 +-
 dev/ci/ci-sf.sh           | 2 +-
 dev/ci/ci-tlc.sh          | 2 +-
 dev/ci/ci-unimath.sh      | 2 +-
 17 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 78ae7f02f9..36c7b9e965 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index cc34bc2957..94fd00c0d2 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -xe
 
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index ec09389f8e..3b897f679a 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 94bd5e468f..2052a1e5ff 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 18d7561804..0e791ebbfd 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c669195ddd..683f9712d6 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 15d73078fd..5e52f44116 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 345924e40a..d398660444 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 29667b018a..7502139c2b 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 0c07564c02..9d27be2e91 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index c21af976f4..7044c3859d 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4450dc0710..c5105a8486 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 2eb150cb52..1b6c6fb847 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 91a33695b0..597a6ab7b3 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 5e41211f1a..c451bf26a1 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index b946324924..df86b3cadd 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 15e619acbb..5b7fc1c053 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
-- 
cgit v1.2.3


From 710c1e1f49ce834acb9488704bcbbf13c4ebaf91 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 7 Mar 2017 23:30:29 +0100
Subject: [travis] Adding a template file and using it for all targets.

---
 dev/ci/ci-color.sh        |  7 +++++--
 dev/ci/ci-compcert.sh     |  5 +++--
 dev/ci/ci-coquelicot.sh   | 10 ++++++----
 dev/ci/ci-fiat-crypto.sh  |  9 ++++++---
 dev/ci/ci-fiat-parsers.sh |  6 +++---
 dev/ci/ci-flocq.sh        |  9 ++++++---
 dev/ci/ci-geocoq.sh       |  6 +++---
 dev/ci/ci-hott.sh         |  8 ++++++--
 dev/ci/ci-iris-coq.sh     | 19 ++++++++++++++-----
 dev/ci/ci-math-classes.sh | 22 +++++++++++++++++-----
 dev/ci/ci-math-comp.sh    |  6 ++++--
 dev/ci/ci-metacoq.sh      | 20 ++++++++++++++------
 dev/ci/ci-template.sh     | 12 ++++++++++++
 dev/ci/ci-tlc.sh          |  8 ++++++--
 dev/ci/ci-unimath.sh      |  5 +++--
 15 files changed, 108 insertions(+), 44 deletions(-)
 create mode 100755 dev/ci/ci-template.sh

(limited to 'dev')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 36c7b9e965..fbcf9be1d6 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,6 +3,9 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color
+Color_CI_DIR=${CI_BUILD_DIR}/color
 
-( cd color && make -j ${NJOBS} )
+svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
+
+( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 3b897f679a..111222ac7f 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,9 +5,10 @@ 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
-git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
 # Patch to avoid the upper version limit
-( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 2052a1e5ff..9dfdb87451 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,12 +1,14 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 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
 
-# Setup coquelicot
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
 
-( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 683f9712d6..7fc0dae2c0 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,9 +1,12 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
+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
 
-( cd fiat-crypto && make -j ${NJOBS} )
+git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
+
+( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 5e52f44116..0b3312e878 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 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
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
 
-( cd fiat && make -j ${NJOBS} parsers )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index d398660444..30eca7a3e9 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,9 +1,12 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq
+Flocq_CI_BRANCH=master
+Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
 
-( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
+
+( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 7502139c2b..7b5950c887 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -3,13 +3,13 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# XXX: replace by generic template
 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
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
 
-( cd GeoCoq                                               && \
+( cd ${GeoCoq_CI_DIR}                                     && \
   ./configure.sh                                          && \
   sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
   sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 9d27be2e91..62733c9452 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,10 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+HoTT_CI_BRANCH=mz-8.7
+HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git
+HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
-( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
+git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
+
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 7044c3859d..10f2c2b4bd 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,17 +1,26 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 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
 
 # Setup stdpp
-git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp
 
-( cd coq-stdpp && make -j ${NJOBS} && make install )
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR}
+
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
 
 # Setup Iris
-git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
 
-( cd iris-coq && make -j ${NJOBS} )
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index c5105a8486..e6a57404fe 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,12 +1,24 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
-( cd math-classes && make -j ${NJOBS} && make install )
+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
 
-git_checkout v8.6 https://github.com/c-corn/corn.git corn
-( cd corn         && make -j ${NJOBS} )
+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
+
+git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+
+( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup Corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 1b6c6fb847..bb8188da4e 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -4,10 +4,12 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-checkout_mathcomp math-comp
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
 
 # odd_order takes too much time for travis.
-( cd math-comp/mathcomp                           && \
+( cd ${mathcomp_CI_DIR}/mathcomp                  && \
   sed -i.bak '/PFsection/d'                  Make && \
   sed -i.bak '/stripped_odd_order_theorem/d' Make && \
   make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 597a6ab7b3..1ea56af29a 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,24 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# MetaCoq + UniCoq
+unicoq_CI_BRANCH=master
+unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
 
-git_checkout master https://github.com/unicoq/unicoq.git unicoq
+metacoq_CI_BRANCH=master
+metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+# Setup UniCoq
 
-git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
 
+# Setup MetaCoq
+
+git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
+
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
new file mode 100755
index 0000000000..700105aed4
--- /dev/null
+++ b/dev/ci/ci-template.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Template_CI_BRANCH=master
+Template_CI_GITURL=https://github.com/Template/Template
+Template_CI_DIR=${CI_BUILD_DIR}/Template
+
+git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
+
+( cd ${Template_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index df86b3cadd..415f9b38f9 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -3,6 +3,10 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+tlc_CI_BRANCH=master
+tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git
+tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
-( cd tlc && make -j ${NJOBS} )
+git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
+
+( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 5b7fc1c053..4c4b4f1ce1 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -5,10 +5,11 @@ 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
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
 
-( cd UniMath                                  && \
+( cd ${UniMath_CI_DIR}                        && \
   sed -i.bak '/Folds/d'              Makefile && \
   sed -i.bak '/HomologicalAlgebra/d' Makefile && \
   make -j ${NJOBS} BUILD_COQ=no )
-- 
cgit v1.2.3


From fd5c5da475baea11d7ee2e1c2e965d7faeed3f33 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 8 Mar 2017 09:56:01 +0100
Subject: [travis] Make the git_checkout function more reliable.

This commit also documents the behavior of said function;
and fix the location of the ssreflect clone to an absolute
path (this is now necessary).
---
 dev/ci/ci-common.sh | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 94fd00c0d2..6f624ab6ec 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,28 +8,29 @@ export PATH=`pwd`/bin:$PATH
 
 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
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
 
-# Where we clone and build external developments
-CI_BUILD_DIR=`pwd`/_build_ci
-
-# git_checkout branch
+# git_checkout branch url dest will create a git repository
+# in <dest> (if it does not exist already) and checkout the
+# remote branch <branch> from <url>
 git_checkout()
 {
   local _BRANCH=${1}
   local _URL=${2}
   local _DEST=${3}
 
-  mkdir -p ${CI_BUILD_DIR}
-  cd ${CI_BUILD_DIR}
-
-  if [ ! -d ${_DEST} ] ; then
-    echo "Checking out ${_DEST}"
-    git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
-  fi
-  ( cd ${_DEST} && git pull &&
+  mkdir -p ${_DEST}
+  ( cd ${_DEST}                                                && \
+    if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \
+    echo "Checking out ${_DEST}"                               && \
+    git fetch ${_URL} ${_BRANCH}                               && \
+    git checkout FETCH_HEAD                                    && \
     echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
 }
 
@@ -43,8 +44,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp math-comp
-  ( cd math-comp/mathcomp            && \
+  checkout_mathcomp ${mathcomp_CI_DIR}
+  ( cd ${mathcomp_CI_DIR}/mathcomp   && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \
     sed -i.bak '/all\/all.v/d'  Make && \
-- 
cgit v1.2.3