Post to zulip if the nightly-testing branch is failing. #13681
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: 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: ${{ 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}" | |
| 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 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 # 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 -- * | |
| - 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: ${{ secrets.NIGHTLY_TESTING }} | |
| - 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: ${{ secrets.NIGHTLY_TESTING }} | |
| 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 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 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/', '') | |
| 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" | |
| # 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.') |