Merge remote-tracking branch 'upstream/trunk' into trunk

7 files changed, 86 insertions, 12 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..54db58c01f 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}
@@ -85,8 +85,8 @@
 ########################################################################
 # 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
@@ -97,14 +97,14 @@
 ########################################################################
 # bedrock_src
 ########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=trunk__API}
+: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
 
 ########################################################################
 # bedrock_facade
 ########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=trunk__API}
+: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
 
 ########################################################################
 # formal-topology
@@ -113,6 +113,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 +133,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-bignums.sh b/dev/ci/ci-bignums.sh
new file mode 100755
index 0000000000..ff5935d4c7
--- /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 3f0716511d..57f569858b 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,17 @@ 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
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
new file mode 100755
index 0000000000..e8018158bf
--- /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-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index ecb36349fb..64b78c0396 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 beb75773b7..46581c6381 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-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 195ede6d00..200d431bcb 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -30,3 +30,20 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 
+echo "DEBUG: ci-user-overlay.sh 0"
+if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
+    echo "DEBUG: ci-user-overlay.sh 1"
+    bedrock_src_CI_BRANCH=trunk__API
+    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    bedrock_facade_CI_BRANCH=trunk__API
+    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
+    fiat_parsers_CI_BRANCH=trunk__API
+    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
+fi
+
+if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
+    math_classes_CI_BRANCH=external-bignums
+    math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
+    Corn_CI_BRANCH=external-bignums
+    Corn_CI_GITURL=https://github.com/letouzey/corn.git
+fi