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(-) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a6601e04..087572e47 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 d4023c916..d4d503278 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 4a23e51be..94bd5e468 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 c594f8360..c669195dd 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 b9cf649a1..345924e40 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 589a826e0..ce870e52b 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 8f82ba9f2..aaffc9d48 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 e97e2c19e..c21af976f 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 9127c1895..4450dc071 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 b83379241..2eb150cb5 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 9a9bd3648..91a33695b 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 2161a1146..b94632492 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