-
Notifications
You must be signed in to change notification settings - Fork 342
236 lines (221 loc) · 10.7 KB
/
nightly_detect_failure.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
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: 'github-mathlib4-bot@leanprover.zulipchat.com'
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: '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': '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='github-mathlib4-bot@leanprover.zulipchat.com', 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.')