Post to zulip if the nightly-testing branch is failing. #16189
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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.') |