nightly_detect_failure.yml

name: Post to zulip if the nightly-testing branch is failing.

on:
  workflow_run:
    workflows: ["ci"]
    types:
      - completed

jobs:
  # Whenever `nightly-testing` fails CI,
  # notify the 'nightly-testing' stream on Zulip.
  handle_failure:
    if: ${{ github.event.workflow_run.conclusion == 'failure' && github.event.workflow_run.head_branch == 'nightly-testing' }}
    runs-on: ubuntu-latest

    steps:
    - name: Send message on Zulip
      uses: zulip/github-actions-zulip/send-message@v1
      with:
        api-key: ${{ secrets.ZULIP_API_KEY }}
        email: 'github-mathlib4-bot@leanprover.zulipchat.com'
        organization-url: 'https://leanprover.zulipchat.com'
        to: 'nightly-testing'
        type: 'stream'
        topic: 'Batteries status updates'
        content: |
          ❌️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).

  # Whenever `nightly-testing` passes CI,
  # push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Batteries on that nightly release.
  handle_success:
    if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
    runs-on: ubuntu-latest

    steps:
    - name: Checkout code
      uses: actions/checkout@v4
      with:
        ref: nightly-testing # checkout nightly-testing branch
        fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
        token: ${{ secrets.NIGHTLY_TESTING }}
    - name: Update the nightly-testing-YYYY-MM-DD tag
      run: |
        toolchain=$(<lean-toolchain)
        if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
          version=${BASH_REMATCH[1]}
          if git ls-remote --tags --exit-code origin "refs/tags/nightly-testing-$version" >/dev/null; then
              echo "Tag nightly-testing-$version already exists on the remote."
          else
              # If the tag does not exist, create and push the tag to remote
              echo "Creating tag nightly-testing-$version from the current state of the nightly-testing branch."
              git tag nightly-testing-$version
              git push origin nightly-testing-$version
          fi
        else
          echo "Error: The file lean-toolchain does not contain the expected pattern."
          exit 1
        fi

    # Now post a success message to zulip, if the last message there is not a success message.
    # https://chat.openai.com/share/87656d2c-c804-4583-91aa-426d4f1537b3
    - name: Install Zulip API client
      run: pip install zulip

    - name: Check last message and post if necessary
      run: |
        import zulip
        client = zulip.Client(email='github-mathlib4-bot@leanprover.zulipchat.com', api_key='${{ secrets.ZULIP_API_KEY }}', site='https://leanprover.zulipchat.com')

        # Get the last message in the 'status updates' topic
        request = {
          'anchor': 'newest',
          'num_before': 1,
          'num_after': 0,
          'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Batteries status updates'}],
          'apply_markdown': False
        }
        response = client.get_messages(request)
        messages = response['messages']
        if not messages or messages[0]['content'] != "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!":
            # Post the success message
            request = {
                'type': 'stream',
                'to': 'nightly-testing',
                'topic': 'Batteries status updates',
                'content': "✅️ The latest CI for Batteries' [`nightly-testing`](https://github.com/leanprover-community/batteries/tree/nightly-testing) branch has succeeded!"
            }
            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.')