Maintainer merge (workflow_run) #133720
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 | |
| permissions: | |
| actions: read | |
| contents: read | |
| pull-requests: write | |
| 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 | |
| steps: | |
| - name: Consume bridge artifact | |
| id: bridge | |
| uses: leanprover-community/privilege-escalation-bridge/consume@d3bd99c50a4cf8c5350a211e8e3ba07ac19067d8 # v1.1.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@2536c51d3d126276eb39f74d6bc9c72ac6ef30d3 # v16 | |
| 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 != '' }} | |
| run: | | |
| { | |
| echo "author=${{ steps.bridge.outputs.author }}${{ steps.legacy.outputs.author }}" | |
| echo "pr_author=${{ steps.bridge.outputs.pr_author }}${{ steps.legacy.outputs.pr_author }}" | |
| echo "pr_number=${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}" | |
| echo "pr_title=${{ steps.bridge.outputs.pr_title }}${{ steps.legacy.outputs.pr_title }}" | |
| echo "pr_url=${{ steps.bridge.outputs.pr_url }}${{ steps.legacy.outputs.pr_url }}" | |
| echo "event_name=${{ steps.bridge.outputs.event_name }}${{ steps.legacy.outputs.event_name }}" | |
| echo "mOrD=${{ steps.bridge.outputs.mOrD }}${{ steps.legacy.outputs.mOrD }}" | |
| echo "input_source=${{ steps.bridge.outputs.pr_number != '' && 'bridge' || (steps.legacy.outputs.pr_number != '' && 'legacy' || 'none') }}" | |
| } | tee -a "$GITHUB_OUTPUT" | |
| printf 'comment<<EOF\n%s\nEOF\n' "${{ steps.bridge.outputs.comment }}${{ steps.legacy.outputs.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: 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: ${{ steps.inputs.outputs.author }} | |
| GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`) | |
| - name: Checkout local actions | |
| if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }} | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| ref: ${{ github.workflow_sha }} | |
| fetch-depth: 1 | |
| sparse-checkout: .github/actions | |
| path: workflow-actions | |
| - name: Get mathlib-ci | |
| if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }} | |
| uses: ./workflow-actions/.github/actions/get-mathlib-ci | |
| - name: Determine Zulip topic | |
| if: ${{ steps.actorTeams.outputs.isTeamMember == '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.actorTeams.outputs.isTeamMember == '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_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}" | |
| message="${message}"$'\n\n---\n'"${metadata}" | |
| printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT" | |
| env: | |
| AUTHOR: ${{ steps.inputs.outputs.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.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: Compose PR comment body | |
| if: ${{ steps.actorTeams.outputs.isTeamMember == 'true' }} | |
| id: pr_comment | |
| run: | | |
| body="🚀 Pull request has been placed on the maintainer queue by ${{ steps.inputs.outputs.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_name}"$']('"${trigger_run_url}"$')\nwf_run: [workflow_run]('"${wf_run_url}"$')'"${legacy_suffix}" | |
| 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.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: ${{ steps.inputs.outputs.pr_number }} | |
| body: ${{ steps.pr_comment.outputs.body }} | |
| - if: ${{ steps.actorTeams.outputs.isTeamMember == '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.actorTeams.outputs.isTeamMember == 'true' }} | |
| uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.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'] }); |