Merge remote-tracking branch 'origin/pnat_tsums' into riemmanZeta_mul_two

Author: CBirkbeck

.github/actionlint.yml

@@ -2,3 +2,4 @@ self-hosted-runner:
   labels:
     - bors
     - pr
+    - doc-gen

.github/build.in.yml

@@ -86,7 +86,7 @@ jobs:
         git diff --name-only --diff-filter D origin/${{ github.base_ref }}... | tee removed_files.txt
         echo "Checking for renamed files..."
 
-        # Shows the `R`enamed files, in human readable format
+        # Shows the `R`enamed files, in human-readable format
         # The `awk` pipe
         # * extracts into an array the old name as the key and the new name as the value
         # * eventually prints "`oldName` was renamed to `newName`" for each key-value pair.

.github/workflows/PR_summary.yml

@@ -27,7 +27,7 @@ jobs:
     # && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style'))
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
+      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
           mode: fix
           lint-bib-file: true

.github/workflows/bors.yml

@@ -42,7 +42,9 @@ jobs:
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
-          git fetch --tags
+          # When in nightly mode, fetch tags from the nightly-testing repository
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
           LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
           echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
 
@@ -58,6 +60,7 @@ jobs:
       - name: Checkout branch or tag
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
         with:
+          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
           ref: ${{ env.BRANCH_REF }}
 
       - name: Configure Lean

.github/workflows/bot_fix_style.yaml

@@ -71,16 +71,39 @@ jobs:
         # Fetch the $OLD tag
         git fetch --depth=1 origin tag "$OLD" --no-tags
         # Fetch the $NEW tag.
-        # This will only fetch commits newer than previously fetched commits (ie $OLD)
+        # This will only fetch commits newer than previously fetched commits (i.e. $OLD)
         git fetch origin tag "$NEW" --no-tags
 
-        # Find all commits to lean4 between the $OLD and $NEW toolchains
-        # and extract the github PR numbers
-        # (drop anything that doesn't look like a PR number from the final result)
-        PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/' | grep -E '^[0-9]+$')
+        # Get all commit SHAs between the $OLD and $NEW toolchains
+        COMMIT_SHAS=$(git log --format="%H" "$OLD..$NEW")
+
+        # Initialize an empty string to collect PR numbers
+        PRS=""
+
+        # For each commit, query the GitHub API to get associated PRs
+        for commit_sha in $COMMIT_SHAS; do
+          echo "Checking commit $commit_sha for associated PRs..."
+
+          # Query GitHub API for PRs associated with this commit
+          # Using jq to extract PR numbers from the response
+          pr_numbers=$(curl -s -H "Accept: application/vnd.github.v3+json" \
+            "https://api.github.com/repos/leanprover/lean4/commits/$commit_sha/pulls" | \
+            jq -r '.[] | select(.merged_at != null) | .number | tostring' 2>/dev/null || echo "")
+
+          # Add each PR number to our list (duplicates will be handled later)
+          for pr_num in $pr_numbers; do
+            if [[ "$pr_num" =~ ^[0-9]+$ ]]; then
+              PRS="$PRS $pr_num"
+              echo "Found PR #$pr_num associated with commit $commit_sha"
+            fi
+          done
+        done
+
+        # Remove duplicates and trim whitespace
+        PRS=$(echo "$PRS" | tr ' ' '\n' | sort -u | tr '\n' ' ' | xargs)
 
         # Output the PRs
-        echo "$PRS"
+        echo "Found PRs: $PRS"
         printf "prs<<EOF\n%s\nEOF" "$PRS" >> "$GITHUB_OUTPUT"
 
     - name: Use merged PRs information

.github/workflows/build.yml

@@ -9,7 +9,7 @@ jobs:
     name: Lint style
     runs-on: ubuntu-latest
     steps:
-      - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
+      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
         with:
           mode: suggest
           lint-bib-file: true