14 files changed, 119 insertions, 73 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1dfade261..99ec43e41 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -28,11 +28,11 @@
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: ${math_classes_CI_BRANCH:=v8.6}
-: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+: ${math_classes_CI_BRANCH:=external-bignums}
+: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git}
 
-: ${Corn_CI_BRANCH:=v8.6}
-: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+: ${Corn_CI_BRANCH:=external-bignums}
+: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git}
 
 ########################################################################
 # Iris
@@ -46,8 +46,8 @@
 ########################################################################
 # HoTT
 ########################################################################
-# Temporal overlay
-: ${HoTT_CI_BRANCH:=mz-8.7}
+# Temporary overlay
+: ${HoTT_CI_BRANCH:=ocaml.4.02.3}
 : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
 # : ${HoTT_CI_BRANCH:=master}
 # : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
@@ -73,38 +73,26 @@
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: ${CompCert_CI_BRANCH:=less_init_plugins}
+: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
 
 ########################################################################
 # VST
 ########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: ${VST_CI_BRANCH:=less_init_plugins}
+: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git}
 
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=master}
-: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=trunk__API}
+: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
 
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
-
-########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
+: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
 ########################################################################
 # formal-topology
@@ -113,6 +101,12 @@
 : ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
 
 ########################################################################
+# coq-dpdgraph
+########################################################################
+: ${coq_dpdgraph_CI_BRANCH:=coq-trunk}
+: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+
+########################################################################
 # CoLoR
 ########################################################################
 : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
@@ -127,3 +121,9 @@
 ########################################################################
 : ${tlc_CI_BRANCH:=master}
 : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
+########################################################################
+# Bignums
+########################################################################
+: ${bignums_CI_BRANCH:=master}
+: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 9e6b6b108..000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index a642354e6..000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make src )
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
new file mode 100755
index 000000000..ff5935d4c
--- /dev/null
+++ b/dev/ci/ci-bignums.sh
@@ -0,0 +1,16 @@
+#!/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
+    source ${ci_dir}/ci-common.sh
+fi
+
+bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
+
+git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
+
+( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 57b50fc8d..309050057 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,31 @@ source ${ci_dir}/ci-common.sh
 
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
+# Compiles CoLoR
+
 svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
 
+sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
+
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
 ( cd ${Color_CI_DIR} && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index d373ed3b1..238960948 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,16 +2,25 @@
 
 set -xe
 
+if [ -n "${GITLAB_CI}" ];
+then
+    export COQBIN=`pwd`/install/bin
+else
+    export COQBIN=`pwd`/bin
+fi
+export PATH="$COQBIN:$PATH"
+
 # Coq's tools need an ending slash :S, we should fix them.
-export COQBIN=`pwd`/bin/
-export PATH=`pwd`/bin:$PATH
+export COQBIN="$COQBIN/"
 
-ls `pwd`/bin
+ls "$COQBIN"
 
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-source ${ci_dir}/ci-user-overlay.sh
+for overlay in ${ci_dir}/user-overlays/*.sh; do
+  source ${overlay}
+done
 source ${ci_dir}/ci-basic-overlay.sh
 
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
new file mode 100755
index 000000000..e8018158b
--- /dev/null
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+
+git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
+
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index e7f98c3de..292331b81 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ 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 parsers parsers-examples )
+( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 056655cf6..2556f84a5 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -9,6 +9,10 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
 # Setup Math-Classes
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index f177d231b..2837dee96 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,6 +7,10 @@ math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
 Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
 # Setup Math-Classes
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index ae7a13b53..6e6c7012b 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
 
 
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
deleted file mode 100644
index 028574743..000000000
--- a/dev/ci/ci-user-overlay.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/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/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
new file mode 100644
index 000000000..af4a96f4a
--- /dev/null
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
new file mode 100644
index 000000000..9146d3d52
--- /dev/null
+++ b/dev/ci/user-overlays/README.md
@@ -0,0 +1,14 @@
+# Add overlays for your pull requests in this directory
+
+An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+
+The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+
+Example: `00669-maximedenes-ssr-merge.sh` containing
+
+```
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
+```