[travis] Adding a template file and using it for all targets.

15 files changed, 108 insertions, 44 deletions

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 36c7b9e96..fbcf9be1d 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 3b897f679..111222ac7 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 2052a1e5f..9dfdb8745 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 683f9712d..7fc0dae2c 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 5e52f4411..0b3312e87 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 d39866044..30eca7a3e 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 7502139c2..7b5950c88 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 9d27be2e9..62733c945 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 7044c3859..10f2c2b4b 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 c5105a848..e6a57404f 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 1b6c6fb84..bb8188da4 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 597a6ab7b..1ea56af29 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 000000000..700105aed
--- /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 df86b3cad..415f9b38f 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 5b7fc1c05..4c4b4f1ce 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 )