Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176#!/usr/bin/env bash
if [ -z "${CI_QUIET}" ];then set -xfiset -e
# default value for NJOBS: "${NJOBS:=1}"export NJOBS
. "$(dirname "${BASH_SOURCE[0]}")/../ci-env.sh"
# Where we download and build external developmentsCI_BUILD_DIR="$PWD/_build_ci"
declare -A overlays
# overlay <project> <giturl> <ref> <prnumber> [<prbranch>]# creates an overlay for project using a given url and branch which is# active for prnumber or prbranch. prbranch defaults to ref.function overlay(){ local project=$1 local ov_url=$2 local ov_ref=$3 local ov_prnumber=$4 local ov_prbranch=$5 : "${ov_prbranch:=$ov_ref}"
if [ "$CI_PULL_REQUEST" = "$ov_prnumber" ] || [ "$CI_BRANCH" = "$ov_prbranch" ]; then if ! is_in_projects "$project"; then echo "Error: $1 is not a known project which can be overlayed" exit 1 fi
overlays[${project}_URL]=$ov_url overlays[${project}_REF]=$ov_ref fi}
set +x. "$(dirname "${BASH_SOURCE[0]}")/../ci-basic-overlay.sh"
for overlay in "$(dirname "${BASH_SOURCE[0]}")"/../user-overlays/*.sh; do # shellcheck source=/dev/null # the directoy can be empty if [ -e "${overlay}" ]; then . "${overlay}"; fidone
if [ -z "${CI_QUIET}" ];then set -xfi
# [git_download <project> [<destination>]] will download <project> and# unpack it in <destination> (if given; default:# $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 there is an overlay, $WITH_SUBMODULES is set to 1 or $CI# is unset or empty (local build), it uses git clone to perform the# download.git_download(){ local project=$1 local dest="${2:-$CI_BUILD_DIR/$project}"
local giturl_var="${project}_CI_GITURL" local giturl="${!giturl_var}" local ref_var="${project}_CI_REF" local ref="${!ref_var}" local parent_project_var="${project}_CI_PARENT_PROJECT" local parent_project="${!parent_project_var}" local submodule_folder_var="${project}_CI_SUBMODULE_FOLDER" local submodule_folder="${!submodule_folder_var}"
local ov_url=${overlays[${project}_URL]} local ov_ref=${overlays[${project}_REF]}
local dest_prefix="$(dirname "$dest")/" if [ "${CI}${USE_CI_DIRECTORY_STRUCTURE}" = "" ]; then # we can reuse the parent project download when not on CI local parent_project_dest="$CI_BUILD_DIR/$parent_project" # we use relative symlinks so they are relocatable local parent_project_relative_dest="${parent_project_dest#$dest_prefix}" else # on CI, we need to ensure that there's no overlap in directory tree # between sibling jobs, since otherwise they will scribble over # each others .v timestamps and result in duplicated builds local parent_project_dest="${dest}-PARENT-${parent_project}" # we use relative symlinks so they are relocatable local parent_project_relative_dest="${parent_project_dest#$dest_prefix}" fi
if [ -d "$dest" ]; then echo "Warning: download and unpacking of $project skipped because $dest already exists." elif [[ $ov_url ]] || [ "$WITH_SUBMODULES" = "1" ] || [ "$CI" = "" ] || [ -n "${parent_project}" ]; then if [ -n "${parent_project}" ]; then # if there is a parent project, we first download the parent # project then symlink the submodule_folder to dest; this allows # project CI scripts to be transparent w.r.t. whether or not the # project is cloned from a submodule / submodule_folder. if [ ! -d "${parent_project_dest}" ]; then WITH_SUBMODULES=1 git_download "${parent_project}" "${parent_project_dest}" fi # now we can create the symlinks ln -s "${parent_project_relative_dest}/${submodule_folder}" "$dest" pushd "$dest" ref="$(git rev-parse HEAD)" else # if $ref isn't a branch (eg it's a commit hash or a tag) git clone -b will fail # in that case do a full git clone git clone "$giturl" "$dest" -b "$ref" --depth 10 || git clone "$giturl" "$dest" pushd "$dest" git checkout "$ref" fi git log -n 1 if [[ $ov_url ]]; then # In CI we merge into the upstream branch to stay synchronized # Locally checkout the overlay and rebase on upstream # We act differently because merging is what will happen when the PR is merged # but rebasing produces something that is nicer to edit if [[ $CI ]]; then git -c pull.rebase=false -c user.email=nobody@example.invalid -c user.name=Nobody \ pull --no-edit --no-ff "$ov_url" "$ov_ref" git log -n 1 HEAD^2 || true # no merge commit if the overlay was merged upstream git log -n 1 else git remote add -t "$ov_ref" -f overlay "$ov_url" git checkout -b "$ov_ref" overlay/"$ov_ref" git rebase "$ref" git log -n 1 fi fi if [ "$WITH_SUBMODULES" = 1 ]; then git submodule update --init --recursive --depth 10 fi popd else # When possible, we download tarballs to reduce bandwidth and latency local archiveurl_var="${project}_CI_ARCHIVEURL" local archiveurl="${!archiveurl_var}" mkdir -p "$dest" pushd "$dest" local commit commit=$(git ls-remote --head "$giturl" "refs/heads/$ref" | cut -f 1) if [[ "$commit" == "" ]]; then # $ref must have been a tag or hash, not a branch commit="$ref" fi wget "$archiveurl/$commit.tar.gz" tar xfz "$commit.tar.gz" --strip-components=1 rm -f "$commit.tar.gz" popd 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}
# run make -k; make again if it failed so that the failing file comes last# makes it easier to find the error messages in the CI logfunction make_full() { if ! make -k "$@"; then make -k "$@"; exit 1; fi}