From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- dev/ci/ci-common.sh | 123 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 dev/ci/ci-common.sh (limited to 'dev/ci/ci-common.sh') diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh new file mode 100644 index 00000000..6fc4293d --- /dev/null +++ b/dev/ci/ci-common.sh @@ -0,0 +1,123 @@ +#!/usr/bin/env bash + +set -xe + +# default value for NJOBS +: "${NJOBS:=1}" +export NJOBS + +if [ -n "${GITLAB_CI}" ]; +then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" + export COQBIN="$PWD/_install_ci/bin" + export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi +else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + else # assume local + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH + fi + export OCAMLPATH="$PWD:$OCAMLPATH" + 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 download and build external developments +CI_BUILD_DIR="$PWD/_build_ci" + +for overlay in "${ci_dir}"/user-overlays/*.sh; do + # shellcheck source=/dev/null + . "${overlay}" +done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" + +# [git_download project] will download [project] and unpack it +# in [$CI_BUILD_DIR/project] if the folder does not exist already; +# if it does, it will do nothing except print a warning (this can be +# useful when building locally). +# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty +# (local build), it uses git clone to perform the download. +git_download() +{ + local PROJECT=$1 + local DEST="$CI_BUILD_DIR/$PROJECT" + + if [ -d "$DEST" ]; then + echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." + elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + git clone "$GITURL" "$DEST" + cd "$DEST" + git checkout "$REF" + else # When possible, we download tarballs to reduce bandwidth and latency + local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" + local ARCHIVEURL="${!ARCHIVEURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + mkdir -p "$DEST" + cd "$DEST" + wget "$ARCHIVEURL/$REF.tar.gz" + tar xvfz "$REF.tar.gz" --strip-components=1 + rm -f "$REF.tar.gz" + fi +} + +make() +{ + # +x: add x only if defined + if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; + then + # Not submake and parallel make requested + command make -j "$NJOBS" "$@" + else + command make "$@" + fi +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq ssreflect/all_ssreflect.vo && \ + make -f Makefile.coq install ) + + echo -en 'travis_fold:end:ssr.install\\r' + +} + +# this installs just the ssreflect + algebra library of math-comp +install_ssralg() +{ + echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + + git_download mathcomp + + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ + make Makefile.coq && \ + make -f Makefile.coq algebra/all_algebra.vo && \ + make -f Makefile.coq install ) + + echo -en 'travis_fold:end:ssralg.install\\r' + +} -- cgit v1.2.3