From 0a06888efd2949195b73d8779d946dcf0f03fb4e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 5 Jan 2025 10:43:19 +1100
Subject: [PATCH] chore: post reminder to create adaptation PR

---
 .github/workflows/nightly_detect_failure.yml | 117 +++++++++++++++++++
 1 file changed, 117 insertions(+)

diff --git a/.github/workflows/nightly_detect_failure.yml b/.github/workflows/nightly_detect_failure.yml
index 98aaf457f0..05020ad3c9 100644
--- a/.github/workflows/nightly_detect_failure.yml
+++ b/.github/workflows/nightly_detect_failure.yml
@@ -88,3 +88,120 @@ jobs:
             result = client.send_message(request)
             print(result)
       shell: python
+
+    # Next, determine if we should remind the humans to create a new PR to the `bump/v4.X.0` branch.
+
+    - name: Check for matching bump/nightly-YYYY-MM-DD branch
+      id: check_branch
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const branchName = `bump/nightly-${process.env.NIGHTLY}`;
+          const branches = await github.rest.repos.listBranches({
+            owner: context.repo.owner,
+            repo: context.repo.repo
+          });
+          const exists = branches.data.some(branch => branch.name === branchName);
+          if (exists) {
+            console.log(`Branch ${branchName} exists.`);
+            return true;
+          } else {
+            console.log(`Branch ${branchName} does not exist.`);
+            return false;
+          }
+        result-encoding: string
+
+    - name: Exit if matching branch exists
+      if: steps.check_branch.outputs.result == 'true'
+      run: |
+        echo "Matching bump/nightly-YYYY-MM-DD branch found, no further action needed."
+        exit 0
+
+    - name: Fetch latest bump branch name
+      id: latest_bump_branch
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const branches = await github.paginate(github.rest.repos.listBranches, {
+            owner: context.repo.owner,
+            repo: context.repo.repo
+          });
+          const bumpBranches = branches
+            .map(branch => branch.name)
+            .filter(name => name.match(/^bump\/v4\.\d+\.0$/))
+            .sort((a, b) => b.localeCompare(a, undefined, {numeric: true, sensitivity: 'base'}));
+          if (!bumpBranches.length) {
+            throw new Exception("Did not find any bump/v4.x.0 branch")
+          }
+          const latestBranch = bumpBranches[0];
+          return latestBranch;
+
+    - name: Fetch lean-toolchain from latest bump branch
+      id: bump_version
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const response = await github.rest.repos.getContent({
+            owner: context.repo.owner,
+            repo: context.repo.repo,
+            path: 'lean-toolchain',
+            ref: ${{ steps.latest_bump_branch.outputs.result }}
+          });
+          const content = Buffer.from(response.data.content, 'base64').toString();
+          const version = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/)[1];
+          return version;
+
+    - name: Compare versions and post a reminder.
+      env:
+        BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
+        BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
+        SHA: ${{ env.SHA }}
+        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
+      shell: python
+      run: |
+        import os
+        import zulip
+        client = zulip.Client(email='github-mathlib4-bot@leanprover.zulipchat.com', api_key=os.getenv('ZULIP_API_KEY'), site='https://leanprover.zulipchat.com')
+        current_version = os.getenv('NIGHTLY')
+        bump_version = os.getenv('BUMP_VERSION')
+        bump_branch = os.getenv('BUMP_BRANCH')
+        sha = os.getenv('SHA')
+        print(f'Current version: {current_version}, Bump version: {bump_version}, SHA: {sha}')
+        if current_version > bump_version:
+            print('Lean toolchain in `nightly-testing` is ahead of the bump branch.')
+            # Get the last message in the 'Batteries bump branch reminders' topic
+            request = {
+              'anchor': 'newest',
+              'num_before': 1,
+              'num_after': 0,
+              'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries bump branch reminders'}],
+              'apply_markdown': False    # Otherwise the content test below fails.
+            }
+            response = client.get_messages(request)
+            messages = response['messages']
+            bump_branch_suffix = bump_branch.replace('bump/', '')
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
+            payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
+            # Only post if the message is different
+            # We compare the first 160 characters, since that includes the date and bump version
+            if not messages or messages[0]['content'][:160] != payload[:160]:
+                # Log messages, because the bot seems to repeat itself...
+                if messages:
+                    print("###### Last message:")
+                    print(messages[0]['content'])
+                    print("###### Current message:")
+                    print(payload)
+                else:
+                    print('The strings match!')
+                # Post the reminder message
+                request = {
+                    'type': 'stream',
+                    'to': 'nightly-testing',
+                    'topic': 'Batteries bump branch reminders',
+                    'content': payload
+                }
+                result = client.send_message(request)
+                print(result)
+        else:
+            print('No action needed.')