Merge PR #8348: Download tarball instead of cloning external projects.

40 files changed, 211 insertions, 282 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 521dfe2a3f..60108cda4f 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1387,12 +1387,12 @@ function make_coq_installer {
 # Provides BigN, BigZ, BigQ that used to be part of Coq standard library
 
 function make_addon_bignums {
-  bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_BRANCH" | cut -f 1)
+  bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1)
   if [[ "$bignums_SHA" == "" ]]; then
-      # $bignums_CI_BRANCH must have been a tag and not a branch
-      bignums_SHA="$bignums_CI_BRANCH"
+      # $bignums_CI_REF must have been a tag / commit and not a branch
+      bignums_SHA="$bignums_CI_REF"
   fi
-  if build_prep "${bignums_CI_GITURL}/archive" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then
+  if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then
     # To make command lines shorter :-(
     echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
     log1 make all
@@ -1405,12 +1405,12 @@ function make_addon_bignums {
 # A new (experimental) tactic language
 
 function make_addon_ltac2 {
-  ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_BRANCH" | cut -f 1)
+  ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1)
   if [[ "$ltac2_SHA" == "" ]]; then
-      # $ltac2_CI_BRANCH must have been a tag and not a branch
-      ltac2_SHA="$ltac2_CI_BRANCH"
+      # $ltac2_CI_REF must have been a tag / commit and not a branch
+      ltac2_SHA="$ltac2_CI_REF"
   fi
-  if build_prep "${ltac2_CI_GITURL}/archive" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then
+  if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then
     log1 make all
     log2 make install
     build_post
@@ -1421,12 +1421,12 @@ function make_addon_ltac2 {
 # A function definition plugin
 
 function make_addon_equations {
-  Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_BRANCH" | cut -f 1)
+  Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1)
   if [[ "$Equations_SHA" == "" ]]; then
-      # $Equations_CI_BRANCH must have been a tag and not a branch
-      Equations_SHA="$Equations_CI_BRANCH"
+      # $Equations_CI_REF must have been a tag / commit and not a branch
+      Equations_SHA="$Equations_CI_REF"
   fi
-  if build_prep "${Equations_CI_GITURL}/archive" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then
+  if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then
     # Note: PATH is autmatically saved/restored by build_prep / build_post
     PATH=$COQBIN:$PATH
     logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a77eb15e92..63d5541f48 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -9,124 +9,147 @@
 ########################################################################
 # MathComp
 ########################################################################
-: "${mathcomp_CI_BRANCH:=master}"
+: "${mathcomp_CI_REF:=master}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}"
-: "${oddorder_CI_BRANCH:=master}"
+: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}"
+
+: "${oddorder_CI_REF:=master}"
 : "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}"
+: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}"
 
 ########################################################################
 # UniMath
 ########################################################################
-: "${UniMath_CI_BRANCH:=master}"
+: "${UniMath_CI_REF:=master}"
 : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}"
+: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}"
 
 ########################################################################
 # Unicoq + Mtac2
 ########################################################################
-: "${unicoq_CI_BRANCH:=master}"
+: "${unicoq_CI_REF:=master}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
+: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_REF:=master-sync}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
+: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
 
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: "${math_classes_CI_BRANCH:=master}"
-: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes}"
+: "${math_classes_CI_REF:=master}"
+: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}"
+: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}"
 
-: "${Corn_CI_BRANCH:=master}"
-: "${Corn_CI_GITURL:=https://github.com/c-corn/corn}"
+: "${Corn_CI_REF:=master}"
+: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}"
+: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}"
 
 ########################################################################
 # Iris
 ########################################################################
-: "${stdpp_CI_BRANCH:=master}"
+: "${stdpp_CI_REF:=master}"
 : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}"
+: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_BRANCH:=master}"
+: "${Iris_CI_REF:=master}"
 : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}"
+: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
 
-: "${lambdaRust_CI_BRANCH:=master}"
+: "${lambdaRust_CI_REF:=master}"
 : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}"
+: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
 ########################################################################
-: "${HoTT_CI_BRANCH:=master}"
+: "${HoTT_CI_REF:=master}"
 : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}"
+: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}"
 
 ########################################################################
 # Ltac2
 ########################################################################
-: "${ltac2_CI_BRANCH:=master}"
+: "${ltac2_CI_REF:=master}"
 : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
+: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
 
 ########################################################################
 # GeoCoq
 ########################################################################
-: "${GeoCoq_CI_BRANCH:=master}"
+: "${GeoCoq_CI_REF:=master}"
 : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
+: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}"
 
 ########################################################################
 # Flocq
 ########################################################################
-: "${Flocq_CI_BRANCH:=master}"
+: "${Flocq_CI_REF:=master}"
 : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
+: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
 # Coquelicot
 ########################################################################
-: "${Coquelicot_CI_BRANCH:=master}"
+: "${Coquelicot_CI_REF:=master}"
 : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
 
 ########################################################################
 # CompCert
 ########################################################################
-: "${CompCert_CI_BRANCH:=master}"
+: "${CompCert_CI_REF:=master}"
 : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}"
+: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}"
 
 ########################################################################
 # VST
 ########################################################################
-: "${VST_CI_BRANCH:=master}"
+: "${VST_CI_REF:=master}"
 : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}"
+: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}"
 
 ########################################################################
 # cross-crypto
 ########################################################################
-: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_REF:=master}"
 : "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}"
+: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}"
 
 ########################################################################
 # fiat_parsers
 ########################################################################
-: "${fiat_parsers_CI_BRANCH:=master}"
+: "${fiat_parsers_CI_REF:=master}"
 : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}"
+: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}"
 
 ########################################################################
 # fiat_crypto
 ########################################################################
-: "${fiat_crypto_CI_BRANCH:=master}"
+: "${fiat_crypto_CI_REF:=master}"
 : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
+: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
 
 ########################################################################
 # formal-topology
 ########################################################################
-: "${formal_topology_CI_BRANCH:=ci}"
+: "${formal_topology_CI_REF:=ci}"
 : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}"
+: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}"
 
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: "${coq_dpdgraph_CI_BRANCH:=coq-master}"
+: "${coq_dpdgraph_CI_REF:=coq-master}"
 : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}"
+: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}"
 
 ########################################################################
 # CoLoR
 ########################################################################
-: "${CoLoR_CI_BRANCH:=master}"
+: "${CoLoR_CI_REF:=master}"
 : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}"
+: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}"
 
 ########################################################################
 # SF
@@ -138,59 +161,68 @@
 ########################################################################
 # TLC
 ########################################################################
-: "${tlc_CI_BRANCH:=master}"
+: "${tlc_CI_REF:=master}"
 : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}"
 
 ########################################################################
 # Bignums
 ########################################################################
-: "${bignums_CI_BRANCH:=master}"
+: "${bignums_CI_REF:=master}"
 : "${bignums_CI_GITURL:=https://github.com/coq/bignums}"
+: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}"
 
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_BRANCH:=master}"
+: "${bedrock2_CI_REF:=master}"
 : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
+: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
 
 ########################################################################
 # Equations
 ########################################################################
-: "${Equations_CI_BRANCH:=master}"
+: "${Equations_CI_REF:=master}"
 : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}"
+: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}"
 
 ########################################################################
 # Elpi
 ########################################################################
-: "${Elpi_CI_BRANCH:=coq-master}"
+: "${Elpi_CI_REF:=coq-master}"
 : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
+: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}"
 
 ########################################################################
 # fcsl-pcm
 ########################################################################
-: "${fcsl_pcm_CI_BRANCH:=master}"
+: "${fcsl_pcm_CI_REF:=master}"
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}"
+: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}"
 
 ########################################################################
 # pidetop
 ########################################################################
-: "${pidetop_CI_BRANCH:=v8.9}"
+: "${pidetop_CI_REF:=v8.9}"
 : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}"
+: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}"
 
 ########################################################################
 # ext-lib
 ########################################################################
-: "${ext_lib_CI_BRANCH:=master}"
+: "${ext_lib_CI_REF:=master}"
 : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}"
+: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}"
 
 ########################################################################
 # simple-io
 ########################################################################
-: "${simple_io_CI_BRANCH:=master}"
+: "${simple_io_CI_REF:=master}"
 : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}"
+: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}"
 
 ########################################################################
 # quickchick
 ########################################################################
-: "${quickchick_CI_BRANCH:=master}"
+: "${quickchick_CI_REF:=master}"
 : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
+: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 447076e092..5205946261 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -3,9 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2"
+FORCE_GIT=1
+git_download bedrock2
 
-git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}"
-( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive )
-
-( cd "${bedrock2_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make )
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index 0082919679..756f54dfbd 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -1,16 +1,8 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
 
-# This script could be included inside other ones
-# Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}" ];
-then
-    . "${ci_dir}/ci-common.sh"
-fi
+git_download bignums
 
-bignums_CI_DIR="${CI_BUILD_DIR}/Bignums"
-
-git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}"
-
-( cd "${bignums_CI_DIR}" && make && make install)
+( cd "${CI_BUILD_DIR}/bignums" && make && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 8ce5f2418f..dc696f69d9 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-CoLoR_CI_DIR=${CI_BUILD_DIR}/color
+git_download CoLoR
 
-# Compile CoLoR
-git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}"
-( cd "${CoLoR_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/CoLoR" && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index c379a01767..3536cc70b2 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -34,7 +34,7 @@ export COQBIN="$COQBIN/"
 
 ls "$COQBIN"
 
-# Where we clone and build external developments
+# Where we download and build external developments
 CI_BUILD_DIR="$PWD/_build_ci"
 
 # shellcheck source=ci-basic-overlay.sh
@@ -44,29 +44,38 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do
     . "${overlay}"
 done
 
-mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
-
-# 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()
+# [git_download project] will download [project] and unpack it
+# in [$CI_BUILD_DIR/project] if the folder does not exist already;
+# if it does, it will do nothing except print a warning (this can be
+# useful when building locally).
+# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty
+# (local build), it uses git clone to perform the download.
+git_download()
 {
-  local _BRANCH=${1}
-  local _URL=${2}
-  local _DEST=${3}
-
-  # Allow an optional 4th argument for the commit
-  local _COMMIT=${4:-FETCH_HEAD}
-  local _DEPTH=()
-  if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi
-
-  mkdir -p "${_DEST}"
-  ( cd "${_DEST}"                                                     && \
-    if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \
-    echo "Checking out ${_DEST}"                                      && \
-    git fetch "${_URL}" "${_BRANCH}"                                  && \
-    git -c advice.detachedHead=false checkout "${_COMMIT}"            && \
-    echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
+  local PROJECT=$1
+  local DEST="$CI_BUILD_DIR/$PROJECT"
+
+  if [ -d "$DEST" ]; then
+    echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists."
+  elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then
+    local GITURL_VAR="${PROJECT}_CI_GITURL"
+    local GITURL="${!GITURL_VAR}"
+    local REF_VAR="${PROJECT}_CI_REF"
+    local REF="${!REF_VAR}"
+    git clone "$GITURL" "$DEST"
+    cd "$DEST"
+    git checkout "$REF"
+  else # When possible, we download tarballs to reduce bandwidth and latency
+    local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL"
+    local ARCHIVEURL="${!ARCHIVEURL_VAR}"
+    local REF_VAR="${PROJECT}_CI_REF"
+    local REF="${!REF_VAR}"
+    mkdir -p "$DEST"
+    cd "$DEST"
+    wget "$ARCHIVEURL/$REF.tar.gz"
+    tar xvfz "$REF.tar.gz" --strip-components=1
+    rm -f "$REF.tar.gz"
+  fi
 }
 
 make()
@@ -86,9 +95,9 @@ install_ssreflect()
 {
   echo 'Installing ssreflect'
 
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+  git_download mathcomp
 
-  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
+  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
     make Makefile.coq && \
     make -f Makefile.coq ssreflect/all_ssreflect.vo && \
     make -f Makefile.coq install )
@@ -100,9 +109,9 @@ install_ssralg()
 {
   echo 'Installing ssralg'
 
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+  git_download mathcomp
 
-  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
+  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
     make Makefile.coq && \
     make -f Makefile.coq algebra/all_algebra.vo && \
     make -f Makefile.coq install )
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 8d490591b6..01c35ceb4a 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -3,8 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert"
+git_download CompCert
 
-git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}"
-
-( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+( cd "${CI_BUILD_DIR}/CompCert" && \
+  ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index 5d57fce1c7..2373ea6c62 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph"
+git_download coq_dpdgraph
 
-git_checkout "${coq_dpdgraph_CI_BRANCH}" "${coq_dpdgraph_CI_GITURL}" "${coq_dpdgraph_CI_DIR}"
-
-( cd "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite )
+( cd "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index d86d61ef6a..5d8817491d 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,10 +3,9 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot"
-
 install_ssreflect
 
-git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}"
+FORCE_GIT=1
+git_download Coquelicot
 
-( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index 9298fc70af..7d5d70cf90 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-Corn_CI_DIR="${CI_BUILD_DIR}/corn"
+git_download Corn
 
-git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}"
-
-( cd "${Corn_CI_DIR}" && make && make install )
+( cd "${CI_BUILD_DIR}/Corn" && make && make install )
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
index a0d3aa6551..900d12c1dd 100755
--- a/dev/ci/ci-cross-crypto.sh
+++ b/dev/ci/ci-cross-crypto.sh
@@ -3,9 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+FORCE_GIT=1
+git_download cross_crypto
 
-git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
-( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
-
-( cd "${cross_crypto_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make )
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index 9c58034be1..9b4a06fd5b 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-Elpi_CI_DIR="${CI_BUILD_DIR}/elpi"
+git_download Elpi
 
-git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}"
-
-( cd "${Elpi_CI_DIR}" && make && make install )
+( cd "${CI_BUILD_DIR}/Elpi" && make && make install )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 98735b4ec4..998d50faa7 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -3,8 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-Equations_CI_DIR="${CI_BUILD_DIR}/Equations"
+git_download Equations
 
-git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}"
-
-( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install)
+( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \
+  make && make test-suite && make examples && make install)
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh
index cf212c2fb5..5eb167d97d 100755
--- a/dev/ci/ci-ext-lib.sh
+++ b/dev/ci/ci-ext-lib.sh
@@ -1,16 +1,8 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
 
-# This script could be included inside other ones
-# Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}" ];
-then
-    . "${ci_dir}/ci-common.sh"
-fi
+git_download ext_lib
 
-ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib"
-
-git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}"
-
-( cd "${ext_lib_CI_DIR}" && make && make install)
+( cd "${CI_BUILD_DIR}/ext_lib" && make && make install)
diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh
index fdc4c729b6..cb951630c8 100755
--- a/dev/ci/ci-fcsl-pcm.sh
+++ b/dev/ci/ci-fcsl-pcm.sh
@@ -3,10 +3,8 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm"
-
 install_ssreflect
 
-git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}"
+git_download fcsl_pcm
 
-( cd "${fcsl_pcm_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/fcsl_pcm" && make )
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 9429344159..e0395754e5 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -3,12 +3,11 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
-
-git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
-
-( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
+FORCE_GIT=1
+git_download fiat_crypto
 
 fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
+
+( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+  make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c6d2f0cfd9..7e8013be9b 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -3,13 +3,12 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
-
-git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
-
-( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
+FORCE_GIT=1
+git_download fiat_crypto
 
 # We need a larger stack size to not overflow ocamlopt+flambda when
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
-( cd "${fiat_crypto_CI_DIR}" && ulimit -s 32768 && make new-pipeline c-files )
+
+( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+  ulimit -s 32768 && make new-pipeline c-files )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 35c2284050..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -3,8 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat"
+FORCE_GIT=1
+git_download fiat_parsers
 
-git_checkout "${fiat_parsers_CI_BRANCH}" "${fiat_parsers_CI_GITURL}" "${fiat_parsers_CI_DIR}"
-
-( cd "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core )
+( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 8599e4d50e..e87483df0a 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-Flocq_CI_DIR="${CI_BUILD_DIR}/flocq"
+git_download Flocq
 
-git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}"
-
-( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 118d151500..8be5a06ed2 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology"
+git_download formal_topology
 
-git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}"
-
-( cd "${formal_topology_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/formal_topology" && make )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 24cd9c4272..8c57318477 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -3,10 +3,8 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
-
-git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
-
 install_ssralg
 
-( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
+git_download GeoCoq
+
+( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 184b90a50b..7eeeb09372 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
+git_download HoTT
 
-git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
-
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
+( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index 1af0f634c4..6960a8b98a 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -3,32 +3,28 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp"
-Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq"
-lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust"
-
 install_ssreflect
 
 # Setup lambdaRust first
-git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}"
+git_download lambdaRust
 
 # Extract required version of Iris
-Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup Iris
-git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}"
+git_download Iris
 
 # Extract required version of std++
-stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
+stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup std++
-git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}"
+git_download stdpp
 
 # Build std++
-( cd "${stdpp_CI_DIR}" && make && make install )
+( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
 
-# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris
-( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install )
+# Build and validate Iris
+( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install )
 
 # Build lambdaRust
-( cd "${lambdaRust_CI_DIR}" && make && make install )
+( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install )
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index 5981aaaae7..4df22bf249 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2"
+git_download ltac2
 
-git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}"
-
-( cd "${ltac2_CI_DIR}" && make && make tests && make install )
+( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 6a064b2971..ae31a8e7f8 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes"
+git_download math_classes
 
-git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}"
-
-( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install )
+( cd "${CI_BUILD_DIR}/math_classes" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 20328baf2a..a74f9fa4d3 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -4,11 +4,10 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
-oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
+git_download mathcomp
 
-git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
-git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
+( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install )
 
-( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
-( cd "${oddorder_CI_DIR}/" && make )
+git_download oddorder
+
+( cd "${CI_BUILD_DIR}/oddorder" && make )
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh
index 1372acb8e5..7075d4d7f6 100755
--- a/dev/ci/ci-mtac2.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -3,17 +3,10 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
+git_download unicoq
 
-# Setup UniCoq
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
 
-git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
+git_download mtac2
 
-( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install )
-
-# Setup MetaCoq
-
-git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
-
-( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index 32cba0808e..d22b9c8f7c 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -1,12 +1,9 @@
 #!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop"
-
-git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
+git_download pidetop
 
 # Travis / Gitlab have different filesystem layout due to use of
 # `-local`. We need to improve this divergence but if we use Dune this
@@ -17,6 +14,6 @@ else
    COQLIB="$COQBIN/../"
 fi
 
-( cd "${pidetop_CI_DIR}" && jbuilder build @install )
+( cd "${CI_BUILD_DIR}/pidetop" && jbuilder build @install )
 
-echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
+echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
index fc39e2685d..08686d7ced 100755
--- a/dev/ci/ci-quickchick.sh
+++ b/dev/ci/ci-quickchick.sh
@@ -1,18 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-
-# This script could be included inside other ones
-# Let's avoid to source ci-common twice in this case
-if [ -z "${CI_BUILD_DIR}" ];
-then
-    . "${ci_dir}/ci-common.sh"
-fi
-
-quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick"
+. "${ci_dir}/ci-common.sh"
 
 install_ssreflect
 
-git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}"
+git_download quickchick
 
-( cd "${quickchick_CI_DIR}" && make && make install)
+( cd "${CI_BUILD_DIR}/quickchick" && make && make install)
diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh
index 66f9801b3c..e7bcd80de7 100755
--- a/dev/ci/ci-simple-io.sh
+++ b/dev/ci/ci-simple-io.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-simple_io_CI_DIR="${CI_BUILD_DIR}/simple-io"
+git_download simple_io
 
-git_checkout "${simple_io_CI_BRANCH}" "${simple_io_CI_GITURL}" "${simple_io_CI_DIR}"
-
-( cd "${simple_io_CI_DIR}" && make build && make install)
+( cd "${CI_BUILD_DIR}/simple_io" && make build && make install)
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
deleted file mode 100755
index e77a553047..0000000000
--- a/dev/ci/ci-template.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${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 )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 31387c8ddc..a2f0bea555 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -3,8 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-tlc_CI_DIR="${CI_BUILD_DIR}/tlc"
+FORCE_GIT=1
+git_download tlc
 
-git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}"
-
-( cd "${tlc_CI_DIR}" && make )
+( cd "${CI_BUILD_DIR}/tlc" && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index aa20fe1ff0..a7644fee23 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
+git_download UniMath
 
-git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
-
-( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
+( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 7a097eaab4..0fec19205a 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-VST_CI_DIR="${CI_BUILD_DIR}/VST"
+git_download VST
 
-git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
-
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )
+( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index e6a2c4460b..d812df3ec0 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
-    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_REF=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
 fi
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
deleted file mode 100644
index 27f588e214..0000000000
--- a/dev/ci/user-overlays/07859-printers.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
-    Equations_CI_BRANCH=fix-printers
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh
deleted file mode 100644
index 293eeb5a5a..0000000000
--- a/dev/ci/user-overlays/07908-proj-mind.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then
-    Equations_CI_BRANCH=fix-proj-mind
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
deleted file mode 100644
index 56c0dc3433..0000000000
--- a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then
-    Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field
-    Equations_CI_GITURL=https://github.com/bollu/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
deleted file mode 100644
index 99a11b9fbf..0000000000
--- a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then
-    quickchick_CI_BRANCH=fix-for-pr-8063
-    quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index d38d1b06d1..68afe7ee4a 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,10 +7,12 @@ request to test it with the adapted version of the external project.
 An overlay is a file which defines where to look for the patched version so that
 testing is possible. It redefines some variables from
 [`ci-basic-overlay.sh`](../ci-basic-overlay.sh):
-give the name of your branch using a `_CI_BRANCH` variable and the location of
-your fork using a `_CI_GITURL` variable.
+give the name of your branch / commit using a `_CI_REF` variable and the
+location of your fork using a `_CI_GITURL` variable.
 The `_CI_GITURL` variable should be the URL of the repository without a
 trailing `.git`.
+If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is
+necessary to redefine the `_CI_ARCHIVEURL` variable as well.
 
 Moreover, the file contains very simple logic to test the pull request number
 or branch name and apply it only in this case.
@@ -25,7 +27,7 @@ Example: `00669-maximedenes-ssr-merge.sh` containing
 #!/bin/sh
 
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
-    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_REF=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
 fi
 ```