ci(.github/workflows): add discover-lean-pr-testing.yml (#17399)

This workflow finds branches of the form `lean-pr-testing-NNNN`
corresponding to core PRs that have been merged into the latest nightly.
These branches should be merged into the `nightly-testing` branch of
mathlib.
The workflow only reports branches that have a non-trivial diff.

.github/workflows/discover-lean-pr-testing.yml

@@ -0,0 +1,109 @@
+name: Discover `lean-pr-testing` branches
+
+on:
+  push:
+    branches:
+      - nightly-testing
+    paths:
+      - lean-toolchain
+
+jobs:
+  discover-lean-pr-testing:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout mathlib repository
+      uses: actions/checkout@v4
+      with:
+        repository: leanprover-community/mathlib
+        ref: nightly-testing
+        fetch-depth: 0  # Fetch all branches
+
+    - name: Set up Git
+      run: |
+        git config --global user.name "github-actions"
+        git config --global user.email "[email protected]"
+
+    - name: Read date from lean-toolchain
+      id: fetch-date
+      run: |
+        TODAY=$(grep -oP 'nightly-\K\d{4}-\d{2}-\d{2}' lean-toolchain)
+        echo "TODAY=$TODAY" >> "$GITHUB_ENV"
+
+    - name: Set YESTERDAY
+      id: set-yesterday
+      run: |
+        YESTERDAY=$(date -d "$TODAY -1 day" +%Y-%m-%d)
+        echo "YESTERDAY=$YESTERDAY" >> "$GITHUB_ENV"
+
+    - name: Clone lean4-nightly repository and get PRs
+      id: get-prs
+      run: |
+        NIGHTLY_URL="https://github.com/leanprover/lean4-nightly.git"
+        
+        # Create a temporary directory for cloning
+        cd "$(mktemp -d)" || exit 1
+        
+        # Clone the repository with a depth of 30 (adjust as needed)
+        git clone --depth 30 "$NIGHTLY_URL"
+        
+        # Navigate to the cloned repository
+        cd lean4-nightly || exit 1
+        YESTERDAY="${{ steps.set-yesterday.outputs.yesterday }}"
+        TODAY="${{ steps.fetch-date.outputs.today }}"
+        PRS=$(git log --oneline "nightly-$YESTERDAY..nightly-$TODAY" | sed 's/.*(#\([0-9]\+\))$/\1/')
+        
+        # Output the PRs
+        echo "$PRS"
+        echo "prs=$PRS" >> "$GITHUB_OUTPUT"
+
+    - name: Use merged PRs information
+      id: find-branches
+      run: |
+        # Use the PRs from the previous step
+        PRS="${{ steps.get-prs.outputs.prs }}"
+        echo "$PRS" | tr ' ' '\n' > prs.txt
+        MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
+
+        # Initialize an empty variable to store branches with relevant diffs
+        RELEVANT_BRANCHES=""
+
+        # Loop through each matching branch
+        for BRANCH in $MATCHING_BRANCHES; do
+            # Get the diff filenames
+            DIFF_FILES=$(git diff --name-only "origin/nightly-testing...$BRANCH")
+            
+            # Check if the diff contains files other than the specified ones
+            if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -e 'lean-toolchain'; then
+                # If it does, add the branch to RELEVANT_BRANCHES
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES $BRANCH"
+            fi
+        done
+
+        # Output the relevant branches
+        echo "'$RELEVANT_BRANCHES'"
+        echo "branches=$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
+
+    - name: Check if there are relevant branches
+      id: check-branches
+      run: |
+        if [ -z "${{ steps.find-branches.outputs.branches }}" ]; then
+          echo "no_branches=true" >> "$GITHUB_ENV"
+        else
+          echo "no_branches=false" >> "$GITHUB_ENV"
+        fi
+
+    - name: Send message on Zulip
+      if: env.no_branches == 'false'
+      uses: zulip/github-actions-zulip/send-message@v1
+      with:
+        api-key: ${{ secrets.ZULIP_API_KEY }}
+        email: '[email protected]'
+        organization-url: 'https://leanprover.zulipchat.com'
+        to: 'nightly-testing'
+        type: 'stream'
+        topic: 'Mathlib status updates'
+        content: |
+          We will need to merge the following branches into `nightly-testing`:
+
+          ${{ steps.find-branches.outputs.branches }}