aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/merge-pr.sh
blob: 20612eeb8538cf821fbeb9ea1d082717ccb96657 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
#!/usr/bin/env bash

set -e
set -o pipefail

API=https://api.github.com/repos/coq/coq
OFFICIAL_REMOTE_URL="git@github.com:coq/coq"

# This script depends (at least) on git and jq.
# It should be used like this: dev/tools/merge-pr.sh /PR number/

RED="\033[31m"
RESET="\033[0m"
GREEN="\033[32m"
BLUE="\033[34m"
YELLOW="\033[33m"
info() {
  echo -e "${GREEN}info:${RESET} $1 ${RESET}"
}
error() {
  echo -e "${RED}error:${RESET} $1 ${RESET}"
}
warning() {
  echo -e "${YELLOW}warning:${RESET} $1 ${RESET}"
}

check_util() {
if ! command -v "$1" > /dev/null 2>&1; then
  error "this script requires the $1 command line utility"
  exit 1
fi
}

ask_confirmation() {
  read -p "Continue anyway? [y/N] " -n 1 -r
  echo
  if [[ ! $REPLY =~ ^[Yy]$ ]]
  then
    exit 1
  fi
}

check_util jq
check_util curl
check_util git
check_util gpg

# command line parsing

if [ $# != 1 ]; then
  error "usage: $0 PR-number"
  exit 1
fi

if [[ "$1" =~ ^[1-9][0-9]*$ ]]; then
  PR=$1
else
  error "$1 is not a number"
  exit 1
fi

# Fetching PR metadata

PRDATA=$(curl -s "$API/pulls/$PR")

TITLE=$(echo "$PRDATA" | jq -r '.title')
info "title for PR $PR is ${BLUE}$TITLE"

BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label')
info "PR $PR targets branch ${BLUE}$BASE_BRANCH"

CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
info "you are merging in ${BLUE}$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 "don't know where to fetch the PR from"
  error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH"
  exit 1
fi
REMOTE_URL=$(git remote get-url "$REMOTE" --push)
if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \
   [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
  error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
  error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
  error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
  ask_confirmation
fi
info "remote for $CURRENT_LOCAL_BRANCH is ${BLUE}$REMOTE"

info "fetching from $REMOTE the PR"
git remote update "$REMOTE"
if ! git ls-remote "$REMOTE" | grep pull >/dev/null; then
  error "remote $REMOTE is not configured to fetch pull requests"
  error "run: git config remote.$REMOTE.fetch +refs/pull/*/head:refs/remotes/$REMOTE/pr/*"
  exit 1
fi
git fetch "$REMOTE" "refs/pull/$PR/head"
COMMIT=$(git rev-parse FETCH_HEAD)
info "commit for PR $PR is ${BLUE}$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"
  ask_confirmation
fi;

# Sanity check: CI failed

STATUS=$(curl -s "$API/commits/$COMMIT/status")

if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then
  error "CI unsuccessful on ${BLUE}$(echo "$STATUS" |
    jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')"
  ask_confirmation
fi;

# Sanity check: has labels named "needs:"

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"
  ask_confirmation
fi

# Sanity check: has milestone

MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title')
if [ "$MILESTONE" = "null" ]; then
  error "no milestone set, please set one"
  ask_confirmation
fi

# Sanity check: has kind

KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)')
if [ "$KIND" = "[]" ]; then
  error "no kind:something label set, please set one"
  ask_confirmation
fi

# Sanity check: user.signingkey
if [ -z "$(git config user.signingkey)" ]; then
  warning "git config user.signingkey is empty"
  warning "gpg will guess a key out of your git config user.* data"
fi

info "merging"
git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e

# TODO: improve this check
if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then
  warning "this PR may have overlays (sorry the check is not perfect)"
  warning "if it has overlays please check the following:"
  warning "- each overlay has a corresponding open PR on the upstream repo"
  warning "- after merging please notify the upstream they can merge the PR"
fi