Skip to content

Maintainer merge #143045

Maintainer merge

Maintainer merge #143045

name: Maintainer merge
# triggers the action when
on:
# the PR receives a comment
issue_comment:
types: [created, edited]
# 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, edited]
jobs:
ping_zulip:
# 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 }}
PR_AUTHOR: ${{ github.event.issue.user.login }}${{ github.event.pull_request.user.login }}
PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
COMMENT_EVENT: ${{ github.event.comment.body }}
COMMENT_REVIEW: ${{ github.event.review.body }}
PR_TITLE_ISSUE: ${{ github.event.issue.title }}
PR_TITLE_PR: ${{ github.event.pull_request.title }}
PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
EVENT_NAME: ${{ github.event_name }}
name: Ping maintainers on Zulip
runs-on: ubuntu-latest
if: github.repository == 'leanprover-community/mathlib4'
steps:
- name: Find maintainer merge/delegate
id: merge_or_delegate
run: |
echo "PR author: ${PR_AUTHOR}"
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}" |
# captures `maintainer merge/delegate` as well as an optional `?`, ignoring subsequent spaces
sed -n 's=^maintainer *\(merge\|delegate\)\(?\?\) *$=\1\2=p' | head -1)"
printf $'"maintainer delegate" or "maintainer merge" found? \'%s\'\n' "${m_or_d}"
printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"
# write an artifact with all data needed below if we don't have access to necessary secrets
if [[ -z '${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }}' ]]
then
printf 'No access to secrets, writing to file.\n'
jq -n \
--arg author "${AUTHOR}" \
--arg pr_author "${PR_AUTHOR}" \
--arg pr_number "${PR_NUMBER}" \
--arg comment "${COMMENT}" \
--arg pr_title "${PR_TITLE_ISSUE}${PR_TITLE_PR}" \
--arg pr_url "${PR_URL}" \
--arg event_name "${EVENT_NAME}" \
--arg m_or_d "${m_or_d}" \
'{
author: $author,
pr_author: $pr_author,
pr_number: $pr_number,
comment: $comment,
pr_title: $pr_title,
pr_url: $pr_url,
event_name: $event_name,
m_or_d: $m_or_d,
}' > artifact-data.json
echo "Generated JSON artifact:"
cat artifact-data.json
printf 'secrets=' >> "${GITHUB_OUTPUT}"
exit 0
else
printf 'secrets=true\n' >> "${GITHUB_OUTPUT}"
fi
# upload artifact if we have no access to secrets
- if: ${{ steps.merge_or_delegate.outputs.secrets == '' && ! steps.merge_or_delegate.outputs.mOrD == '' }}
name: Upload artifact
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
with:
name: workflow-data
path: artifact-data.json
retention-days: 5
# Run the following steps only if we have access to secrets / write perms on GITHUB_TOKEN
- if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' && ! steps.merge_or_delegate.outputs.mOrD == '' }}
name: Check whether user is part of mathlib-reviewers team
uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
id: actorTeams
with:
organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
# Organization to get membership from.
team: 'mathlib-reviewers'
username: ${{ env.AUTHOR }}
GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
- name: Checkout
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
with:
ref: master
sparse-checkout: |
scripts/get_tlabel.py
scripts/maintainer_merge_message.py
- name: Determine Zulip topic
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
id: determine_topic
run: |
./scripts/get_tlabel.sh "/repos/leanprover-community/mathlib4/issues/${PR_NUMBER}" >> "$GITHUB_OUTPUT"
env:
GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
- name: Form the message
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
id: form_the_message
run: |
# for debugging, we print the available variables
echo "github.event.action: '${{ github.event.action }}'"
echo ""
message="$(
./scripts/maintainer_merge_message.sh "${AUTHOR}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE_ISSUE}${PR_TITLE_PR}" "${COMMENT_EVENT}${COMMENT_REVIEW}" "${PR_AUTHOR}"
)"
printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
- name: Send message on Zulip
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
with:
api-key: ${{ secrets.ZULIP_API_KEY }}
email: 'github-mathlib4-bot@leanprover.zulipchat.com'
organization-url: 'https://leanprover.zulipchat.com'
to: 'mathlib reviewers'
type: 'stream'
topic: ${{ steps.determine_topic.outputs.topic }}
content: ${{ steps.form_the_message.outputs.title }}
- name: Add comment to PR
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
with:
# if a comment triggers the action, then `issue.number` is set
# if a review or review comment triggers the action, then `pull_request.number` is set
issue-number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
body: |
🚀 Pull request has been placed on the maintainer queue by ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}.
- name: Add label to PR
if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }}
uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
with:
# labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
github-token: ${{secrets.TRIAGE_TOKEN}}
script: |
const { owner, repo, number: issue_number } = context.issue;
await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });