nightly_detect_failure.yml

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

on:
  workflow_run:
    workflows: ["continuous integration"]
    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@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: 'Mathlib status updates'
        content: |
          ❌ The latest CI for Mathlib's branch#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: 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 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}"
              hash="$(git rev-parse "nightly-testing-${version}")"
              curl -X POST "https://speed.lean-lang.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
          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

    # Next, we'll update the `nightly-with-mathlib` branch at Lean.
    - name: Cleanup workspace
      run: |
        sudo rm -rf -- *
    # Checkout the Lean repository on 'nightly-with-mathlib'
    - name: Checkout Lean repository
      uses: actions/checkout@v4
      with:
        repository: leanprover/lean4
        token: ${{ secrets.LEAN_PR_TESTING }}
        ref: nightly-with-mathlib
    # Merge the relevant nightly.
    - name: Fetch tags from 'lean4-nightly', and merge relevant nightly into 'nightly-with-mathlib'
      run: |
        git remote add nightly https://github.com/leanprover/lean4-nightly.git
        git fetch nightly --tags
        # Note: old jobs may run out of order, but it is safe to merge an older `nightly-YYYY-MM-DD`.
        git merge "nightly-${NIGHTLY}" --strategy-option ours --allow-unrelated-histories || true
        git push origin

    # 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 in the 'status updates' topic
        request = {
          'anchor': 'newest',
          'num_before': 1,
          'num_after': 0,
          'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Mathlib status updates'}],
          '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 Mathlib's branch#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': 'Mathlib status updates',
                'content': f"✅ The latest CI for Mathlib's branch#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@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: |
          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@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: 'Mathlib 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: 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 'Mathlib bump branch reminders' topic
            request = {
              'anchor': 'newest',
              'num_before': 1,
              'num_after': 0,
              'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Mathlib 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': 'Mathlib bump branch reminders',
                    'content': payload
                }
                result = client.send_message(request)
                print(result)
        else:
            print('No action needed.')