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 From 56dc3e331c6b4b2bfa5ac072db57db8250884ce3 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 12:33:37 +0100 Subject: Improve build of travis target on local machine. - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). --- dev/ci/ci-common.sh | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 412da626fd..cc34bc2957 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -12,6 +12,9 @@ ls `pwd`/bin mathcomp_CI_BRANCH=master mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci + # git_checkout branch git_checkout() { @@ -19,9 +22,15 @@ git_checkout() 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'`" ) + mkdir -p ${CI_BUILD_DIR} + cd ${CI_BUILD_DIR} + + if [ ! -d ${_DEST} ] ; then + echo "Checking out ${_DEST}" + git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} + fi + ( cd ${_DEST} && git pull && + echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } checkout_mathcomp() -- cgit v1.2.3 From ba36aab9ad9a3d210211e1d4527dd0f6f493ca05 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 16:14:39 +0100 Subject: [travis] Change headband for wider compatibility. --- dev/ci/ci-common.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index cc34bc2957..94fd00c0d2 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -xe -- cgit v1.2.3 From fd5c5da475baea11d7ee2e1c2e965d7faeed3f33 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 8 Mar 2017 09:56:01 +0100 Subject: [travis] Make the git_checkout function more reliable. This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). --- dev/ci/ci-common.sh | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 94fd00c0d2..6f624ab6ec 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,28 +8,29 @@ export PATH=`pwd`/bin:$PATH ls `pwd`/bin +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci + # Maybe we should just use Ruby... mathcomp_CI_BRANCH=master mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp -# Where we clone and build external developments -CI_BUILD_DIR=`pwd`/_build_ci - -# git_checkout branch +# git_checkout branch url dest will create a git repository +# in (if it does not exist already) and checkout the +# remote branch from git_checkout() { local _BRANCH=${1} local _URL=${2} local _DEST=${3} - mkdir -p ${CI_BUILD_DIR} - cd ${CI_BUILD_DIR} - - if [ ! -d ${_DEST} ] ; then - echo "Checking out ${_DEST}" - git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} - fi - ( cd ${_DEST} && git pull && + mkdir -p ${_DEST} + ( cd ${_DEST} && \ + if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch ${_URL} ${_BRANCH} && \ + git checkout FETCH_HEAD && \ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } @@ -43,8 +44,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp math-comp - ( cd math-comp/mathcomp && \ + 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 && \ -- cgit v1.2.3 From 2cee6aa7a30b39c53e23fc69f0b9e7754ebee740 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Mar 2017 19:53:00 +0100 Subject: [travis] Basic support for overlays. We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. --- dev/ci/ci-common.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 6f624ab6ec..c94f150263 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -11,9 +11,9 @@ ls `pwd`/bin # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci -# Maybe we should just use Ruby... -mathcomp_CI_BRANCH=master -mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git +source ${ci_dir}/ci-user-overlay.sh +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 -- cgit v1.2.3 From 44b2c7979e1ea3a834f4e9bd2fcd631d568b895e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 17:17:33 +0100 Subject: [travis] Fix iris-coq build. We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83 --- dev/ci/ci-common.sh | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index c94f150263..2711b7ecaa 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -25,12 +25,16 @@ git_checkout() 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 1 ${_URL} . ; fi && \ + if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ echo "Checking out ${_DEST}" && \ git fetch ${_URL} ${_BRANCH} && \ - git checkout FETCH_HEAD && \ + git checkout ${_COMMIT} && \ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } -- cgit v1.2.3