diff options
Diffstat (limited to 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh new file mode 100644 index 0000000000..412da626fd --- /dev/null +++ b/dev/ci/ci-common.sh @@ -0,0 +1,52 @@ +#!/bin/bash + +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... +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' + +} |
