maintainer_bors_wf_run.yml

name: Add "ready-to-merge" and "delegated" label (workflow_run)

on:
  workflow_run:
    workflows: ['Add "ready-to-merge" and "delegated" label']
    types:
      - completed

permissions:
  actions: read
  contents: read


jobs:
  add_ready_to_merge_label:
    name: Add ready-to-merge or delegated label
    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@f5dfe313a79647c07315b451b2dc2a81a161a50d # v1.2.0
        with:
          artifact: workflow-data
          source_workflow: Add "ready-to-merge" and "delegated" label
          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_number=meta.pr_number
            bot=outputs.bot
            removeLabels=outputs.removeLabels
            mOrD=outputs.mOrD

      - name: Download legacy artifact (fallback)
        id: download-legacy-artifact
        if: ${{ steps.bridge.outputs.pr_number == '' }}
        uses: dawidd6/action-download-artifact@8a338493df3d275e4a7a63bcff3b8fe97e51a927 # v19
        with:
          workflow: maintainer_bors.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_number=$(jq -r '.pr_number // empty' "${data_file}")"
            echo "bot=$(jq -r '.bot // empty' "${data_file}")"
            echo "removeLabels=$(jq -r '.removeLabels // .remove_labels // empty' "${data_file}")"
            echo "mOrD=$(jq -r '.mOrD // .m_or_d // empty' "${data_file}")"
          } | 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_NUMBER: ${{ steps.bridge.outputs.pr_number }}${{ steps.legacy.outputs.pr_number }}
          INPUT_BOT: ${{ steps.bridge.outputs.bot }}${{ steps.legacy.outputs.bot }}
          INPUT_REMOVE_LABELS: ${{ steps.bridge.outputs.removeLabels }}${{ steps.legacy.outputs.removeLabels }}
          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') }}
        run: |
          {
            echo "author=${INPUT_AUTHOR}"
            echo "pr_number=${INPUT_PR_NUMBER}"
            echo "bot=${INPUT_BOT}"
            echo "removeLabels=${INPUT_REMOVE_LABELS}"
            echo "mOrD=${INPUT_MORD}"
            echo "input_source=${INPUT_SOURCE}"
          } | 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_bors.yml"
          echo "Using legacy workflow-data artifact fallback from maintainer_bors.yml" >> "$GITHUB_STEP_SUMMARY"

      - name: Check whether user is a mathlib admin
        id: user_permission
        if: ${{ ! steps.inputs.outputs.mOrD == '' || ! steps.inputs.outputs.removeLabels == '' }}
        uses: actions-cool/check-user-permission@c21884f3dda18dafc2f8b402fe807ccc9ec1aa5e # v2.4.0
        with:
          username: ${{ steps.inputs.outputs.author }}
          require: 'admin'

      - name: Generate app token
        id: app-token
        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
        if: ${{ ! steps.inputs.outputs.mOrD == '' || ! steps.inputs.outputs.removeLabels == '' }}
        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 ready-to-merge or delegated label
        id: add_label
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        uses: octokit/request-action@b91aabaa861c777dcdb14e2387e30eddf04619ae # v3.0.0
        with:
          route: POST /repos/:repository/issues/:issue_number/labels
          # Unexpected input warning from the following is expected:
          # https://github.com/octokit/request-action?tab=readme-ov-file#warnings
          repository: ${{ github.repository }}
          issue_number: ${{ steps.inputs.outputs.pr_number }}
          labels: '["${{ steps.inputs.outputs.mOrD }}"]'
        env:
          # This token is masked by the token minting action and will not be logged accidentally
          GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}

      - if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        id: remove_labels
        name: Remove "awaiting-author" and "maintainer-merge"
        # 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: |
          for label in awaiting-author maintainer-merge; do
            curl --request DELETE \
              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.inputs.outputs.pr_number }}/labels/${label}" \
              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
          done

      - name: On bors r/d-, remove ready-to-merge or delegated label
        if: ${{ ! steps.inputs.outputs.removeLabels == '' && steps.user_permission.outputs.require-result == 'true' }}
        # 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: |
          for label in ready-to-merge delegated; do
            curl --request DELETE \
              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.inputs.outputs.pr_number }}/labels/${label}" \
              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
          done

      - name: Checkout local actions
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == '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.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        uses: ./workflow-actions/.github/actions/get-mathlib-ci

      - name: Set up Python
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
        with:
          python-version: '3.x'

      - name: Install dependencies
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        run: |
          python -m pip install --upgrade pip
          pip install -r "$CI_SCRIPTS_DIR/zulip/requirements.txt"

      - name: update zulip emoji reactions
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == 'true' ) }}
        continue-on-error: true
        env:
          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
          ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
          ZULIP_SITE: https://leanprover.zulipchat.com
        run: |
          python "${CI_SCRIPTS_DIR}/zulip/zulip_emoji_reactions.py" "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.inputs.outputs.mOrD }}" "${{ steps.inputs.outputs.mOrD }}" "${{ steps.inputs.outputs.pr_number }}"