diff options
Diffstat (limited to 'dev/tools')
| -rwxr-xr-x | dev/tools/backport-pr.sh | 10 | ||||
| -rw-r--r-- | dev/tools/coqdev.el | 12 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 65 | ||||
| -rwxr-xr-x | dev/tools/pre-commit | 12 |
4 files changed, 73 insertions, 26 deletions
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index e4359f7038..5205350a61 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -27,9 +27,9 @@ BRANCH=backport-pr-${PRNUM} RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../') MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/') -if git checkout -b ${BRANCH}; then +if git checkout -b "${BRANCH}"; then - if ! git cherry-pick -x ${RANGE}; then + if ! git cherry-pick -x "${RANGE}"; then echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -50,7 +50,7 @@ else fi -if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then +if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then echo read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r echo @@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi -git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" -git branch -d ${BRANCH} +git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}" +git branch -d "${BRANCH}" # To-Do: # - Support for backporting a PR before it is merged diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 62fdaec802..9dd12087a6 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -103,5 +103,17 @@ Note that this function is executed before _Coqproject is read if it exists." 2 (3 . 4) (5 . 6))) (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) +(defvar bug-reference-bug-regexp) +(defvar bug-reference-url-format) +(defun coqdev-setup-bug-reference-mode () + "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq. + +This does not enable `bug-reference-mode'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)") + (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) + (provide 'coqdev) ;;; coqdev ends here diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 2f6f1af541..00d04e6b3d 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -4,11 +4,20 @@ set -e set -o pipefail API=https://api.github.com/repos/coq/coq -OFFICIAL_REMOTE_URL="git@github.com:coq/coq" +OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq" +OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" -# This script depends (at least) on git and jq. +# This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ +# Set SLOW_CONF to have the confirmation output wait for a newline +# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ +if [ -z ${SLOW_CONF+x} ]; then + QUICK_CONF="-n 1" +else + QUICK_CONF="" +fi + RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" @@ -32,7 +41,7 @@ fi } ask_confirmation() { - read -p "Continue anyway? [y/N] " -n 1 -r + read -p "Continue anyway? [y/N] " $QUICK_CONF -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -61,10 +70,12 @@ fi # Fetching PR metadata -TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title') +PRDATA=$(curl -s "$API/pulls/$PR") + +TITLE=$(echo "$PRDATA" | jq -r '.title') info "title for PR $PR is ${BLUE}$TITLE" -BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') +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) @@ -77,11 +88,15 @@ if [ -z "$REMOTE" ]; then 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 +REMOTE_URL=$(git remote get-url "$REMOTE" --all) +if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ + [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \ + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_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_URL" + error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" ask_confirmation fi @@ -105,19 +120,39 @@ if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then ask_confirmation fi; +# Sanity check: the local branch is up-to-date with upstream + +LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD) +UPSTREAM_COMMIT=$(git rev-parse @{u}) +if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then + + # Is it just that the upstream branch is behind? + # It could just be that we merged other PRs and we didn't push yet + + 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." + ask_confirmation + else + error "Local branch is not up-to-date with ${REMOTE}." + error "Pull before merging." + ask_confirmation + fi +fi + # Sanity check: CI failed -STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') +STATUS=$(curl -s "$API/commits/$COMMIT/status") -if [ "$STATUS" != "success" ]; then - error "CI unsuccessful on ${BLUE}$(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=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') +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 @@ -125,7 +160,7 @@ fi # Sanity check: has milestone -MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title') +MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title') if [ "$MILESTONE" = "null" ]; then error "no milestone set, please set one" ask_confirmation @@ -133,7 +168,7 @@ fi # Sanity check: has kind -KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)') +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 diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index a514b8866a..ad2f2f93e7 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -14,9 +14,9 @@ then # We fix whitespace in the index and in the working tree # separately to preserve non-added changes. - index=$(mktemp "git-fix-ws-index.XXXXX") - fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX") - tree=$(mktemp "git-fix-ws-tree.XXXXX") + index=$(mktemp "git-fix-ws-index.XXXXXX") + fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") + tree=$(mktemp "git-fix-ws-tree.XXXXXX") 1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." 1>&2 echo "If an error destroys your changes you can recover using them." 1>&2 echo "(The files are cleaned up on success.)" @@ -27,8 +27,8 @@ then # reset work tree and index # NB: untracked files which were not added are untouched - git apply --cached -R "$index" - git apply -R "$tree" + git apply --whitespace=nowarn --cached -R "$index" + git apply --whitespace=nowarn -R "$tree" # Fix index # For end of file newlines we must go through the worktree @@ -45,7 +45,7 @@ then # making git fail. Don't fail now: we fix the worktree first. if [ -s "$fixed_index" ] then - git apply -R "$fixed_index" + git apply --whitespace=nowarn -R "$fixed_index" fi # Fix worktree |