Skip to content

Post to zulip if the nightly-testing branch is failing. #92858

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

Post to zulip if the nightly-testing branch is failing. #92858

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: '[email protected]'
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 "http://speed.lean-fro.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: '[email protected]'
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: |
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 version = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/)[1];
return version;
- 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='[email protected]', 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.')