Trigger CI for leanprover/lean4#6083

.github/workflows/PR_summary.yml

@@ -5,6 +5,7 @@ on:
 
 jobs:
   build:
+    name: "post-or-update-summary-comment"
     runs-on: ubuntu-latest
 
     steps:

.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

@@ -24,6 +24,25 @@ jobs:
         git config --global user.name "github-actions"
         git config --global user.email "[email protected]"
 
+    - name: Determine old and new lean-toolchain
+      id: determine-toolchains
+      run: |
+        # `lean-toolchain` contains a string of the form "leanprover/lean4:nightly-2024-11-20"
+        # We grab the part after the ":"
+        NEW=$(cut -f2 -d: lean-toolchain)
+
+        # Find the commit hash of the previous change to `lean-toolchain`
+        PREV_COMMIT=$(git log -2 --format=format:%H -- lean-toolchain | tail -1)
+
+        # Get the contents of `lean-toolchain` from the previous commit
+        # The "./" in front of the path is important for `git show`
+        OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
+
+        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
       run: |
@@ -38,28 +57,37 @@ jobs:
         # Navigate to the cloned repository
         cd lean4-nightly || exit 1
 
-        # Shallow fetch of the last two tags
-        LAST_TWO_TAGS=$(git ls-remote --tags | grep nightly | tail -2 | cut -f2)
-        OLD=$(echo "$LAST_TWO_TAGS" | head -1)
-        NEW=$(echo "$LAST_TWO_TAGS" | tail -1)
+        # Use the OLD and NEW toolchains determined in the previous step
+        OLD="${{ steps.determine-toolchains.outputs.old }}"
+        NEW="${{ steps.determine-toolchains.outputs.new }}"
+
+        # Fetch the $OLD tag
         git fetch --depth=1 origin tag "$OLD" --no-tags
-        # Fetch the latest 100 commits prior to the $NEW tag.
-        # This should cover the terrain between $OLD and $NEW while still being a speedy download.
-        git fetch --depth=100 origin tag "$NEW" --no-tags
+        # Fetch the $NEW tag.
+        # 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"
-        echo "prs=$PRS" >> "$GITHUB_OUTPUT"
+        printf "prs<<EOF\n%s\nEOF" "$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 ========================="
+        echo "$PRS"
         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"
 
         # Initialize an empty variable to store branches with relevant diffs
@@ -73,25 +101,26 @@ 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 $BRANCH"
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES"$'\n- '"$BRANCH"
             fi
         done
 
         # Output the relevant branches
+        echo "=== RELEVANT_BRANCHES ==========="
         echo "'$RELEVANT_BRANCHES'"
-        echo "branches=$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
+        printf "branches<<EOF\n%s\nEOF" "$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"
+          echo "branches_exist=false" >> "$GITHUB_ENV"
         else
-          echo "no_branches=false" >> "$GITHUB_ENV"
+          echo "branches_exist=true" >> "$GITHUB_ENV"
         fi
 
     - name: Send message on Zulip
-      if: env.no_branches == 'false'
+      if: env.branches_exist == 'true'
       uses: zulip/github-actions-zulip/send-message@v1
       with:
         api-key: ${{ secrets.ZULIP_API_KEY }}

.github/workflows/maintainer_bors.yml

@@ -19,13 +19,8 @@ jobs:
     # both set simultaneously: depending on the event that triggers the PR, usually only one is set
     env:
       AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
-      PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
       COMMENT_EVENT: ${{ github.event.comment.body }}
       COMMENT_REVIEW: ${{ github.event.review.body }}
-      PR_TITLE_ISSUE: ${{ github.event.issue.title }}
-      PR_TITLE_PR: ${{ github.event.pull_request.title }}
-      PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
-      EVENT_NAME: ${{ github.event_name }}
     name: Add ready-to-merge or delegated label
     runs-on: ubuntu-latest
     steps:
@@ -43,8 +38,7 @@ jobs:
 
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
-          printf $'PR_NUMBER: \'%s\'\n' "${PR_NUMBER}"
-          printf $'OTHER_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
+          printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
@@ -64,9 +58,6 @@ jobs:
         uses: actions-cool/check-user-permission@v2
         with:
           require: 'admin'
-          # review(_comment) use
-          # require: 'write'
-          # token: ${{ secrets.TRIAGE_TOKEN }}
 
       - name: Add ready-to-merge or delegated label
         id: add_label
@@ -75,13 +66,12 @@ jobs:
             steps.merge_or_delegate.outputs.bot == 'true' ) }}
         uses: octokit/[email protected]
         with:
-          # check is this ok? was /repos/:repository/issues/:issue_number/labels
           route: POST /repos/:repository/issues/:issue_number/labels
           repository: ${{ github.repository }}
           issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
           labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }} # comment uses ${{ secrets.GITHUB_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
 
       - if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
@@ -92,6 +82,37 @@ jobs:
         # (and send an annoying email) if the labels don't exist
         run: |
           curl --request DELETE \
-            --url "https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels/awaiting-author" \
+            --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:
+          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 }}"