nightly_detect_failure.yml

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

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

jobs:
  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@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
      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 branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
          You can `git fetch; git checkout nightly-testing` and push a fix.

  handle_success:
    if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
    runs-on: ubuntu-latest

    steps:
    - name: Generate app token
      id: app-token
      uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
      with:
        app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
        private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
    # The create-github-app-token README states that this token is masked and will not be logged accidentally.

    - name: Checkout code
      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      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: ${{ steps.app-token.outputs.token }}
    - name: Update the nightly-testing-YYYY-MM-DD branch
      run: |
        toolchain="$(<lean-toolchain)"
        if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
          version=${BASH_REMATCH[1]}
          printf 'NIGHTLY=%s\n' "${version}" >> "${GITHUB_ENV}"
          # Check if the remote tag exists
          if git ls-remote --tags --exit-code origin "nightly-testing-$version" >/dev/null; then
              printf 'Tag nightly-testing-%s already exists on the remote.' "${version}"
          else
              # If the tag does not exist, create and push the tag to remote
              printf 'Creating tag %s from the current state of the nightly-testing branch.' "nightly-testing-${version}"
              git tag "nightly-testing-${version}"
              git push origin "nightly-testing-${version}"
          fi
          hash="$(git rev-parse "nightly-testing-${version}")"
          printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
        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
      env:
        ZULIP_EMAIL: 'github-mathlib4-bot@leanprover.zulipchat.com'
        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
        ZULIP_SITE: 'https://leanprover.zulipchat.com'
        SHA: ${{ env.SHA }}
      run: |
        import os
        import zulip
        client = zulip.Client(email=os.getenv('ZULIP_EMAIL'), api_key=os.getenv('ZULIP_API_KEY'), site=os.getenv('ZULIP_SITE'))

        # Get the last message from the bot in the 'status updates' topic.
        # We narrow by sender to ignore human replies in between.
        bot_email = 'github-mathlib4-bot@leanprover.zulipchat.com'
        request = {
          'anchor': 'newest',
          'num_before': 1,
          'num_after': 0,
          'narrow': [
            {'operator': 'stream', 'operand': 'nightly-testing'},
            {'operator': 'topic', 'operand': 'Batteries status updates'},
            {'operator': 'sender', 'operand': bot_email}
          ],
          'apply_markdown': False    # Otherwise the content test below fails.
        }
        response = client.get_messages(request)
        messages = response['messages']
        if not messages or messages[0]['content'] != f"✅ The latest CI for Batteries' [nightly-testing branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))":
            # Post the success message
            request = {
                'type': 'stream',
                'to': 'nightly-testing',
                'topic': 'Batteries status updates',
                'content': f"✅ The latest CI for Batteries' [nightly-testing branch](https://github.com/${{ github.repository }}/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
            }
            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@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
      with:
        script: |
          const branchName = `bump/nightly-${process.env.NIGHTLY}`;
          console.log(`Looking for branch: ${branchName}`);

          // Use paginate to get all branches
          const branches = await github.paginate(github.rest.repos.listBranches, {
            owner: context.repo.owner,
            repo: context.repo.repo
          });

          const exists = branches.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@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
      with:
        result-encoding: string
        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@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0.1
      with:
        script: |
          try {
            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 match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
            if (!match) {
              core.setFailed('Toolchain pattern did not match');
              core.setOutput('toolchain_content', content);
              return null;
            }
            return match[1];
          } catch (error) {
            core.setFailed(error.message);
            return null;
          }

    - name: Send warning message on Zulip if pattern doesn't match
      if: failure()
      uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
      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: |
          ⚠️ Warning: The lean-toolchain file in the latest bump branch does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
          Current content: ${{ steps.bump_version.outputs.toolchain_content }}
          This needs to be fixed for the nightly testing process to work correctly.

    - name: Setup for automatic PR creation
      if: steps.check_branch.outputs.result == 'false'
      env:
        BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
        BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
        SHA: ${{ env.SHA }}
      run: |
        echo "Installing zulip CLI..."
        pip install zulip
        echo "Configuring git identity for mathlib4-bot..."
        git config --global user.name "mathlib4-bot"
        git config --global user.email "github-mathlib4-bot@leanprover.zulipchat.com"
        echo "Setting up zulip credentials..."
        {
          echo "[api]"
          echo "email=github-mathlib4-bot@leanprover.zulipchat.com"
          echo "key=${{ secrets.ZULIP_API_KEY }}"
          echo "site=https://leanprover.zulipchat.com"
        } > ~/.zuliprc
        chmod 600 ~/.zuliprc
        echo "Setup complete"

    - name: Clean workspace and checkout Batteries
      if: steps.check_branch.outputs.result == 'false'
      run: |
        sudo rm -rf -- *
    # Regenerate the app token just before use.
    # GitHub App tokens expire after 1 hour, and the preceding steps can take longer than that.
    - name: Regenerate app token for Batteries checkout
      if: steps.check_branch.outputs.result == 'false'
      id: app-token-2
      uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
      with:
        app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
        private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
    - name: Checkout Batteries repository
      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      if: steps.check_branch.outputs.result == 'false'
      with:
        ref: nightly-testing # checkout nightly-testing branch (shouldn't matter which)
        fetch-depth: 0 # checkout all branches
        token: ${{ steps.app-token-2.outputs.token }}

    - name: Attempt automatic PR creation
      id: auto_pr
      if: steps.check_branch.outputs.result == 'false'
      continue-on-error: true
      env:
        BUMP_VERSION: ${{ steps.bump_version.outputs.result }}
        BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }}
        SHA: ${{ env.SHA }}
        GH_TOKEN: ${{ steps.app-token-2.outputs.token }}
        ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
      run: |
        echo "Current version: ${NIGHTLY}"
        echo "Target bump branch: ${BUMP_BRANCH}"
        echo "Using commit SHA: ${SHA}"
        current_version="${NIGHTLY}"
        bump_branch_suffix="${BUMP_BRANCH#bump/}"
        echo "Running create-adaptation-pr.sh with:"
        echo "  bumpversion: ${bump_branch_suffix}"
        echo "  nightlydate: ${current_version}"
        echo "  nightlysha: ${SHA}"
        ./scripts/create-adaptation-pr.sh --bumpversion="${bump_branch_suffix}" --nightlydate="${current_version}" --nightlysha="${SHA}" --auto=yes

    - name: Fallback to manual instructions
      if: steps.auto_pr.outcome == 'failure' && steps.check_branch.outputs.result == 'false'
      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 }}
        REPOSITORY: ${{ github.repository }}
        CURRENT_RUN_ID: ${{ github.run_id }}
      shell: python
      run: |
        import os
        import re
        import zulip
        client = zulip.Client(config_file="~/.zuliprc")
        current_version = os.getenv('NIGHTLY')
        bump_version = os.getenv('BUMP_VERSION')
        bump_branch = os.getenv('BUMP_BRANCH')
        sha = os.getenv('SHA')
        repository = os.getenv('REPOSITORY')
        current_run_id = os.getenv('CURRENT_RUN_ID')
        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 from the bot in the 'Batteries bump branch reminders' topic.
            # We narrow by sender to ignore human replies in between.
            bot_email = 'github-mathlib4-bot@leanprover.zulipchat.com'
            request = {
              'anchor': 'newest',
              'num_before': 1,
              'num_after': 0,
              'narrow': [
                {'operator': 'stream', 'operand': 'nightly-testing'},
                {'operator': 'topic', 'operand': 'Batteries bump branch reminders'},
                {'operator': 'sender', 'operand': bot_email}
              ],
              'apply_markdown': False    # Otherwise the content test below fails.
            }
            response = client.get_messages(request)
            messages = response['messages']
            last_bot_message = messages[0] if messages else None
            bump_branch_suffix = bump_branch.replace('bump/', '')
            failed_link = f"https://github.com/{repository}/actions/runs/{current_run_id}"
            payload = f"🛠️: Automatic PR creation [failed]({failed_link}). Please 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 Batteries root:\n\n"
            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
            # Check if we already posted a message for this nightly date and bump branch.
            # We extract these fields from the last bot message rather than comparing substrings,
            # since the message also contains a run ID that differs between workflow runs.
            should_post = True
            if last_bot_message:
                last_content = last_bot_message['content']
                # Extract nightly date and bump branch from last bot message
                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2})', last_content)
                branch_match = re.search(r'PR that to (bump/v[\d.]+)', last_content)
                if date_match and branch_match:
                    last_date = date_match.group(1)
                    last_branch = branch_match.group(1)
                    if last_date == current_version and last_branch == bump_branch:
                        should_post = False
                        print(f'Already posted for nightly {current_version} and {bump_branch}')
            if should_post:
                if last_bot_message:
                    print("###### Last bot message:")
                    print(last_bot_message['content'])
                    print("###### Current message:")
                    print(payload)
                # 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.')