Post to zulip if the nightly-testing branch is failing. #315
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: ["continuous integration"] | |
| types: | |
| - completed | |
| # Serialize reporting runs per branch so the "read last message, then post" dedup in | |
| # `report_success` can't interleave between two concurrent runs (which would double-post ✅). | |
| # Never cancel in-flight runs: `housekeeping` may be mid-push of a tag or branch. | |
| concurrency: | |
| group: nightly-detect-failure-${{ github.event.workflow_run.head_branch }} | |
| cancel-in-progress: false | |
| jobs: | |
| handle_failure: | |
| if: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && | |
| 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@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.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-mathlib' | |
| type: 'stream' | |
| topic: 'Mathlib status updates' | |
| content: | | |
| ❌ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.event.workflow_run.head_sha }}](https://github.com/${{ github.repository }}/commit/${{ github.event.workflow_run.head_sha }})). | |
| You can `git fetch; git checkout nightly-testing` and push a fix. | |
| # Post the ✅ status as a standalone job, independent of the `housekeeping` job below. | |
| # This is the user-facing health signal for the nightly-testing branch, so it must run | |
| # on every green CI regardless of the toolchain (nightly/rc/stable) and regardless of | |
| # whether any housekeeping step fails. It needs nothing but the Zulip API. | |
| report_success: | |
| if: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && | |
| github.event.workflow_run.conclusion == 'success' && | |
| github.event.workflow_run.head_branch == 'nightly-testing' }} | |
| runs-on: ubuntu-latest | |
| steps: | |
| - 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' | |
| # Use the SHA whose CI succeeded. This is the tested commit and is always available | |
| # (it does not depend on the toolchain being a nightly, unlike the old `env.SHA`, | |
| # which came from the `nightly-testing-YYYY-MM-DD` tag created in the housekeeping job). | |
| SHA: ${{ github.event.workflow_run.head_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')) | |
| success_message = f"✅ The latest CI for Mathlib's [nightly-testing branch](https://github.com/leanprover-community/mathlib4-nightly-testing/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))" | |
| # Get the recent messages from the bot in the 'status updates' topic. | |
| # We narrow by sender to ignore human replies in between. | |
| # We look at several recent messages (not just the latest) so that an intervening | |
| # 🛠️❗ housekeeping notice or ⚠️ warning posted to this same topic does not cause us | |
| # to re-post a duplicate ✅ when CI is re-run for the same SHA. | |
| bot_email = 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| request = { | |
| 'anchor': 'newest', | |
| 'num_before': 5, | |
| 'num_after': 0, | |
| 'narrow': [ | |
| {'operator': 'stream', 'operand': 'nightly-testing-mathlib'}, | |
| {'operator': 'topic', 'operand': 'Mathlib 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 any(message['content'] == success_message for message in messages): | |
| # Post the success message | |
| request = { | |
| 'type': 'stream', | |
| 'to': 'nightly-testing-mathlib', | |
| 'topic': 'Mathlib status updates', | |
| 'content': success_message | |
| } | |
| result = client.send_message(request) | |
| print(result) | |
| shell: python | |
| # Housekeeping for a green nightly-testing build: tag the commit, advance the tracking | |
| # branches, and remind/PR the bump branch. None of this is the user-facing status report | |
| # (that is `report_success` above), so when it can't run (non-nightly toolchain) or fails, | |
| # it must not silence the ✅. | |
| housekeeping: | |
| if: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && | |
| github.event.workflow_run.conclusion == 'success' && | |
| github.event.workflow_run.head_branch == 'nightly-testing' }} | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| # `pull-requests: read` is needed by the `open_bump_prs` step below, which lists open | |
| # adaptation PRs. Listing PRs on a public repo may happen to work unauthenticated, but | |
| # this job passes a `GITHUB_TOKEN` restricted by this block, so ask for the scope. | |
| pull-requests: read | |
| id-token: write | |
| steps: | |
| - name: Generate app token | |
| id: app-token | |
| uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@d6393a535c054122e507b6c5e1b2f4c31c604121 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }} | |
| key-name: mathlib-nightly-testing-app-pk | |
| azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_NIGHTLY_TESTING }} | |
| azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }} | |
| # This token is masked by the token minting action and will not be logged accidentally. | |
| - name: Checkout code | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| # Pin to the SHA whose CI just succeeded, not the current tip of `nightly-testing`, | |
| # which may have advanced while CI was running. Without this, the tag and | |
| # `nightly-testing-{green,daily}` updates below can point to an untested commit. | |
| ref: ${{ github.event.workflow_run.head_sha }} | |
| 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-green branch | |
| continue-on-error: true | |
| run: | | |
| # `nightly-testing-green` records the latest successfully built `nightly-testing` commit; | |
| # live.lean-lang.org and the prebuilt CI tools read from it. Normally a fast-forward, but | |
| # if `nightly-testing`'s history is rewritten (e.g. a toolchain reset to an rc) the branch | |
| # diverges and a plain push is rejected forever, freezing it. Recover by force-pushing, but | |
| # only when the tested commit is strictly newer than the current tip (by committer date), so | |
| # an out-of-order CI completion (older commit finishing after a newer one) can't roll back. | |
| if git push origin HEAD:nightly-testing-green; then | |
| exit 0 | |
| fi | |
| git fetch origin nightly-testing-green | |
| tip="$(git rev-parse FETCH_HEAD)" | |
| head_ct="$(git show -s --format=%ct HEAD)" | |
| tip_ct="$(git show -s --format=%ct "$tip")" | |
| if git merge-base --is-ancestor HEAD "$tip"; then | |
| echo "nightly-testing-green is ahead of the tested commit; leaving it alone." | |
| elif (( head_ct > tip_ct )); then | |
| echo "nightly-testing-green diverged; force-pushing to the newer tested commit." | |
| git push --force-with-lease=refs/heads/nightly-testing-green:"$tip" origin HEAD:nightly-testing-green | |
| else | |
| echo "nightly-testing-green is newer than the tested commit; leaving it alone." | |
| fi | |
| - name: Create a nightly-testing-YYYY-MM-DD tag | |
| id: tag | |
| run: | | |
| toolchain="$(<lean-toolchain)" | |
| if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then | |
| echo "is_nightly=true" >> "${GITHUB_OUTPUT}" | |
| 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. | |
| # The `ls-remote` check above is racy: a concurrent run can push the | |
| # tag between our check and our push. Tolerate that case. | |
| printf 'Creating tag %s from the current state of the nightly-testing branch.' "nightly-testing-${version}" | |
| git tag "nightly-testing-${version}" | |
| if ! git push origin "nightly-testing-${version}"; then | |
| if git ls-remote --tags --exit-code origin "nightly-testing-${version}" >/dev/null; then | |
| printf 'Tag nightly-testing-%s was created concurrently; continuing.' "${version}" | |
| else | |
| exit 1 | |
| fi | |
| fi | |
| # Fast-forward `nightly-testing-daily` to the tested SHA. We pin to the SHA whose CI | |
| # succeeded, which may be older than the current `nightly-testing` tip if an older | |
| # commit's CI finishes after a newer one's, so don't force-push here or we'd roll the | |
| # branch backwards. (`nightly-testing-green` is advanced, with recovery from a history | |
| # rewrite, by the `Update the nightly-testing-green branch` step above.) | |
| git push origin HEAD:nightly-testing-daily || echo "Skipping nightly-testing-daily update: not a fast-forward." | |
| 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 | |
| # nightly-testing is on a non-nightly toolchain (e.g. an rc or stable release such | |
| # as `v4.31.0-rc1`). There is no `nightly-YYYY-MM-DD` to tag, no Lean nightly to | |
| # merge, and no bump-branch reminder to compute, so we skip the rest of the | |
| # housekeeping rather than failing. The ✅ status is still posted by `report_success`. | |
| echo "is_nightly=false" >> "${GITHUB_OUTPUT}" | |
| echo "lean-toolchain '$toolchain' is not a nightly (rc/stable?); skipping tag and bump-branch reminders." | |
| fi | |
| # 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 | |
| if: steps.tag.outputs.is_nightly == 'true' | |
| id: check_branch | |
| uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 | |
| with: | |
| script: | | |
| const branchName = `bump/nightly-${process.env.NIGHTLY}`; | |
| console.log(`Looking for branch: ${branchName}`); | |
| // Use paginate to get all branches from nightly-testing repository | |
| const branches = await github.paginate(github.rest.repos.listBranches, { | |
| owner: 'leanprover-community', | |
| repo: 'mathlib4-nightly-testing' | |
| }); | |
| 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.tag.outputs.is_nightly == 'true' && 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 | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' | |
| id: latest_bump_branch | |
| uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 | |
| with: | |
| result-encoding: string | |
| script: | | |
| const branches = await github.paginate(github.rest.repos.listBranches, { | |
| owner: 'leanprover-community', | |
| repo: 'mathlib4-nightly-testing' | |
| }); | |
| 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; | |
| # Don't stack up adaptation PRs. If an earlier `bump/nightly-YYYY-MM-DD` PR into the | |
| # current bump branch is still open, creating another one just buries it: the new branch | |
| # is cut from a `bump/v4.X.0` that is missing the earlier adaptations, so the merge | |
| # conflicts and the humans get a daily "creation failed" notice that says nothing about | |
| # the real blocker. Instead we don't attempt at all, and say so (see | |
| # `Report skipped bump-branch attempt to Zulip` below). | |
| - name: Check for an open bump/nightly-YYYY-MM-DD PR into the current bump branch | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' | |
| id: open_bump_prs | |
| uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 | |
| with: | |
| script: | | |
| const repo = 'mathlib4-nightly-testing'; | |
| const base = '${{ steps.latest_bump_branch.outputs.result }}'; | |
| const prs = await github.paginate(github.rest.pulls.list, { | |
| owner: 'leanprover-community', | |
| repo, | |
| state: 'open', | |
| base | |
| }); | |
| // Only branches in the nightly-testing repo itself count: a branch named | |
| // `bump/nightly-*` in someone's fork must not be able to stall the automation. | |
| // Drafts do count; a draft adaptation PR still needs to land before the next one. | |
| const blocking = prs | |
| .filter(pr => pr.head.repo && pr.head.repo.full_name === `leanprover-community/${repo}`) | |
| .filter(pr => /^bump\/nightly-\d{4}-\d{2}-\d{2}(-rev\d+)?$/.test(pr.head.ref)) | |
| .sort((a, b) => a.number - b.number); | |
| for (const pr of blocking) { | |
| console.log(`Blocking: #${pr.number} ${pr.head.ref}`); | |
| } | |
| if (!blocking.length) { | |
| console.log(`No open bump/nightly-* PR into ${base}.`); | |
| } | |
| core.setOutput('found', blocking.length ? 'true' : 'false'); | |
| core.setOutput('count', String(blocking.length)); | |
| // Render the list here so the reporting step below needs no JSON parsing. | |
| core.setOutput('list_md', blocking | |
| .map(pr => `* [nightly#${pr.number}](${pr.html_url}) ${pr.title}`) | |
| .join('\n')); | |
| core.setOutput('first_md', blocking.length | |
| ? `[nightly#${blocking[0].number}](${blocking[0].html_url})` | |
| : ''); | |
| - name: Fetch lean-toolchain from latest bump branch | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == 'false' | |
| id: bump_version | |
| uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 | |
| 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-community', | |
| repo: 'mathlib4-nightly-testing', | |
| 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}(?:-rev\d+)?)/); | |
| 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: steps.tag.outputs.is_nightly == 'true' && failure() && steps.bump_version.outcome == 'failure' | |
| uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.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-mathlib' | |
| type: 'stream' | |
| topic: 'Mathlib 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(-revK)'. | |
| **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. | |
| # Deliberately not conditioned on `open_bump_prs`: both the creation path and the | |
| # `Report skipped bump-branch attempt to Zulip` step below need the Zulip client. | |
| - name: Setup Zulip client and git identity | |
| if: steps.tag.outputs.is_nightly == 'true' && 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: Report skipped bump-branch attempt to Zulip | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == 'true' | |
| env: | |
| BUMP_BRANCH: ${{ steps.latest_bump_branch.outputs.result }} | |
| BLOCKING_COUNT: ${{ steps.open_bump_prs.outputs.count }} | |
| BLOCKING_LIST: ${{ steps.open_bump_prs.outputs.list_md }} | |
| BLOCKING_FIRST: ${{ steps.open_bump_prs.outputs.first_md }} | |
| shell: python | |
| run: | | |
| import os | |
| import zulip | |
| client = zulip.Client(config_file="~/.zuliprc") | |
| current_version = os.getenv('NIGHTLY') | |
| bump_branch = os.getenv('BUMP_BRANCH') | |
| count = int(os.getenv('BLOCKING_COUNT')) | |
| blocking_list = os.getenv('BLOCKING_LIST') | |
| blocking_first = os.getenv('BLOCKING_FIRST') | |
| # This marker is the dedup key, and is what distinguishes this message from the | |
| # `Automatic PR creation failed` reminder that shares this topic. Don't reword it | |
| # without updating the `should_post` test below. | |
| marker = 'Bump branch creation skipped' | |
| preamble = ( | |
| f"⏸️ **{marker}.** We did not attempt to create a bump branch merging " | |
| f"`nightly-testing` with the `nightly-{current_version}` toolchain into " | |
| f"`{bump_branch}`, because " | |
| ) | |
| if count == 1: | |
| payload = ( | |
| preamble | |
| + f"the last such PR at {blocking_first} has not yet been merged. " | |
| "Please review and/or merge this first; we'll then attempt to create a new " | |
| "bump branch for the next nightly." | |
| ) | |
| else: | |
| payload = ( | |
| preamble | |
| + "these earlier bump PRs have not yet been merged:\n\n" | |
| + blocking_list | |
| + "\n\nPlease review and/or merge these first, oldest first; we'll then " | |
| "attempt to create a new bump branch for the next nightly." | |
| ) | |
| # Post at most once per nightly date and bump branch: this job runs on every green CI | |
| # of `nightly-testing`, several times a day. We narrow by sender to ignore human | |
| # replies, and look back over several messages rather than just the newest, so that an | |
| # intervening `Automatic PR creation failed` notice cannot hide our own last one. | |
| bot_email = 'github-mathlib4-bot@leanprover.zulipchat.com' | |
| response = client.get_messages({ | |
| 'anchor': 'newest', | |
| 'num_before': 20, | |
| 'num_after': 0, | |
| 'narrow': [ | |
| {'operator': 'stream', 'operand': 'nightly-testing-mathlib'}, | |
| {'operator': 'topic', 'operand': 'Mathlib bump branch reminders'}, | |
| {'operator': 'sender', 'operand': bot_email} | |
| ], | |
| 'apply_markdown': False # Otherwise the content test below fails. | |
| }) | |
| # Newest first, and only messages of our own kind. | |
| previous = [m for m in reversed(response['messages']) if marker in m['content']] | |
| last_skip_message = previous[0] if previous else None | |
| should_post = True | |
| if last_skip_message: | |
| last_content = last_skip_message['content'] | |
| if (f'`nightly-{current_version}`' in last_content | |
| and f'`{bump_branch}`' in last_content): | |
| should_post = False | |
| print(f'Already posted for nightly {current_version} and {bump_branch}') | |
| if should_post: | |
| if last_skip_message: | |
| print("###### Last message of this kind:") | |
| print(last_skip_message['content']) | |
| print("###### Current message:") | |
| print(payload) | |
| result = client.send_message({ | |
| 'type': 'stream', | |
| 'to': 'nightly-testing-mathlib', | |
| 'topic': 'Mathlib bump branch reminders', | |
| 'content': payload | |
| }) | |
| print(result) | |
| # The Zulip client reports API-level failures in the return value rather than by | |
| # raising, so a rejected message would otherwise be lost with the job still green. | |
| if result.get('result') != 'success': | |
| raise RuntimeError( | |
| f"Zulip send failed: {result.get('code')}: {result.get('msg')}") | |
| - name: Clean workspace and checkout Mathlib4 | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == '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 Mathlib4 checkout | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == 'false' | |
| id: app-token-2 | |
| uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@d6393a535c054122e507b6c5e1b2f4c31c604121 | |
| with: | |
| app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }} | |
| key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }} | |
| key-name: mathlib-nightly-testing-app-pk | |
| azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_NIGHTLY_TESTING }} | |
| azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }} | |
| - name: Checkout Mathlib4 repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == '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: Checkout local actions | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == 'false' | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| ref: ${{ github.workflow_sha }} | |
| fetch-depth: 1 | |
| sparse-checkout: .github/actions | |
| path: workflow-actions | |
| - name: Get mathlib-ci | |
| id: get_mathlib_ci | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == 'false' | |
| uses: ./workflow-actions/.github/actions/get-mathlib-ci | |
| - name: Attempt automatic PR creation | |
| id: auto_pr | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == '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}" | |
| "${CI_SCRIPTS_DIR}/nightly/create-adaptation-pr.sh" --bumpversion="${bump_branch_suffix}" --nightlydate="${current_version}" --nightlysha="${SHA}" --auto=yes | |
| - name: Fallback to manual instructions | |
| if: steps.tag.outputs.is_nightly == 'true' && steps.auto_pr.outcome == 'failure' && steps.check_branch.outputs.result == 'false' && steps.open_bump_prs.outputs.found == '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 'Mathlib 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-mathlib'}, | |
| {'operator': 'topic', 'operand': 'Mathlib 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:\n\n" | |
| payload += f"```bash\ntmpscript=$(mktemp)\nwget -qO \"$tmpscript\" https://raw.githubusercontent.com/leanprover-community/mathlib-ci/${{ steps.get_mathlib_ci.outputs.ref }}/scripts/nightly/create-adaptation-pr.sh\nchmod +x \"$tmpscript\"\ntmpdir=$(mktemp -d)\ngit clone --filter=blob:none https://github.com/leanprover-community/mathlib4 \"$tmpdir\"\ncd \"$tmpdir\"\n\"$tmpscript\" --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. | |
| # This topic also carries `Bump branch creation skipped` messages, posted by the | |
| # step of that name above, and those quote the titles of the blocking PRs. Require | |
| # this message's own marker before trusting the field regexes below, so that a PR | |
| # title cannot make a skip notice look like an already-reported failure. | |
| 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}(?:-rev\d+)?)', last_content) | |
| # `[\d.]+` used to swallow the sentence-ending period here, so `branch_match` | |
| # never equalled the bare branch name and this dedup never fired: several | |
| # nightly dates in this topic have two identical reminders as a result. | |
| branch_match = re.search(r'PR that to (bump/v\d+\.\d+\.\d+)', last_content) | |
| if 'Automatic PR creation' in last_content and 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-mathlib', | |
| 'topic': 'Mathlib bump branch reminders', | |
| 'content': payload | |
| } | |
| result = client.send_message(request) | |
| print(result) | |
| else: | |
| print('No action needed.') | |
| # If any non-`continue-on-error` housekeeping step above failed, surface it loudly to the | |
| # status topic. Without this, a green CI whose housekeeping breaks (tagging, bump | |
| # reminders) would fail silently, since `report_success` is a separate job. | |
| # We stay quiet when the failure is the malformed-bump-branch case, which already has its | |
| # own dedicated ⚠️ warning step above (otherwise we would double-post). | |
| - name: Report housekeeping failure to Zulip | |
| if: failure() && steps.bump_version.outcome != 'failure' | |
| uses: zulip/github-actions-zulip/send-message@f675f2b4eb2a95fae974215476dcb7ad8dfeff6b # v2.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-mathlib' | |
| type: 'stream' | |
| topic: 'Mathlib status updates' | |
| content: | | |
| 🛠️❗ Housekeeping for the nightly-testing branch [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) ([${{ github.event.workflow_run.head_sha }}](https://github.com/${{ github.repository }}/commit/${{ github.event.workflow_run.head_sha }})). | |
| CI passed (success reporting is handled by the separate `report_success` job), but tagging / bump-branch reminders did not complete. Please check the run. |