From 332d85dc6c69fbcc2aae7b9d4af975fb43769b05 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 23:43:09 -0400
Subject: Add coq-dpdgraph CI

---
 dev/ci/ci-basic-overlay.sh |  6 ++++++
 dev/ci/ci-coq-dpdgraph.sh  | 10 ++++++++++
 2 files changed, 16 insertions(+)
 create mode 100755 dev/ci/ci-coq-dpdgraph.sh

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..8bd68f4ee6 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -112,6 +112,12 @@
 : ${formal_topology_CI_BRANCH:=ci}
 : ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
 
+########################################################################
+# coq-dpdgraph
+########################################################################
+: ${coq_dpdgraph_CI_BRANCH:=master}
+: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+
 ########################################################################
 # CoLoR
 ########################################################################
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
new file mode 100755
index 0000000000..44b0e4c4d5
--- /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 | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
-- 
cgit v1.2.3


From f371ead0234693ab8f68591d160cc2ee4dd8509f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 2 Jun 2017 20:12:23 -0400
Subject: Add an overlay for coq-dpdgraph for 8.7

---
 dev/ci/ci-basic-overlay.sh | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8bd68f4ee6..73a3ba04f2 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -115,8 +115,11 @@
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-: ${coq_dpdgraph_CI_BRANCH:=master}
-: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+# Temporary overlay
+: ${coq_dpdgraph_CI_BRANCH:=trunk+clobber-test-suite}
+: ${coq_dpdgraph_CI_GITURL:=https://github.com/JasonGross/coq-dpdgraph.git}
+#: ${coq_dpdgraph_CI_BRANCH:=master}
+#: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
 
 ########################################################################
 # CoLoR
-- 
cgit v1.2.3


From 29ba5cdc0ea31ea62c727f8dcf53d2c805d4bcb3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 8 Jun 2017 13:07:00 -0400
Subject: Remove coq-dpdgraph overlay

---
 dev/ci/ci-basic-overlay.sh | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 73a3ba04f2..81f4c87177 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -115,11 +115,8 @@
 ########################################################################
 # coq-dpdgraph
 ########################################################################
-# Temporary overlay
-: ${coq_dpdgraph_CI_BRANCH:=trunk+clobber-test-suite}
-: ${coq_dpdgraph_CI_GITURL:=https://github.com/JasonGross/coq-dpdgraph.git}
-#: ${coq_dpdgraph_CI_BRANCH:=master}
-#: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
+: ${coq_dpdgraph_CI_BRANCH:=coq-trunk}
+: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}
 
 ########################################################################
 # CoLoR
-- 
cgit v1.2.3


From 55ffdf526f8dbf99a88a05910e646446f6bb3421 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 8 Jun 2017 13:08:13 -0400
Subject: Mirror dpdgraph's travis test more accurately

---
 dev/ci/ci-coq-dpdgraph.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index 44b0e4c4d5..e8018158bf 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -7,4 +7,4 @@ 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 | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
+( 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) )
-- 
cgit v1.2.3


From 75f42c5c4f350f301ef1968459f4f19f7a349ad4 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 11 Jun 2017 20:22:43 -0400
Subject: Point ci-hott at a newer version of HoTT

---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..d75011de3f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -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}
-- 
cgit v1.2.3


From 8443867a2f944c3ecaf0b0b826368c29935a21e1 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Thu, 8 Jun 2017 18:30:18 +0200
Subject: add overlays

---
 dev/ci/ci-user-overlay.sh | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 195ede6d00..0edaf07efc 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -30,3 +30,13 @@ 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
-- 
cgit v1.2.3


From 013c0232953f1f5832c30940119da05847e99ce2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 12 Jun 2017 15:43:12 +0200
Subject: Temporary overlay, waiting for upstream PR merges.

---
 dev/ci/ci-basic-overlay.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index a6972c9500..7a9df93c45 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -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
-- 
cgit v1.2.3


From fe972a369adf533e2f4ec89eafb63b08a26e2ec7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 6 Jun 2017 19:45:48 +0200
Subject: [travis] adapt CoLoR compilation to depend on the bignum package

---
 dev/ci/ci-color.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 3f0716511d..cb212e845c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,19 @@ source ${ci_dir}/ci-common.sh
 
 Color_CI_DIR=${CI_BUILD_DIR}/color
 
+# Setup Bignums
+
+git_checkout master https://github.com/coq/bignums.git bignums
+
+( cd bignums && make -j ${NJOBS} && make install )
+
+# 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} )
-- 
cgit v1.2.3


From 08e86c0af77e83b8569fe611b9fb74e772d710a8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 6 Jun 2017 20:47:26 +0200
Subject: [travis] overlay + extra deps for math-classes (and formal-topology)

---
 dev/ci/ci-formal-topology.sh | 6 ++++++
 dev/ci/ci-math-classes.sh    | 6 ++++++
 dev/ci/ci-user-overlay.sh    | 5 +++++
 3 files changed, 17 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index ecb36349fb..87171ba0bd 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -9,6 +9,12 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
+# Setup Bignums
+
+git_checkout master https://github.com/coq/bignums.git bignums
+
+( cd bignums && make -j ${NJOBS} && make install )
+
 # 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..10b9d7af24 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,6 +7,12 @@ math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
 Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
+# Setup Bignums
+
+git_checkout master https://github.com/coq/bignums.git bignums
+
+( cd bignums && make -j ${NJOBS} && make install )
+
 # 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 0edaf07efc..594e3c3744 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -40,3 +40,8 @@ if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_make
     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
+fi
-- 
cgit v1.2.3


From 0fd563c07433db5aad5c5a3f196ea692bb60c04e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 6 Jun 2017 21:22:15 +0200
Subject: [travis] extra test ci-bignums (+factorize other scripts)

---
 dev/ci/ci-basic-overlay.sh   |  6 ++++++
 dev/ci/ci-bignums.sh         | 16 ++++++++++++++++
 dev/ci/ci-color.sh           |  4 +---
 dev/ci/ci-formal-topology.sh |  4 +---
 dev/ci/ci-math-classes.sh    |  4 +---
 5 files changed, 25 insertions(+), 9 deletions(-)
 create mode 100755 dev/ci/ci-bignums.sh

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3adc319355..98d342412a 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -133,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 cb212e845c..57f569858b 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -7,9 +7,7 @@ Color_CI_DIR=${CI_BUILD_DIR}/color
 
 # Setup Bignums
 
-git_checkout master https://github.com/coq/bignums.git bignums
-
-( cd bignums && make -j ${NJOBS} && make install )
+source ${ci_dir}/ci-bignums.sh
 
 # Compiles CoLoR
 
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 87171ba0bd..64b78c0396 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -11,9 +11,7 @@ formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
 # Setup Bignums
 
-git_checkout master https://github.com/coq/bignums.git bignums
-
-( cd bignums && make -j ${NJOBS} && make install )
+source ${ci_dir}/ci-bignums.sh
 
 # Setup Math-Classes
 
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 10b9d7af24..46581c6381 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -9,9 +9,7 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
 
 # Setup Bignums
 
-git_checkout master https://github.com/coq/bignums.git bignums
-
-( cd bignums && make -j ${NJOBS} && make install )
+source ${ci_dir}/ci-bignums.sh
 
 # Setup Math-Classes
 
-- 
cgit v1.2.3


From 268ccbb0d3d990e42cef4ae4833e0e7964aea24d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 10 Jun 2017 17:35:10 +0200
Subject: [travis] overlay for corn

---
 dev/ci/ci-user-overlay.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 594e3c3744..200d431bcb 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -44,4 +44,6 @@ 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
-- 
cgit v1.2.3


From 7e63c300a3aa1e3befb29bab9094e8b1939824bb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 13 Jun 2017 17:22:42 +0200
Subject: Temporary overlays for bignums.

---
 dev/ci/ci-basic-overlay.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 98d342412a..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
-- 
cgit v1.2.3