Post to zulip if the nightly-testing branch is failing. #139
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: ["Lean Action CI"] | |
| types: | |
| - completed | |
| jobs: | |
| handle_failure: | |
| if: ${{ github.repository == 'leanprover/cslib' && | |
| 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: 'Cslib status updates' | |
| content: | | |
| ❌ The latest CI for Cslib's [nightly-testing branch](https://github.com/leanprover/cslib/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.repository == 'leanprover/cslib' && | |
| 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}" | |
| # For now, these next two lines are commented out, but if later we want to set up benchmarking at the Speed server that can be restored. | |
| # hash="$(git rev-parse "nightly-testing-${version}")" | |
| # curl -X POST "https://speed.lean-lang.org/cslib/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 | |
| # If later we set up integrated testing so every Lean PR is tested against Cslib, | |
| # we will need to copy over some functionality from Mathlib's `nightly_detect_failure.yml` job. | |
| # 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': 'Cslib 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 Cslib's [nightly-testing branch](https://github.com/leanprover/cslib/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': 'Cslib status updates', | |
| 'content': f"✅ The latest CI for Cslib's [nightly-testing branch](https://github.com/leanprover/cslib/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: 'leanprover', | |
| repo: 'cslib' | |
| }); | |
| 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: 'leanprover', | |
| repo: 'cslib' | |
| }); | |
| 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: | | |
| const branchName = '${{ steps.latest_bump_branch.outputs.result }}'; | |
| let content = ''; | |
| let sha = ''; | |
| // Get branch SHA first for durable URL | |
| try { | |
| const branchResponse = await github.rest.repos.getBranch({ | |
| owner: 'leanprover', | |
| repo: 'cslib', | |
| branch: branchName | |
| }); | |
| sha = branchResponse.data.commit.sha; | |
| core.setOutput('branch_sha', sha); | |
| } catch (error) { | |
| core.setFailed(`Failed to get branch SHA for ${branchName}: ${error.message}`); | |
| core.setOutput('branch_name', branchName); | |
| return null; | |
| } | |
| // Retry logic for fetching content (in case of network errors) | |
| const maxRetries = 3; | |
| for (let attempt = 1; attempt <= maxRetries; attempt++) { | |
| try { | |
| const response = await github.rest.repos.getContent({ | |
| owner: context.repo.owner, | |
| repo: context.repo.repo, | |
| path: 'lean-toolchain', | |
| ref: branchName | |
| }); | |
| content = Buffer.from(response.data.content, 'base64').toString().trim(); | |
| if (content) { | |
| break; // Success, exit retry loop | |
| } else if (attempt < maxRetries) { | |
| console.log(`Attempt ${attempt}: lean-toolchain content is empty, retrying...`); | |
| await new Promise(resolve => setTimeout(resolve, 2000)); // Wait 2 seconds | |
| } | |
| } catch (error) { | |
| if (attempt === maxRetries) { | |
| core.setFailed(`Failed to fetch lean-toolchain from ${branchName} after ${maxRetries} attempts: ${error.message}`); | |
| core.setOutput('branch_name', branchName); | |
| return null; | |
| } | |
| console.log(`Attempt ${attempt}: Error fetching lean-toolchain from ${branchName}, retrying... ${error.message}`); | |
| await new Promise(resolve => setTimeout(resolve, 2000)); // Wait 2 seconds | |
| } | |
| } | |
| if (!content) { | |
| core.setFailed(`lean-toolchain content is empty after ${maxRetries} attempts from branch ${branchName}`); | |
| core.setOutput('toolchain_content', '(empty)'); | |
| core.setOutput('branch_name', branchName); | |
| return null; | |
| } | |
| core.setOutput('toolchain_content', content); | |
| core.setOutput('branch_name', branchName); | |
| const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/); | |
| if (!match) { | |
| core.setFailed('Toolchain pattern did not match'); | |
| return null; | |
| } | |
| return match[1]; | |
| - 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: 'Cslib status updates' | |
| content: | | |
| ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'. | |
| **Branch:** `${{ steps.bump_version.outputs.branch_name }}` | |
| **File URL:** https://github.com/${{ github.repository }}/blob/${{ steps.bump_version.outputs.branch_sha }}/lean-toolchain | |
| **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 Cslib | |
| if: steps.check_branch.outputs.result == 'false' | |
| run: | | |
| sudo rm -rf -- * | |
| - name: Checkout Cslib 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 'Cslib bump branch reminders' topic | |
| request = { | |
| 'anchor': 'newest', | |
| 'num_before': 1, | |
| 'num_after': 0, | |
| 'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Cslib 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 Cslib 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': 'Cslib bump branch reminders', | |
| 'content': payload | |
| } | |
| result = client.send_message(request) | |
| print(result) | |
| else: | |
| print('No action needed.') |