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 +++++++++++++++++++++++++++++++++++++++++++ dev/ci/ci-compcert.sh | 2 +- dev/ci/ci-coquelicot.sh | 21 ++------------------- dev/ci/ci-fiat-crypto.sh | 5 +---- dev/ci/ci-flocq.sh | 2 +- dev/ci/ci-geocoq.sh | 2 +- dev/ci/ci-hott.sh | 2 +- dev/ci/ci-iris-coq.sh | 24 +++--------------------- dev/ci/ci-math-classes.sh | 4 ++-- dev/ci/ci-math-comp.sh | 10 +++++----- dev/ci/ci-metacoq.sh | 4 ++-- dev/ci/ci-tlc.sh | 2 +- 12 files changed, 63 insertions(+), 58 deletions(-) (limited to 'dev/ci') 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' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4023c9165..d4d503278a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh opam install -j ${NJOBS} -y menhir -git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git +git_checkout coq-8.6 https://github.com/maximedenes/CompCert.git CompCert # Patch to avoid the upper version limit ( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 4a23e51be6..94bd5e468f 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -4,26 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( 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 -j ${NJOBS} && make install ) - -# Setup ssr -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup coquelicot -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot ( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c594f83603..c669195ddd 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -4,9 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git +git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto ( cd fiat-crypto && make -j ${NJOBS} ) - -# ( cd corn && make -j ${NJOBS} ) - diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index b9cf649a1a..345924e40a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -4,6 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq ( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 589a826e02..ce870e52b5 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,7 +7,7 @@ source ${ci_dir}/ci-common.sh GeoCoq_CI_BRANCH=master GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git -git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq ( cd GeoCoq && \ ./configure.sh && \ diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 8f82ba9f21..aaffc9d484 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git +git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index e97e2c19e3..c21af976f4 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -4,32 +4,14 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Refactor into install-ssreflect -git clone --depth 1 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( 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 -j ${NJOBS} && make install ) - -# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup stdpp -git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git +git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp ( cd coq-stdpp && make -j ${NJOBS} && make install ) # Setup Iris -git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git +git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq ( cd iris-coq && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 9127c18951..4450dc0710 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -4,9 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git +git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes ( cd math-classes && make -j ${NJOBS} && make install ) -git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git +git_checkout v8.6 https://github.com/c-corn/corn.git corn ( cd corn && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index b833792419..2eb150cb52 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git +checkout_mathcomp math-comp # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) +( cd math-comp/mathcomp && \ + sed -i.bak '/PFsection/d' Make && \ + sed -i.bak '/stripped_odd_order_theorem/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 9a9bd3648b..91a33695b0 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -6,11 +6,11 @@ source ${ci_dir}/ci-common.sh # MetaCoq + UniCoq -git clone --depth 1 https://github.com/unicoq/unicoq.git +git_checkout master https://github.com/unicoq/unicoq.git unicoq ( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git +git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq ( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 2161a11461..b946324924 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone https://gforge.inria.fr/git/tlc/tlc.git +git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc ( cd tlc && make -j ${NJOBS} ) -- 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 +++ dev/ci/ci-compcert.sh | 5 ++++- dev/ci/ci-unimath.sh | 15 +++++++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) create mode 100755 dev/ci/ci-unimath.sh (limited to 'dev/ci') 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... diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4d503278a..ec09389f8e 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +CompCert_CI_BRANCH=master +CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git + opam install -j ${NJOBS} -y menhir -git_checkout coq-8.6 https://github.com/maximedenes/CompCert.git CompCert +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert # Patch to avoid the upper version limit ( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 0000000000..15e619acbb --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_BRANCH=master +UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath + +( cd UniMath && \ + sed -i.bak '/Folds/d' Makefile && \ + sed -i.bak '/HomologicalAlgebra/d' Makefile && \ + make -j ${NJOBS} BUILD_COQ=no ) + -- cgit v1.2.3 From d9d8977cf213f0d4b2e8d324c759c23df58ba457 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 21 Feb 2017 09:46:34 +0100 Subject: [travis] track an 8.7 specific branch of HoTT. This is required since we merged PR#309: Ltac as a plugin. --- dev/ci/ci-hott.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/ci') diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index aaffc9d484..0c07564c02 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.6 https://github.com/ejgallego/HoTT.git HoTT +git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) -- cgit v1.2.3 From 4567e3a0a44a6c398375effa7d9a49342172512a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Feb 2017 02:28:27 +0100 Subject: [travis] [External CI] fiat-parsers --- dev/ci/ci-fiat-parsers.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100755 dev/ci/ci-fiat-parsers.sh (limited to 'dev/ci') diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 0000000000..15d73078fd --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_parsers_CI_BRANCH=master +fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat + +( cd fiat && make -j ${NJOBS} parsers ) -- cgit v1.2.3 From ae5ae4967c423a26b99666dcce441236dd7b9a7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Mar 2017 16:33:47 +0100 Subject: [travis] Move GeoCoq to allow fail. We need to agree a bit more with upstream. --- dev/ci/ci-geocoq.sh | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev/ci') diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index ce870e52b5..29667b018a 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -12,5 +12,7 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq ( cd GeoCoq && \ ./configure.sh && \ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + sed -i.bak '/Elements\/Book_1\.v/d' Make && \ + sed -i.bak '/Elements\/Book_3\.v/d' Make && \ coq_makefile -f Make -o Makefile && \ make -j ${NJOBS} ) -- 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') 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-color.sh | 2 +- dev/ci/ci-common.sh | 2 +- dev/ci/ci-compcert.sh | 2 +- dev/ci/ci-coquelicot.sh | 2 +- dev/ci/ci-cpdt.sh | 2 +- dev/ci/ci-fiat-crypto.sh | 2 +- dev/ci/ci-fiat-parsers.sh | 2 +- dev/ci/ci-flocq.sh | 2 +- dev/ci/ci-geocoq.sh | 2 +- dev/ci/ci-hott.sh | 2 +- dev/ci/ci-iris-coq.sh | 2 +- dev/ci/ci-math-classes.sh | 2 +- dev/ci/ci-math-comp.sh | 2 +- dev/ci/ci-metacoq.sh | 2 +- dev/ci/ci-sf.sh | 2 +- dev/ci/ci-tlc.sh | 2 +- dev/ci/ci-unimath.sh | 2 +- 17 files changed, 17 insertions(+), 17 deletions(-) (limited to 'dev/ci') diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 78ae7f02f9..36c7b9e965 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/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 diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index ec09389f8e..3b897f679a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 94bd5e468f..2052a1e5ff 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 18d7561804..0e791ebbfd 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c669195ddd..683f9712d6 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 15d73078fd..5e52f44116 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 345924e40a..d398660444 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 29667b018a..7502139c2b 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 0c07564c02..9d27be2e91 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index c21af976f4..7044c3859d 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4450dc0710..c5105a8486 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 2eb150cb52..1b6c6fb847 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 91a33695b0..597a6ab7b3 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 5e41211f1a..c451bf26a1 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index b946324924..df86b3cadd 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 15e619acbb..5b7fc1c053 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -- cgit v1.2.3 From 710c1e1f49ce834acb9488704bcbbf13c4ebaf91 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 7 Mar 2017 23:30:29 +0100 Subject: [travis] Adding a template file and using it for all targets. --- dev/ci/ci-color.sh | 7 +++++-- dev/ci/ci-compcert.sh | 5 +++-- dev/ci/ci-coquelicot.sh | 10 ++++++---- dev/ci/ci-fiat-crypto.sh | 9 ++++++--- dev/ci/ci-fiat-parsers.sh | 6 +++--- dev/ci/ci-flocq.sh | 9 ++++++--- dev/ci/ci-geocoq.sh | 6 +++--- dev/ci/ci-hott.sh | 8 ++++++-- dev/ci/ci-iris-coq.sh | 19 ++++++++++++++----- dev/ci/ci-math-classes.sh | 22 +++++++++++++++++----- dev/ci/ci-math-comp.sh | 6 ++++-- dev/ci/ci-metacoq.sh | 20 ++++++++++++++------ dev/ci/ci-template.sh | 12 ++++++++++++ dev/ci/ci-tlc.sh | 8 ++++++-- dev/ci/ci-unimath.sh | 5 +++-- 15 files changed, 108 insertions(+), 44 deletions(-) create mode 100755 dev/ci/ci-template.sh (limited to 'dev/ci') diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 36c7b9e965..fbcf9be1d6 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,6 +3,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color +Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color +Color_CI_DIR=${CI_BUILD_DIR}/color -( cd color && make -j ${NJOBS} ) +svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} + +( cd ${Color_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 3b897f679a..111222ac7f 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,9 +5,10 @@ source ${ci_dir}/ci-common.sh CompCert_CI_BRANCH=master CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git +CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir -git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} # Patch to avoid the upper version limit -( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) +( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 2052a1e5ff..9dfdb87451 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,14 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +Coquelicot_CI_BRANCH=master +Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git +Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot + install_ssreflect -# Setup coquelicot -git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot +git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} -( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 683f9712d6..7fc0dae2c0 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,9 +1,12 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto +fiat_crypto_CI_BRANCH=master +fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git +fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto -( cd fiat-crypto && make -j ${NJOBS} ) +git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} + +( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 5e52f44116..0b3312e878 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh fiat_parsers_CI_BRANCH=master fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git +fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat -git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} -( cd fiat && make -j ${NJOBS} parsers ) +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index d398660444..30eca7a3e9 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,9 +1,12 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq +Flocq_CI_BRANCH=master +Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git +Flocq_CI_DIR=${CI_BUILD_DIR}/flocq -( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} + +( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7502139c2b..7b5950c887 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,13 +3,13 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: replace by generic template GeoCoq_CI_BRANCH=master GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git +GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} -( cd GeoCoq && \ +( cd ${GeoCoq_CI_DIR} && \ ./configure.sh && \ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ sed -i.bak '/Elements\/Book_1\.v/d' Make && \ diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 9d27be2e91..62733c9452 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT +HoTT_CI_BRANCH=mz-8.7 +HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git +HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT -( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) +git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} + +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 7044c3859d..10f2c2b4bd 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,17 +1,26 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +stdpp_CI_BRANCH=master +stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git +stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp + +Iris_CI_BRANCH=master +Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git +Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq + install_ssreflect # Setup stdpp -git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp -( cd coq-stdpp && make -j ${NJOBS} && make install ) +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} + +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) # Setup Iris -git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq -( cd iris-coq && make -j ${NJOBS} ) +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} + +( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index c5105a8486..e6a57404fe 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,12 +1,24 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes -( cd math-classes && make -j ${NJOBS} && make install ) +math_classes_CI_BRANCH=v8.6 +math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes -git_checkout v8.6 https://github.com/c-corn/corn.git corn -( cd corn && make -j ${NJOBS} ) +Corn_CI_BRANCH=v8.6 +Corn_CI_GITURL=https://github.com/c-corn/corn.git +Corn_CI_DIR=${CI_BUILD_DIR}/corn +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 1b6c6fb847..bb8188da4e 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,12 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -checkout_mathcomp math-comp +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +checkout_mathcomp ${mathcomp_CI_DIR} # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ +( cd ${mathcomp_CI_DIR}/mathcomp && \ sed -i.bak '/PFsection/d' Make && \ sed -i.bak '/stripped_odd_order_theorem/d' Make && \ make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 597a6ab7b3..1ea56af29a 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,16 +1,24 @@ #!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# MetaCoq + UniCoq +unicoq_CI_BRANCH=master +unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -git_checkout master https://github.com/unicoq/unicoq.git unicoq +metacoq_CI_BRANCH=master +metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git +metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq -( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +# Setup UniCoq -git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq +git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} -( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +# Setup MetaCoq + +git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} + +( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh new file mode 100755 index 0000000000..700105aed4 --- /dev/null +++ b/dev/ci/ci-template.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Template_CI_BRANCH=master +Template_CI_GITURL=https://github.com/Template/Template +Template_CI_DIR=${CI_BUILD_DIR}/Template + +git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} + +( cd ${Template_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index df86b3cadd..415f9b38f9 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc +tlc_CI_BRANCH=master +tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git +tlc_CI_DIR=${CI_BUILD_DIR}/tlc -( cd tlc && make -j ${NJOBS} ) +git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} + +( cd ${tlc_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 5b7fc1c053..4c4b4f1ce1 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -5,10 +5,11 @@ source ${ci_dir}/ci-common.sh UniMath_CI_BRANCH=master UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git +UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath -git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} -( cd UniMath && \ +( cd ${UniMath_CI_DIR} && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ make -j ${NJOBS} BUILD_COQ=no ) -- 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') 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-basic-overlay.sh | 103 +++++++++++++++++++++++++++++++++++++++++++++ dev/ci/ci-color.sh | 1 - dev/ci/ci-common.sh | 6 +-- dev/ci/ci-compcert.sh | 2 - dev/ci/ci-coquelicot.sh | 2 - dev/ci/ci-fiat-crypto.sh | 2 - dev/ci/ci-fiat-parsers.sh | 2 - dev/ci/ci-flocq.sh | 2 - dev/ci/ci-geocoq.sh | 2 - dev/ci/ci-hott.sh | 2 - dev/ci/ci-iris-coq.sh | 4 -- dev/ci/ci-math-classes.sh | 4 -- dev/ci/ci-metacoq.sh | 5 --- dev/ci/ci-sf.sh | 3 +- dev/ci/ci-tlc.sh | 2 - dev/ci/ci-unimath.sh | 2 - dev/ci/ci-user-overlay.sh | 22 ++++++++++ 17 files changed, 130 insertions(+), 36 deletions(-) create mode 100644 dev/ci/ci-basic-overlay.sh create mode 100644 dev/ci/ci-user-overlay.sh (limited to 'dev/ci') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 0000000000..da5b425794 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,103 @@ +#!/usr/bin/env bash + +# This is the basic overlay set for repositories in the CI. + +# Maybe we should just use Ruby to have real objects... + +######################################################################## +# MathComp +######################################################################## +: ${mathcomp_CI_BRANCH:=master} +: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} + +######################################################################## +# UniMath +######################################################################## +: ${UniMath_CI_BRANCH:=master} +: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} + +######################################################################## +# Unicoq + Metacoq +######################################################################## +: ${unicoq_CI_BRANCH:=master} +: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} + +: ${metacoq_CI_BRANCH:=master} +: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} + +######################################################################## +# Mathclasses + Corn +######################################################################## +: ${math_classes_CI_BRANCH:=v8.6} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} + +: ${Corn_CI_BRANCH:=v8.6} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} + +######################################################################## +# Iris +######################################################################## +: ${stdpp_CI_BRANCH:=master} +: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} + +: ${Iris_CI_BRANCH:=master} +: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} + +######################################################################## +# HoTT +######################################################################## +: ${HoTT_CI_BRANCH:=mz-8.7} +: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} + +######################################################################## +# GeoCoq +######################################################################## +: ${GeoCoq_CI_BRANCH:=master} +: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} + +######################################################################## +# Flocq +######################################################################## +: ${Flocq_CI_BRANCH:=master} +: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${Coquelicot_CI_BRANCH:=master} +: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${CompCert_CI_BRANCH:=master} +: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} + +######################################################################## +# fiat_parsers +######################################################################## +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} + +######################################################################## +# fiat_crypto +######################################################################## +: ${fiat_crypto_CI_BRANCH:=master} +: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} + +######################################################################## +# CoLoR +######################################################################## +: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} + +######################################################################## +# SF +######################################################################## +: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz} + +######################################################################## +# TLC +######################################################################## +: ${tlc_CI_BRANCH:=master} +: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} + diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index fbcf9be1d6..3f0716511d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,7 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color Color_CI_DIR=${CI_BUILD_DIR}/color svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} 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 diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 111222ac7f..c78ffdc2c0 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -CompCert_CI_BRANCH=master -CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 9dfdb87451..40eff03b78 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Coquelicot_CI_BRANCH=master -Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot install_ssreflect diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 7fc0dae2c0..93d39aab07 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -fiat_crypto_CI_BRANCH=master -fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 0b3312e878..c62aa1d859 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -fiat_parsers_CI_BRANCH=master -fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 30eca7a3e9..ec19bd9939 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Flocq_CI_BRANCH=master -Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git Flocq_CI_DIR=${CI_BUILD_DIR}/flocq git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7b5950c887..4e5aa2687b 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -GeoCoq_CI_BRANCH=master -GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 62733c9452..1bf6e9a872 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -HoTT_CI_BRANCH=mz-8.7 -HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 10f2c2b4bd..eb1d1be078 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -3,12 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -stdpp_CI_BRANCH=master -stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp -Iris_CI_BRANCH=master -Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq install_ssreflect diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index e6a57404fe..beb75773b7 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -3,12 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -math_classes_CI_BRANCH=v8.6 -math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes -Corn_CI_BRANCH=v8.6 -Corn_CI_GITURL=https://github.com/c-corn/corn.git Corn_CI_DIR=${CI_BUILD_DIR}/corn # Setup Math-Classes diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 1ea56af29a..e31691179e 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -3,12 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -unicoq_CI_BRANCH=master -unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq - -metacoq_CI_BRANCH=master -metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq # Setup UniCoq diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index c451bf26a1..7d23ccad97 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,7 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz +# XXX: Needs fixing to properly set the build directory. +wget ${sf_CI_TARURL} tar xvfz sf.tgz ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 415f9b38f9..ce26399378 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -tlc_CI_BRANCH=master -tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git tlc_CI_DIR=${CI_BUILD_DIR}/tlc git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 4c4b4f1ce1..175b82b5f9 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -UniMath_CI_BRANCH=master -UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh new file mode 100644 index 0000000000..0285747432 --- /dev/null +++ b/dev/ci/ci-user-overlay.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash + +# Add user overlays here. You can use some logic to detect if you are +# in your travis branch and conditionally enable the overlay. + +# Some useful Travis variables: +# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables) +# +# - TRAVIS_BRANCH: For builds not triggered by a pull request this is +# the name of the branch currently being built; whereas for builds +# triggered by a pull request this is the name of the branch +# targeted by the pull request (in many cases this will be master). +# +# - TRAVIS_COMMIT: The commit that the current build is testing. +# +# - TRAVIS_PULL_REQUEST: The pull request number if the current job is +# a pull request, “false” if it’s not a pull request. +# +# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request, +# the name of the branch from which the PR originated. "" if the +# current job is a push build. + -- cgit v1.2.3 From becc6ef43a0f838d1f6388e8c7373c13f26082bc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 21 Mar 2017 15:12:27 +0100 Subject: trivial: fix comment --- dev/ci/ci-basic-overlay.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/ci') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index da5b425794..241ec35861 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -68,7 +68,7 @@ : ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} ######################################################################## -# Coquelicot +# CompCert ######################################################################## : ${CompCert_CI_BRANCH:=master} : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} -- 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 ++++++-- dev/ci/ci-iris-coq.sh | 14 +++++++++----- 2 files changed, 15 insertions(+), 7 deletions(-) (limited to 'dev/ci') 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'`" ) } diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index eb1d1be078..262dd6fa01 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -9,14 +9,18 @@ Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq install_ssreflect -# Setup stdpp +# Setup Iris first, as it is needed to compute the dependencies -git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins -( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) +# Setup stdpp +stdpp_CI_GITURL=${IRIS_DEP[1]}.git +stdpp_CI_COMMIT=${IRIS_DEP[2]} -# Setup Iris +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} -git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) +# Build iris now ( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) -- cgit v1.2.3 From f29e577ef81e608cb8b3a68f4e171716c1280711 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 20 Mar 2017 13:38:14 +0100 Subject: [travis] Add VST --- dev/ci/ci-basic-overlay.sh | 9 +++++++++ dev/ci/ci-vst.sh | 13 +++++++++++++ 2 files changed, 22 insertions(+) create mode 100755 dev/ci/ci-vst.sh (limited to 'dev/ci') diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 241ec35861..336ce9d8f1 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,11 @@ ######################################################################## # HoTT ######################################################################## +# Temporal overlay : ${HoTT_CI_BRANCH:=mz-8.7} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} +# : ${HoTT_CI_BRANCH:=master} +# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## # GeoCoq @@ -73,6 +76,12 @@ : ${CompCert_CI_BRANCH:=master} : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} +######################################################################## +# VST +######################################################################## +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} + ######################################################################## # fiat_parsers ######################################################################## diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 0000000000..c111951852 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +VST_CI_DIR=${CI_BUILD_DIR}/VST + +# opam install -j ${NJOBS} -y menhir +git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} + +# Targets are: msl veric floyd +# Patch to avoid the upper version limit +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) -- cgit v1.2.3