Trigger CI for leanprover-community/batteries#1063

.github/workflows/bench_summary_comment.yml

@@ -27,7 +27,7 @@ jobs:
         run: |
           {
             cat scripts/bench_summary.lean
-            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4"' "${PR}"
+            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4" %s' "${PR}" "${{ github.run_id }}"
           } |
             lake env lean --stdin
         env:

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

@@ -4,6 +4,8 @@ on:
   push:
     branches:
       - nightly-testing
+    paths:
+      - lean-toolchain
 
 jobs:
   discover-lean-pr-testing:
@@ -36,8 +38,10 @@ jobs:
         # The "./" in front of the path is important for `git show`
         OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
 
-        echo "new=$NEW" >> "$GITHUB_OUTPUT"
+        echo "old=$OLD"
+        echo "new=$NEW"
         echo "old=$OLD" >> "$GITHUB_OUTPUT"
+        echo "new=$NEW" >> "$GITHUB_OUTPUT"
 
     - name: Clone lean4 repository and get PRs
       id: get-prs
@@ -63,7 +67,10 @@ jobs:
         # This will only fetch commits newer than previously fetched commits (ie $OLD)
         git fetch origin tag "$NEW" --no-tags
 
-        PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
+        # 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]+$')
         
         # Output the PRs
         echo "$PRS"
@@ -74,12 +81,14 @@ jobs:
       run: |
         # Use the PRs from the previous step
         PRS="${{ steps.get-prs.outputs.prs }}"
+        echo "=== PRS ========================="
         echo "$PRS"
-        echo "===================="
         echo "$PRS" | tr ' ' '\n' > prs.txt
+        echo "=== prs.txt ====================="
+        cat prs.txt
         MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
+        echo "=== MATCHING_BRANCHES ==========="
         echo "$MATCHING_BRANCHES"
-        echo "===================="
 
         # Initialize an empty variable to store branches with relevant diffs
         RELEVANT_BRANCHES=""
@@ -92,11 +101,12 @@ jobs:
             # 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\n- $BRANCH"
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES"$'\n- '"$BRANCH"
             fi
         done
 
         # Output the relevant branches
+        echo "=== RELEVANT_BRANCHES ==========="
         echo "'$RELEVANT_BRANCHES'"
         printf "branches<<EOF\n%s\nEOF" "$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
 

.github/workflows/maintainer_bors.yml

@@ -84,4 +84,36 @@ jobs:
           curl --request DELETE \
             --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
             --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
-            # comment uses ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Set up Python
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+
+      - name: Install dependencies
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        run: |
+          python -m pip install --upgrade pip
+          pip install zulip
+
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+          sparse-checkout: |
+            scripts/zulip_emoji_merge_delegate.py
+
+      - name: Run Zulip Emoji Merge Delegate Script
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
+          ( steps.user_permission.outputs.require-result == 'true' ||
+            steps.merge_or_delegate.outputs.bot == 'true' ) }}
+        env:
+          ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+          ZULIP_EMAIL: [email protected]
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"

.github/workflows/zulip_emoji_merge_delegate.yaml

@@ -1,19 +1,19 @@
 name: Zulip Emoji Merge Delegate
 
 on:
-  schedule:
-    - cron: '0 * * * *'  # Runs every hour
+  push:
+    branches:
+      - master
 
 jobs:
-  zulip-emoji-merge-delegate:
+  zulip-emoji-merged:
     runs-on: ubuntu-latest
 
     steps:
     - name: Checkout mathlib repository
       uses: actions/checkout@v4
       with:
-        sparse-checkout: |
-          scripts
+        fetch-depth: 0 # donwload the full repository
 
     - name: Set up Python
       uses: actions/setup-python@v5
@@ -30,6 +30,13 @@ jobs:
         ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
         ZULIP_EMAIL: [email protected]
         ZULIP_SITE: https://leanprover.zulipchat.com
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
       run: |
-        python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$GITHUB_TOKEN"
+          # scan the commits of the past 10 minutes, assuming that the timezone of the current machine
+          # is the same that performed the commit
+          git log --since="10 minutes ago" --pretty=oneline
+
+          printf $'Scanning commits:\n%s\n\nContinuing\n' "$(git log --since="10 minutes ago" --pretty=oneline)"
+          while read -r pr_number; do
+            printf $'Running the python script with pr "%s"\n' "${pr_number}"
+            python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "[Merged by Bors]" "${pr_number}"
+          done < <(git log --oneline -n 10 | awk -F# '{ gsub(/)$/, ""); print $NF}')

Mathlib.lean

@@ -287,14 +287,18 @@ import Mathlib.Algebra.Group.Nat.Even
 import Mathlib.Algebra.Group.Nat.TypeTags
 import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.Group.NatPowAssoc
+import Mathlib.Algebra.Group.Operations
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.PNatPowAssoc
 import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Group.Pointwise.Finset.Interval
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.Group.Pointwise.Set.Card
+import Mathlib.Algebra.Group.Pointwise.Set.Finite
+import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Semiconj.Basic
 import Mathlib.Algebra.Group.Semiconj.Defs
@@ -515,6 +519,7 @@ import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.Algebra.Module.Equiv.Defs
 import Mathlib.Algebra.Module.Equiv.Opposite
 import Mathlib.Algebra.Module.FinitePresentation
+import Mathlib.Algebra.Module.FreeLocus
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
@@ -661,6 +666,7 @@ import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PiLex
 import Mathlib.Algebra.Order.Group.Pointwise.Bounds
 import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
+import Mathlib.Algebra.Order.Group.Pointwise.Interval
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.Synonym
@@ -2820,11 +2826,7 @@ import Mathlib.Data.Set.Operations
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Pairwise.Lattice
-import Mathlib.Data.Set.Pointwise.BigOperators
-import Mathlib.Data.Set.Pointwise.Finite
-import Mathlib.Data.Set.Pointwise.Interval
 import Mathlib.Data.Set.Pointwise.Iterate
-import Mathlib.Data.Set.Pointwise.ListOfFn
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Data.Set.Pointwise.Support
 import Mathlib.Data.Set.Prod
@@ -3952,6 +3954,7 @@ import Mathlib.Order.Filter.ENNReal
 import Mathlib.Order.Filter.EventuallyConst
 import Mathlib.Order.Filter.Extr
 import Mathlib.Order.Filter.FilterProduct
+import Mathlib.Order.Filter.Finite
 import Mathlib.Order.Filter.Germ.Basic
 import Mathlib.Order.Filter.Germ.OrderedMonoid
 import Mathlib.Order.Filter.IndicatorFunction

Mathlib/Algebra/Algebra/Operations.lean

@@ -6,9 +6,9 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Opposite
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Module.Submodule.Pointwise
-import Mathlib.Data.Set.Pointwise.BigOperators
 import Mathlib.Data.Set.Semiring
 import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise