[Merged by Bors] - fix: rewrite update_dependencies_zulip action

.github/workflows/update_dependencies_zulip.yml

@@ -7,39 +7,44 @@ on:
     workflows: ["continuous integration"]
     types:
       - completed
+    branches:
+      - 'update-dependencies-**'
 
 jobs:
   monitor-failures:
     runs-on: ubuntu-latest
-    if: ${{ github.event.workflow_run.conclusion == 'failure' && startsWith(github.event.workflow_run.head_branch, 'update-dependencies-') }}
+    if: ${{ github.event.workflow_run.conclusion == 'failure' }}
 
     steps:
-      - name: Checkout repository
-        uses: actions/checkout@v4
+      - name: Construct message
+        uses: actions/github-script@v7
+        id: construct_message
         with:
-          fetch-depth: 0
-          token: ${{ secrets.NIGHTLY_TESTING }}
-
-      - name: Set GH_TOKEN
-        run: echo "GH_TOKEN=${{ secrets.NIGHTLY_TESTING }}" >> "$GITHUB_ENV"
-
-      - name: Get PR number
-        id: get_pr
-        run: |
-          pr_number=$(gh pr list --state open --head "leanprover-community/mathlib4:${{ github.event.workflow_run.head_branch }}" --json number -q '.[0].number')
-          echo "pr_number=$pr_number" >> "$GITHUB_ENV"
-
-      - name: Update PR labels
-        if: env.pr_number
-        run: |
-          gh pr edit "${{ env.pr_number }}" --remove-label "auto-merge-after-CI" --add-label "awaiting-CI,awaiting-review"
-
-      - name: Get CI URL
-        id: ci_url
-        run: |
-          url="https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}"
-          curl -s "$url" |
-            awk -v url="$url" -F'/' '/^ *href/ {gsub(/"/, "", $NF); printf("summary<<EOF\n%s/job/%s\nEOF", url, $NF)}' >> "$GITHUB_OUTPUT"
+          github-token: ${{ secrets.NIGHTLY_TESTING }}
+          result-encoding: string
+          script: |
+            const owner = context.repo.owner, repo = context.repo.repo;
+            let output = "❌ `lake update` [failed](" + context.payload.workflow_run.html_url + "). "
+            let prs = context.payload.workflow_run.pull_requests
+            if (prs.length) {
+              for (let pr of prs) {
+                const { data: pullRequest } = await github.rest.pulls.get({
+                  owner,
+                  repo,
+                  pull_number: pr.number,
+                });
+                output += "Found [PR " + pr.number + "](" + pullRequest.html_url + "). "
+                await github.rest.issues.removeLabel({
+                  owner,
+                  repo,
+                  issue_number: pr.number,
+                  name: "auto-merge-after-CI",
+                });
+              }
+            } else {
+              output += "No PR found for this run!";
+            }
+            return output;
 
       - name: Send Zulip message
         uses: zulip/github-actions-zulip/send-message@v1
@@ -51,4 +56,4 @@ jobs:
           type: 'stream'
           topic: 'Mathlib `lake update` failure'
           content: |
-            ❌ `lake update` [failed](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
+            ${{ steps.construct_message.outputs.result }}