maintainer_bors_wf_run.yml

name: Bors merge/delegate follow-up (workflow_run)

on:
  workflow_run:
    workflows: ['Bors merge/delegate follow-up']
    types:
      - completed

permissions:
  actions: read
  contents: read


jobs:
  bors_command_followup:
    name: Bors merge/delegate follow-up
    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@ea7d63d1c8ece92a8e89b6a6d8fda40603167a91 # v1.3.0
        with:
          artifact: workflow-data
          source_workflow: Bors merge/delegate follow-up
          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
            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_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 "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_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 "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 == '' }}
        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 == '' }}
        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 }}

      # The `ready-to-merge` / `delegated` lifecycle labels are managed by bors
      # itself (see the `[labels]` table in bors.toml); this workflow no longer
      # adds or removes them. It still removes the `awaiting-author` and
      # `maintainer-merge` labels and updates the Zulip emoji on a merge/delegate
      # command.
      - 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: Checkout local actions
        if: ${{ ! steps.inputs.outputs.mOrD == '' &&
          ( steps.user_permission.outputs.require-result == 'true' ||
            steps.inputs.outputs.bot == '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.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@ece7cb06caefa5fff74198d8649806c4678c61a1 # v6.3.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 }}"