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