blob: 1bfdf7dfbeb75e319d1a1b54e5a285944cf2362c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
#!/usr/bin/env bash
set -xe
if [ -n "${GITLAB_CI}" ];
then
export COQBIN=`pwd`/_install_ci/bin
export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
else
export COQBIN=`pwd`/bin
fi
export PATH="$COQBIN:$PATH"
# Coq's tools need an ending slash :S, we should fix them.
export COQBIN="$COQBIN/"
ls "$COQBIN"
# Where we clone and build external developments
CI_BUILD_DIR=`pwd`/_build_ci
for overlay in ${ci_dir}/user-overlays/*.sh; do
source ${overlay}
done
source ${ci_dir}/ci-basic-overlay.sh
mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
# git_checkout branch url dest will create a git repository
# in <dest> (if it does not exist already) and checkout the
# remote branch <branch> from <url>
git_checkout()
{
local _BRANCH=${1}
local _URL=${2}
local _DEST=${3}
# Allow an optional 4th argument for the commit
local _COMMIT=${4:-FETCH_HEAD}
local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
mkdir -p ${_DEST}
( cd ${_DEST} && \
if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
echo "Checking out ${_DEST}" && \
git fetch ${_URL} ${_BRANCH} && \
git checkout ${_COMMIT} && \
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 ${mathcomp_CI_DIR}
( cd ${mathcomp_CI_DIR}/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 all && make install )
echo -en 'travis_fold:end:ssr.install\\r'
}
|
