Maintainer merge (workflow_run) #211360
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Maintainer merge (workflow_run) | |
| # triggers the action when | |
| on: | |
| workflow_run: | |
| workflows: ["Maintainer merge"] | |
| types: | |
| - completed | |
| jobs: | |
| ping_zulip: | |
| name: Ping maintainers on Zulip | |
| runs-on: ubuntu-latest | |
| if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }} | |
| permissions: | |
| actions: read | |
| contents: read | |
| id-token: write | |
| pull-requests: write | |
| steps: | |
| - name: Consume bridge artifact | |
| id: bridge | |
| uses: leanprover-community/privilege-escalation-bridge/consume@ea7d63d1c8ece92a8e89b6a6d8fda40603167a91 # v1.3.0 | |
| with: | |
| artifact: workflow-data | |
| source_workflow: Maintainer merge | |
| require_event: issue_comment,pull_request_review,pull_request_review_comment | |
| fail_on_missing: false | |
| token: ${{ github.token }} | |
| extract: | | |
| author=event.comment.user.login|event.review.user.login | |
| pr_author=event.issue.user.login|event.pull_request.user.login | |
| pr_number=meta.pr_number | |
| comment=event.comment.body|event.review.body | |
| pr_title=event.issue.title|event.pull_request.title | |
| pr_url=event.issue.html_url|event.pull_request.html_url | |
| event_name=meta.event_name | |
| mOrD=outputs.mOrD | |
| - name: Download legacy artifact (fallback) | |
| id: download-legacy-artifact | |
| if: ${{ steps.bridge.outputs.pr_number == '' }} | |
| uses: dawidd6/action-download-artifact@b6e2e70617bc3265edd6dab6c906732b2f1ae151 # v21 | |
| with: | |
| workflow: maintainer_merge.yml | |
| name: workflow-data | |
| path: ./artifacts | |
| if_no_artifact_found: ignore | |
| run_id: ${{ github.event.workflow_run.id }} | |
| - name: Extract legacy artifact data (fallback) | |
| id: legacy | |
| if: ${{ steps.bridge.outputs.pr_number == '' && steps.download-legacy-artifact.outputs.found_artifact == 'true' }} | |
| run: | | |
| data_file="./artifacts/artifact-data.json" | |
| if [ ! -f "${data_file}" ] | |
| then | |
| echo "Legacy artifact not found at ${data_file}." | |
| exit 0 | |
| fi | |
| { | |
| echo "author=$(jq -r '.author // empty' "${data_file}")" | |
| echo "pr_author=$(jq -r '.pr_author // empty' "${data_file}")" | |
| echo "pr_number=$(jq -r '.pr_number // empty' "${data_file}")" | |
| echo "pr_title=$(jq -r '.pr_title // empty' "${data_file}")" | |
| echo "pr_url=$(jq -r '.pr_url // empty' "${data_file}")" | |
| echo "event_name=$(jq -r '.event_name // empty' "${data_file}")" | |
| echo "mOrD=$(jq -r '.mOrD // .m_or_d // empty' "${data_file}")" | |
| } | tee -a "$GITHUB_OUTPUT" | |
| comment="$(jq -r '.comment // empty' "${data_file}")" | |
| printf 'comment<<EOF\n%s\nEOF\n' "${comment}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Select bridge or legacy inputs | |
| id: inputs | |
| if: ${{ steps.bridge.outputs.pr_number != '' || steps.legacy.outputs.pr_number != '' }} | |
| env: | |
| INPUT_AUTHOR: ${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }} | |
| INPUT_PR_AUTHOR: ${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }} | |
| INPUT_PR_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }} | |
| INPUT_PR_TITLE: ${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }} | |
| INPUT_PR_URL: ${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }} | |
| INPUT_EVENT_NAME: ${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }} | |
| INPUT_MORD: ${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }} | |
| INPUT_SOURCE: ${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }} | |
| INPUT_COMMENT: ${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.comment }} | |
| run: | | |
| { | |
| echo "author=${INPUT_AUTHOR}" | |
| echo "pr_author=${INPUT_PR_AUTHOR}" | |
| echo "pr_number=${INPUT_PR_NUMBER}" | |
| echo "pr_title=${INPUT_PR_TITLE}" | |
| echo "pr_url=${INPUT_PR_URL}" | |
| echo "event_name=${INPUT_EVENT_NAME}" | |
| echo "mOrD=${INPUT_MORD}" | |
| echo "input_source=${INPUT_SOURCE}" | |
| } | tee -a "$GITHUB_OUTPUT" | |
| printf 'comment<<EOF\n%s\nEOF\n' "${INPUT_COMMENT}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Note legacy artifact fallback | |
| if: ${{ steps.inputs.outputs.input_source == 'legacy' }} | |
| run: | | |
| echo "::notice::Using legacy workflow-data artifact fallback from maintainer_merge.yml" | |
| echo "Using legacy workflow-data artifact fallback from maintainer_merge.yml" >> "$GITHUB_STEP_SUMMARY" | |
| - if: ${{ ! steps.inputs.outputs.mOrD == '' }} | |
| name: Resolve splice-bot attribution | |
| id: attribution | |
| env: | |
| AUTHOR: ${{ steps.inputs.outputs.author }} | |
| COMMENT: ${{ steps.inputs.outputs.comment }} | |
| run: | | |
| # When mathlib-splicebot[bot] relays a 'maintainer merge/delegate' command | |
| # from a review comment on the original PR, its comment ends with an | |
| # attribution line of the form (see the SPLICEBOT_LABEL_COMMANDS repo variable) | |
| # Requested by @reviewer via splice-bot from #12345. | |
| # so the Zulip report and PR comment credit the requesting reviewer instead | |
| # of the bot. The requester's free text is rendered by SpliceBot as a | |
| # markdown blockquote, so this line-anchored match cannot be forged; we | |
| # additionally only trust the attribution line when the comment author is | |
| # the bot itself. | |
| display_author="${AUTHOR}" | |
| if [ "${AUTHOR}" = "mathlib-splicebot[bot]" ] | |
| then | |
| attributed="$(printf '%s' "${COMMENT}" | tr -d '\r' | | |
| sed -n 's=^Requested by @\([A-Za-z0-9-][A-Za-z0-9-]*\) via splice-bot from #\([0-9][0-9]*\)\.$=\1 (via splice-bot from #\2)=p' | tail -1)" | |
| if [ -n "${attributed}" ] | |
| then | |
| display_author="${attributed}" | |
| fi | |
| fi | |
| echo "display_author=${display_author}" | tee -a "$GITHUB_OUTPUT" | |
| # bot usernames would cause this step to error with "Could not resolve to a User...", | |
| # so we skip it for all bot accounts; allowed bots are validated in the next step | |
| - if: ${{ ! steps.inputs.outputs.mOrD == '' && ! endsWith(steps.inputs.outputs.author, '[bot]') }} | |
| name: Check whether user is part of mathlib-reviewers team | |
| uses: tspascoal/get-user-teams-membership@b2546c5affc730fd8e3d8483ae9ad3621938c2f9 # v4.0.2 | |
| id: actorTeams | |
| with: | |
| organization: leanprover-community # optional. Default value ${{ github.repository_owner }} | |
| # Organization to get membership from. | |
| team: 'mathlib-reviewers' | |
| username: ${{ steps.inputs.outputs.author }} | |
| GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`) | |
| - if: ${{ ! steps.inputs.outputs.mOrD == '' }} | |
| name: Determine whether the author may use the maintainer merge command | |
| id: authorized | |
| env: | |
| AUTHOR: ${{ steps.inputs.outputs.author }} | |
| IS_TEAM_MEMBER: ${{ steps.actorTeams.outputs.isTeamMember }} | |
| run: | | |
| # mathlib-splicebot[bot] posts 'maintainer merge' comments on split PRs | |
| # on behalf of reviewers; SpliceBot's command-level authorization | |
| # (see SPLICEBOT_LABEL_COMMANDS) has already checked that the | |
| # requester is a reviewer or maintainer. | |
| if [ "${IS_TEAM_MEMBER}" = "true" ] || [ "${AUTHOR}" = "mathlib-splicebot[bot]" ] | |
| then | |
| echo "authorized=true" | tee -a "$GITHUB_OUTPUT" | |
| else | |
| echo "authorized=false" | tee -a "$GITHUB_OUTPUT" | |
| fi | |
| - name: Checkout local actions | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| with: | |
| ref: ${{ github.workflow_sha }} | |
| fetch-depth: 1 | |
| sparse-checkout: .github/actions | |
| path: workflow-actions | |
| - name: Get mathlib-ci | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| uses: ./workflow-actions/.github/actions/get-mathlib-ci | |
| - name: Determine Zulip topic | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| id: determine_topic | |
| run: | | |
| "${CI_SCRIPTS_DIR}/maintainer/get_tlabel.sh" "/repos/leanprover-community/mathlib4/issues/${PR_NUMBER}" >> "$GITHUB_OUTPUT" | |
| env: | |
| GH_TOKEN: ${{secrets.GITHUB_TOKEN}} | |
| PR_NUMBER: ${{ steps.inputs.outputs.pr_number }} | |
| - name: Form the message | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| id: form_the_message | |
| run: | | |
| message="$( | |
| "${CI_SCRIPTS_DIR}/maintainer/maintainer_merge_message.sh" "${AUTHOR}" "${{ steps.inputs.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE}" "${COMMENT}" "${PR_AUTHOR}" | |
| )" | |
| trigger_name="${{ steps.inputs.outputs.event_name }}" | |
| trigger_run_url="${{ github.event.workflow_run.html_url }}" | |
| wf_run_url="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| legacy_suffix="" | |
| if [ "${{ steps.inputs.outputs.input_source }}" = "legacy" ] | |
| then | |
| legacy_suffix=" (legacy)" | |
| fi | |
| metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}" | |
| echo "${metadata}" | |
| # message="${message}"$'\n\n---\n'"${metadata}" | |
| printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT" | |
| env: | |
| AUTHOR: ${{ steps.attribution.outputs.display_author }} | |
| EVENT_NAME: ${{ steps.inputs.outputs.event_name }} | |
| PR_NUMBER: ${{ steps.inputs.outputs.pr_number }} | |
| PR_URL: ${{ steps.inputs.outputs.pr_url }} | |
| PR_TITLE: ${{ steps.inputs.outputs.pr_title }} | |
| COMMENT: ${{ steps.inputs.outputs.comment }} | |
| PR_AUTHOR: ${{ steps.inputs.outputs.pr_author }} | |
| - name: Send message on Zulip | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| continue-on-error: true | |
| uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.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: Compose PR comment body | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| id: pr_comment | |
| env: | |
| DISPLAY_AUTHOR: ${{ steps.attribution.outputs.display_author }} | |
| run: | | |
| body="🚀 Pull request has been placed on the maintainer queue by ${DISPLAY_AUTHOR}." | |
| trigger_name="${{ steps.inputs.outputs.event_name }}" | |
| trigger_run_url="${{ github.event.workflow_run.html_url }}" | |
| wf_run_url="${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| legacy_suffix="" | |
| if [ "${{ steps.inputs.outputs.input_source }}" = "legacy" ] | |
| then | |
| legacy_suffix=" (legacy)" | |
| fi | |
| metadata=$'['"${trigger_name}"$']('"${trigger_run_url}"$'), [wf_run]('"${wf_run_url}"$')'"${legacy_suffix}" | |
| echo "${metadata}" | |
| # body="${body}"$'\n\n---\n'"${metadata}" | |
| printf 'body<<EOF\n%s\nEOF\n' "${body}" | tee -a "$GITHUB_OUTPUT" | |
| - name: Add comment to PR | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| continue-on-error: true | |
| uses: GrantBirki/comment@3439715f0cf3b8fc29bf47be0e3226679c06c41a # v3.0.0 | |
| 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: ${{ steps.inputs.outputs.pr_number }} | |
| body: ${{ steps.pr_comment.outputs.body }} | |
| - if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| name: Generate app token | |
| id: app-token | |
| uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }} | |
| key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }} | |
| key-name: mathlib-triage-app-pk | |
| azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_TRIAGE }} | |
| azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }} | |
| - name: Add label to PR | |
| if: ${{ steps.authorized.outputs.authorized == 'true' }} | |
| continue-on-error: true | |
| uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 | |
| with: | |
| # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow | |
| # This token is masked by the token minting action and will not be logged accidentally. | |
| github-token: ${{ steps.app-token.outputs.token }} | |
| script: | | |
| const { owner, repo } = context.repo; | |
| const issue_number = ${{ steps.inputs.outputs.pr_number }}; | |
| await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] }); |