Skip to content

Add "ready-to-merge" and "delegated" label #803

Add "ready-to-merge" and "delegated" label

Add "ready-to-merge" and "delegated" label #803

name: Add "ready-to-merge" and "delegated" label
# triggers the action when
on:
# the PR receives a comment
issue_comment:
types: [created]
# the PR receives a review
pull_request_review:
# whether or not it is accompanied by a comment
types: [submitted]
# the PR receives a review comment
pull_request_review_comment:
types: [created]
jobs:
add_ready_to_merge_label:
# we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not
# both set simultaneously: depending on the event that triggers the PR, usually only one is set
env:
AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
COMMENT_EVENT: ${{ github.event.comment.body }}
COMMENT_REVIEW: ${{ github.event.review.body }}
name: Add ready-to-merge or delegated label
runs-on: ubuntu-latest
steps:
- name: Find bors merge/delegate
id: merge_or_delegate
run: |
COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}"
# we strip `\r` since line endings from GitHub contain this character
COMMENT="${COMMENT//$'\r'/}"
# for debugging, we print some information
printf '%s' "${COMMENT}" | hexdump -cC
printf 'Comment:"%s"\n' "${COMMENT}"
m_or_d="$(printf '%s' "${COMMENT}" |
sed -n 's=^bors *\(merge\|r+\) *$=ready-to-merge=p; s=^bors *d.*=delegated=p' | head -1)"
printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
[ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
then
printf $'bot=true\n'
printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
else
printf $'bot=false\n'
printf $'bot=false\n' >> "${GITHUB_OUTPUT}"
fi
- name: Check whether user is a mathlib admin
id: user_permission
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
uses: actions-cool/check-user-permission@v2
with:
require: 'admin'
- name: Add ready-to-merge or delegated label
id: add_label
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
( steps.user_permission.outputs.require-result == 'true' ||
steps.merge_or_delegate.outputs.bot == 'true' ) }}
uses: octokit/[email protected]
with:
route: POST /repos/:repository/issues/:issue_number/labels
repository: ${{ github.repository }}
issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
env:
GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
- if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
( steps.user_permission.outputs.require-result == 'true' ||
steps.merge_or_delegate.outputs.bot == 'true' ) }}
id: remove_labels
name: Remove "awaiting-author"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
run: |
curl --request DELETE \
--url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
--header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
# comment uses ${{ secrets.GITHUB_TOKEN }}