From 30a2def37ecdeeed24325089a0b0ca264100389c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 19:37:15 +0100
Subject: [travis] [External CI] Factor out math-comp installs.

We make math-comp overlays easier, we also start structuring the
scripts a bit more.
---
 dev/ci/ci-common.sh | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a6601e045..087572e47d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -4,3 +4,46 @@ set -xe
 
 export PATH=`pwd`/bin:$PATH
 ls `pwd`/bin
+
+# Maybe we should just use Ruby...
+mathcomp_CI_BRANCH=master
+mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+
+# git_checkout branch
+git_checkout()
+{
+  local _BRANCH=${1}
+  local _URL=${2}
+  local _DEST=${3}
+
+  echo "Checking out ${_DEST}"
+  git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
+  ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+  checkout_mathcomp math-comp
+  ( cd math-comp/mathcomp            && \
+    sed -i.bak '/ssrtest/d'     Make && \
+    sed -i.bak '/odd_order/d'   Make && \
+    sed -i.bak '/all\/all.v/d'  Make && \
+    sed -i.bak '/character/d'   Make && \
+    sed -i.bak '/real_closed/d' Make && \
+    sed -i.bak '/solvable/d'    Make && \
+    sed -i.bak '/field/d'       Make && \
+    sed -i.bak '/fingroup/d'    Make && \
+    sed -i.bak '/algebra/d'     Make && \
+    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+  echo -en 'travis_fold:end:ssr.install\\r'
+
+}
-- 
cgit v1.2.3


From 575bbed527977aee520a3954a196f5b59ae947c5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 11 Feb 2017 02:06:01 +0100
Subject: [travis] [External CI] CompCert official 8.6 support + UniMath

---
 dev/ci/ci-common.sh | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 087572e47d..412da626fd 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,7 +2,10 @@
 
 set -xe
 
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
 export PATH=`pwd`/bin:$PATH
+
 ls `pwd`/bin
 
 # Maybe we should just use Ruby...
-- 
cgit v1.2.3