diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/MERGING.md | 78 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 159 |
2 files changed, 211 insertions, 26 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md new file mode 100644 index 0000000000..71fc396088 --- /dev/null +++ b/dev/doc/MERGING.md @@ -0,0 +1,78 @@ +# Merging changes in Coq + +This document describes how patches (submitted as Pull Requests) should be +merged into the main repository (https://github.com/coq/coq). + +## Code owners + +The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the +system, two owners. One is the principal maintainer of the component, the other +is the secondary maintainer. + +When a pull request is submitted, GitHub will automatically ask the principal +maintainer for a review. If the pull request touches several parts, all the +corresponding principal maintainers will be asked for a review. + +Maintainers are never assigned as reviewer on their own PRs. + +If a principal maintainer submits a PR that changes the component they own, they +must assign the secondary maintainer as reviewer. They should also do it if they +know they are not available to do the review. + +## Reviewing + +When maintainers receive a review request, they are expected to: + +* Put their name in the assignee field, if they are in charge of the component + that is the main target of the patch (or if they are the only maintainer asked + to review the PR). +* Review the PR, approve it or request changes. +* If they are the assignee, check if all reviewers approved the PR. If not, + regularly ping the author (if changes should be implemented) or the reviewers + (if reviews are missing). The assignee ensures that any requests for more + discussion have been granted. When the discussion has converged and ALL + REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging + process described below. + +In all cases, maintainers can delegate reviews to the other maintainer of the +same component, except if it would lead to a maintainer reviewing their own +patch. + +A maintainer is expected to be reasonably reactive, but no specific timeframe is +given for reviewing. + +(*) In case a component is touched in a trivial way (adding/removing one file in +a `Makefile`, etc), or by applying a systematic process (global renaming, +deprecationg propagation, etc) that has been reviewed globally, the assignee can +say in a comment they think a review is not required and proceed with the merge. + +## Merging + +Once all reviewers approved the PR, the assignee is expected to check that CI +completed without relevant failures, and that the PR comes with appropriate +documentation and test cases. If not, they should leave a comment on the PR and +put the approriate label. Otherwise, they are expected to merge the PR using the +[merge script](/dev/tools/merge-pr.sh). + +When the PR has conflicts, the assignee can either: +- ask the author to rebase the branch, fixing the conflicts +- warn the author that they are going to rebase the branch, and push to the + branch directly + +In both cases, CI should be run again. + +In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix +the conflicts in the merge commit (following the same steps as below), and push +to `master` directly. Don't use the GitHub interface to fix these conflicts. + +The command to be used is: +``` +$ dev/tools/merge-pr XXXX +``` +where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. + +Maintainers MUST NOT merge their own patches. + +DON'T USE the GitHub interface for merging, since it will prevent the automated +backport script from operating properly, generates bad commit messages, and a +messy history when there are conflicts. diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 9f24960fff..2f6f1af541 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -1,50 +1,157 @@ #!/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/ -#TODO: check arguments and show usage if relevant +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}" +} -PR=$1 +check_util() { +if ! command -v "$1" > /dev/null 2>&1; then + error "this script requires the $1 command line utility" + exit 1 +fi +} -CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) -REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") -git fetch "$REMOTE" "refs/pull/$PR/head" +ask_confirmation() { + read -p "Continue anyway? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]] + then + exit 1 + fi +} -API=https://api.github.com/repos/coq/coq +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 + +TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title') +info "title for PR $PR is ${BLUE}$TITLE" BASE_BRANCH=$(curl -s "$API/pulls/$PR" | 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" -a \ + "$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) -STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') +info "commit for PR $PR is ${BLUE}$COMMIT" + +# Sanity check: merge to a different branch if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then - echo "Wrong base branch" - read -p "Bypass? [y/N] " -n 1 -r - echo - if [[ ! $REPLY =~ ^[Yy]$ ]] - then - exit 1 - fi + 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" | jq -r '.state') + if [ "$STATUS" != "success" ]; then - echo "CI status is \"$STATUS\"" - read -p "Bypass? [y/N] " -n 1 -r - echo - if [[ ! $REPLY =~ ^[Yy]$ ]] - then - exit 1 - fi + error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" | + jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" + ask_confirmation fi; -git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e +# Sanity check: has labels named "needs:" + +NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | 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=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title') +if [ "$MILESTONE" = "null" ]; then + error "no milestone set, please set one" + ask_confirmation +fi + +# Sanity check: has kind + +KIND=$(curl -s "$API/pulls/$PR" | 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; then - echo "******************************************" - echo "** WARNING: does this PR have overlays? **" - echo "******************************************" +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 |