diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/change-header | 1 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 31 | ||||
| -rwxr-xr-x | dev/tools/pin-ci.sh | 46 |
3 files changed, 63 insertions, 15 deletions
diff --git a/dev/tools/change-header b/dev/tools/change-header index 59c6f43958..3b0a9d1ef9 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -43,6 +43,7 @@ for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do mv $i.tmp$$ $i modified=$(expr $modified + 1) else + echo "$i: header unchanged" kept=$(expr $kept + 1) fi rm $i.head.tmp$$ diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..ce64aebdc7 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -22,7 +22,6 @@ fi RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" -BLUE="\033[34m" YELLOW="\033[33m" info() { echo -e "${GREEN}info:${RESET} $1 ${RESET}" @@ -74,17 +73,17 @@ fi PRDATA=$(curl -s "$API/pulls/$PR") TITLE=$(echo "$PRDATA" | jq -r '.title') -info "title for PR $PR is ${BLUE}$TITLE" +info "title for PR $PR is $TITLE" BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label') -info "PR $PR targets branch ${BLUE}$BASE_BRANCH" +info "PR $PR targets branch $BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) -info "you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" +info "you are merging in $CURRENT_LOCAL_BRANCH" REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") if [ -z "$REMOTE" ]; then - error "branch ${BLUE}$CURRENT_LOCAL_BRANCH${RESET} has not associated remote" + error "branch $CURRENT_LOCAL_BRANCH has not associated remote" error "don't know where to fetch the PR from" error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH" exit 1 @@ -96,12 +95,12 @@ if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then - error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" - error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" - error "it points to ${BLUE}$REMOTE_URL${RESET} instead" + error "remote $REMOTE does not point to the official Coq repo" + error "that is $OFFICIAL_REMOTE_GIT_URL" + error "it points to $REMOTE_URL instead" ask_confirmation fi -info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE" +info "remote for $CURRENT_LOCAL_BRANCH is $REMOTE" info "fetching from $REMOTE the PR" git remote update "$REMOTE" @@ -112,12 +111,12 @@ if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then fi git fetch "$REMOTE" "refs/pull/$PR/head" COMMIT=$(git rev-parse FETCH_HEAD) -info "commit for PR $PR is ${BLUE}$COMMIT" +info "commit for PR $PR is $COMMIT" # Sanity check: merge to a different branch if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then - error "PR requests merge in ${BLUE}$BASE_BRANCH${RESET} but you are merging in ${BLUE}$CURRENT_LOCAL_BRANCH" + error "PR requests merge in $BASE_BRANCH but you are merging in $CURRENT_LOCAL_BRANCH" ask_confirmation fi; @@ -132,12 +131,14 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then warning "Your branch is ahead of ${REMOTE}." - warning "You should see this warning only if you've just merged another PR and did not push yet." + warning "On master, GitHub's branch protection rule prevents merging several PRs at once." + warning "You should run [git push ${REMOTE}] between each call to the merge script." ask_confirmation else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi @@ -164,7 +165,7 @@ fi STATUS=$(curl -s "$API/commits/$COMMIT/status") if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then - error "CI unsuccessful on ${BLUE}$(echo "$STATUS" | + error "CI unsuccessful on $(echo "$STATUS" | jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" ask_confirmation fi; @@ -173,7 +174,7 @@ fi; NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') if [ "$NEEDS_LABELS" != "[]" ]; then - error "needs:something labels still present: ${BLUE}$NEEDS_LABELS" + error "needs:something labels still present: $NEEDS_LABELS" ask_confirmation fi diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh new file mode 100755 index 0000000000..dbf54d7f0a --- /dev/null +++ b/dev/tools/pin-ci.sh @@ -0,0 +1,46 @@ +#!/usr/bin/env bash + +# Use this script to pin the commit used by the developments tracked by the CI + +OVERLAYS="./dev/ci/ci-basic-overlay.sh" + +process_development() { + local DEV=$1 + local REPO_VAR="${DEV}_CI_GITURL" + local REPO=${!REPO_VAR} + local BRANCH_VAR="${DEV}_CI_REF" + local BRANCH=${!BRANCH_VAR} + if [[ -z "$BRANCH" ]] + then + echo "$DEV has no branch set, skipping" + return 0 + fi + if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]] + then + echo "$DEV is already set to hash $BRANCH, skipping" + return 0 + fi + echo "Resolving $DEV as $BRANCH from $REPO" + local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1) + if [[ -z "$HASH" ]] + then + echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping" + return 0 + fi + read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; then + # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022 + sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS + fi +} + +# Execute the script to set the overlay variables +. $OVERLAYS + +# Find all variables declared in the base overlay of the form *_CI_GITURL +for REPO_VAR in $(compgen -A variable | grep _CI_GITURL) +do + DEV=${REPO_VAR%_CI_GITURL} + process_development $DEV +done |