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')

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')

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')

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')

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