Merge branch 'trunk' into pr379

21 files changed, 337 insertions, 99 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
new file mode 100644
index 0000000000..336ce9d8f1
--- /dev/null
+++ b/dev/ci/ci-basic-overlay.sh
@@ -0,0 +1,112 @@
+#!/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
+########################################################################
+# Temporal overlay
+: ${HoTT_CI_BRANCH:=mz-8.7}
+: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
+# : ${HoTT_CI_BRANCH:=master}
+# : ${HoTT_CI_GITURL:=https://github.com/HoTT/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}
+
+########################################################################
+# CompCert
+########################################################################
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+
+########################################################################
+# VST
+########################################################################
+: ${VST_CI_BRANCH:=master}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.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 78ae7f02f9..3f0716511d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 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_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-common.sh b/dev/ci/ci-common.sh
index 2a6601e045..2711b7ecaa 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -1,6 +1,66 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 set -xe
 
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
 export PATH=`pwd`/bin:$PATH
+
 ls `pwd`/bin
+
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
+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
+# 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}
+
+  # Allow an optional 4th argument for the commit
+  local _COMMIT=${4:-FETCH_HEAD}
+  local _DEPTH=$(if [ -z "${4}" ]; then echo "--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 checkout ${_COMMIT}                                    && \
+    echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+  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 && \
+    sed -i.bak '/character/d'   Make && \
+    sed -i.bak '/real_closed/d' Make && \
+    sed -i.bak '/solvable/d'    Make && \
+    sed -i.bak '/field/d'       Make && \
+    sed -i.bak '/fingroup/d'    Make && \
+    sed -i.bak '/algebra/d'     Make && \
+    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+  echo -en 'travis_fold:end:ssr.install\\r'
+
+}
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index d4023c9165..c78ffdc2c0 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,10 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
+
 opam install -j ${NJOBS} -y menhir
-git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git
+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 4a23e51be6..40eff03b78 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,29 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
 
-# coquelicot just needs mathcomp
-( cd math-comp/mathcomp && \
-  sed -i.bak '/ssrtest/d'   Make && \
-  sed -i.bak '/odd_order/d'   Make && \
-  sed -i.bak '/all\/all.v/d'  Make && \
-  sed -i.bak '/character/d'   Make && \
-  sed -i.bak '/real_closed/d' Make && \
-  sed -i.bak '/solvable/d'    Make && \
-  sed -i.bak '/field/d'       Make && \
-  sed -i.bak '/fingroup/d'    Make && \
-  sed -i.bak '/algebra/d'     Make && \
-  make -j ${NJOBS} && make install )
+install_ssreflect
 
-# Setup ssr
-# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
-# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
 
-# Setup coquelicot
-git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
-
-( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
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 c594f83603..93d39aab07 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,12 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git
+fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 
-( cd fiat-crypto && make -j ${NJOBS} )
-
-# ( cd corn && 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
new file mode 100755
index 0000000000..c62aa1d859
--- /dev/null
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
+
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
+
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index b9cf649a1a..ec19bd9939 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,9 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 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 589a826e02..4e5aa2687b 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,16 +1,16 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 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 clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
+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 && \
+  sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
   coq_makefile -f Make -o Makefile                        && \
   make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 8f82ba9f21..1bf6e9a872 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 -b mz-8.6 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 e97e2c19e3..262dd6fa01 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,35 +1,26 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-# XXX: Refactor into install-ssreflect
-git clone --depth 1 https://github.com/math-comp/math-comp.git
-
-# coquelicot just needs mathcomp
-( cd math-comp/mathcomp && \
-  sed -i.bak '/ssrtest/d'     Make && \
-  sed -i.bak '/odd_order/d'   Make && \
-  sed -i.bak '/all\/all.v/d'  Make && \
-  sed -i.bak '/character/d'   Make && \
-  sed -i.bak '/real_closed/d' Make && \
-  sed -i.bak '/solvable/d'    Make && \
-  sed -i.bak '/field/d'       Make && \
-  sed -i.bak '/fingroup/d'    Make && \
-  sed -i.bak '/algebra/d'     Make && \
-  make -j ${NJOBS} && make install )
-
-# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S
-# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
-# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
+
+Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
+
+install_ssreflect
+
+# Setup Iris first, as it is needed to compute the dependencies
+
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins
 
 # Setup stdpp
-git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+stdpp_CI_GITURL=${IRIS_DEP[1]}.git
+stdpp_CI_COMMIT=${IRIS_DEP[2]}
 
-( cd coq-stdpp && make -j ${NJOBS} && make install )
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
 
-# Setup Iris
-git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
 
-( cd iris-coq && make -j ${NJOBS} )
+# Build iris now
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 9127c18951..beb75773b7 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,12 +1,20 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
-# $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git
-( cd math-classes && make -j ${NJOBS} && make install )
+math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git
-( cd corn         && make -j ${NJOBS} )
+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 b833792419..bb8188da4e 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,13 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+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                              && \
-     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 )
+( 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 9a9bd3648b..e31691179e 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,19 @@
-#!/bin/bash
+#!/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_DIR=${CI_BUILD_DIR}/unicoq
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
-git clone --depth 1 https://github.com/unicoq/unicoq.git
+# Setup UniCoq
 
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
 
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+# 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-sf.sh b/dev/ci/ci-sf.sh
index 5e41211f1a..7d23ccad97 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,9 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 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-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 2161a11461..ce26399378 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,8 +1,10 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone 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
new file mode 100755
index 0000000000..175b82b5f9
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
+
+( cd ${UniMath_CI_DIR}                        && \
+  sed -i.bak '/Folds/d'              Makefile && \
+  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
+  make -j ${NJOBS} BUILD_COQ=no )
+
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
new file mode 100644
index 0000000000..0285747432
--- /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.
+
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
new file mode 100755
index 0000000000..c111951852
--- /dev/null
+++ b/dev/ci/ci-vst.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+VST_CI_DIR=${CI_BUILD_DIR}/VST
+
+# opam install -j ${NJOBS} -y menhir
+git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
+
+# Targets are: msl veric floyd
+# Patch to avoid the upper version limit
+( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} )