From 1b0d67a0cf1b725715e97ba6448c3ff0154813bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 21 Mar 2017 17:17:28 +0100 Subject: [travis] [8.6.only] Backport latest changes from trunk. --- .travis.yml | 4 ++ Makefile.ci | 2 +- dev/ci/ci-basic-overlay.sh | 103 +++++++++++++++++++++++++++++++++++++++++++++ dev/ci/ci-color.sh | 8 ++-- dev/ci/ci-common.sh | 34 ++++++++++----- dev/ci/ci-compcert.sh | 9 ++-- dev/ci/ci-coquelicot.sh | 10 ++--- dev/ci/ci-cpdt.sh | 2 +- dev/ci/ci-fiat-crypto.sh | 9 ++-- dev/ci/ci-fiat-parsers.sh | 10 +++++ dev/ci/ci-flocq.sh | 9 ++-- dev/ci/ci-geocoq.sh | 10 ++--- dev/ci/ci-hott.sh | 8 ++-- dev/ci/ci-iris-coq.sh | 24 ++++++++--- dev/ci/ci-math-classes.sh | 20 ++++++--- dev/ci/ci-math-comp.sh | 8 ++-- dev/ci/ci-metacoq.sh | 17 +++++--- dev/ci/ci-sf.sh | 5 ++- dev/ci/ci-template.sh | 12 ++++++ dev/ci/ci-tlc.sh | 8 ++-- dev/ci/ci-unimath.sh | 9 ++-- dev/ci/ci-user-overlay.sh | 22 ++++++++++ 22 files changed, 268 insertions(+), 75 deletions(-) create mode 100644 dev/ci/ci-basic-overlay.sh create mode 100755 dev/ci/ci-fiat-parsers.sh create mode 100755 dev/ci/ci-template.sh create mode 100644 dev/ci/ci-user-overlay.sh diff --git a/.travis.yml b/.travis.yml index f609852bc..7138d5c61 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,4 +1,7 @@ dist: trusty +# Travis builds are slower using sudo: false (the container-based +# infrastructure) as of March 2017; see +# https://github.com/coq/coq/pull/467 for some discussion. sudo: required # Until Ocaml becomes a language, we set a known one. language: c @@ -29,6 +32,7 @@ env: - TEST_TARGET="ci-coquelicot" - TEST_TARGET="ci-geocoq" - TEST_TARGET="ci-fiat-crypto" + - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" diff --git a/Makefile.ci b/Makefile.ci index e4b5832f6..897318c4d 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,5 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ - ci-color ci-math-classes ci-tlc ci-fiat-crypto \ + ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ ci-unimath diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 000000000..241ec3586 --- /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} + +######################################################################## +# CompCert +######################################################################## +: ${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 78ae7f02f..3f0716511 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash 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_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-common.sh b/dev/ci/ci-common.sh index 412da626f..9fdd2504d 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 @@ -8,20 +8,34 @@ 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 +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci -# git_checkout branch +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 +# in (if it does not exist already) and checkout the +# remote branch from 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'`" ) + # Allow an optional 4th argument for the commit + local _COMMIT=${4:-FETCH_HEAD} + local _DEPTH=${5:-1} + + mkdir -p ${_DEST} + ( cd ${_DEST} && \ + if [ ! -d .git ] ; then git clone --depth ${_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() @@ -34,8 +48,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 && \ diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index ec09389f8..c78ffdc2c 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,13 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash 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 -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 94bd5e468..40eff03b7 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +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-cpdt.sh b/dev/ci/ci-cpdt.sh index 18d756180..0e791ebbf 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 c669195dd..93d39aab0 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/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_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 new file mode 100755 index 000000000..c62aa1d85 --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} + +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 345924e40..ec19bd993 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/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_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 29667b018..4e5aa2687 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,15 +1,13 @@ -#!/bin/bash +#!/usr/bin/env bash 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 0c07564c0..1bf6e9a87 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT +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 c21af976f..dcb46ed2a 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,17 +1,27 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp + +Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq + install_ssreflect +# Setup Iris first, as it is needed to compute the dependencies + +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} +read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins + # Setup stdpp -git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp +stdpp_CI_GITURL=${IRIS_DEP[1]}.git +stdpp_CI_COMMIT=${IRIS_DEP[2]} +stdpp_CI_DEPTH="1000" -( cd coq-stdpp && make -j ${NJOBS} && make install ) +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} ${stdpp_CI_DEPTH} -# Setup Iris -git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) -( cd iris-coq && make -j ${NJOBS} ) +# Build iris now +( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4450dc071..beb75773b 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,12 +1,20 @@ -#!/bin/bash +#!/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_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_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 2eb150cb5..bb8188da4 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,13 +1,15 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... 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 91a33695b..e31691179 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,16 +1,19 @@ -#!/bin/bash +#!/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_DIR=${CI_BUILD_DIR}/unicoq +metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq -git_checkout master https://github.com/unicoq/unicoq.git unicoq +# Setup UniCoq -( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} -git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) +# 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-sf.sh b/dev/ci/ci-sf.sh index 5e41211f1..7d23ccad9 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash 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-template.sh b/dev/ci/ci-template.sh new file mode 100755 index 000000000..700105aed --- /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 b94632492..ce2639937 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc +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 15e619acb..175b82b5f 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,13 @@ -#!/bin/bash +#!/usr/bin/env bash 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 +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 ) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh new file mode 100644 index 000000000..028574743 --- /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