-
Notifications
You must be signed in to change notification settings - Fork 331
361 lines (311 loc) · 13.2 KB
/
build.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
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
# DO NOT EDIT THIS FILE!!!
# This file is automatically generated by mk_build_yml.sh
# Edit build.yml.in instead and run mk_build_yml.sh to update.
# Forks of mathlib and other projects should be able to use build_fork.yml directly
# The jobs in this file run on self-hosted workers and will not be run from external forks
on:
push:
branches-ignore:
# ignore tmp branches used by bors
- 'staging.tmp*'
- 'trying.tmp*'
- 'staging*.tmp'
- 'nolints'
# ignore staging branch used by bors, this is handled by bors.yml
- 'staging'
merge_group:
name: continuous integration
jobs:
# Cancels previous runs of jobs in this file
cancel:
if: github.repository == 'leanprover-community/mathlib4'
name: 'Cancel Previous Runs (CI)'
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/[email protected]
with:
all_but_latest: true
access_token: ${{ github.token }}
style_lint:
if: github.repository == 'leanprover-community/mathlib4'
name: Lint style
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
# Run the case checker action
- name: Check Case Sensitivity
uses: credfeto/[email protected]
- name: Look for ignored files
uses: credfeto/[email protected]
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v5
with:
python-version: 3.8
- name: lint
run: |
./scripts/lint-style.sh
- name: Install bibtool
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool
- name: lint references.bib
run: |
./scripts/lint-bib.sh
check_imported:
if: github.repository == 'leanprover-community/mathlib4'
name: Check all files imported
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
run: |
./scripts/mk_all.sh
- name: check that all files are imported
run: git diff --exit-code
check_workflows:
if: github.repository == 'leanprover-community/mathlib4'
name: check workflows
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4
- name: update workflows
run: |
cd .github/workflows/
./mk_build_yml.sh
- name: check that workflows were consistent
run: git diff --exit-code
summarize_declarations:
if: github.repository == 'leanprover-community/mathlib4'
name: summarize_declarations
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- name: print_lost_declarations
run: |
## back and forth to settle a "detached head" (maybe?)
git checkout -q master
git checkout -q -
printf '### Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
build:
if: github.repository == 'leanprover-community/mathlib4'
name: Build
runs-on: pr
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
# Delete all but the 5 most recent toolchains.
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
: # Do nothing on success
else
: # Do nothing on failure, but suppress errors
fi
# The Hoskinson runners may not have jq installed, so do that now.
- name: 'Setup jq'
uses: dcarbone/[email protected]
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
- uses: actions/checkout@v4
# We update `Mathlib.lean` as a convenience here,
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
./scripts/mk_all.sh Mathlib
- name: If using a lean-pr-release toolchain, uninstall
run: |
if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
elan toolchain uninstall "$(cat lean-toolchain)"
fi
- name: print lean and lake versions
run: |
lean --version
lake --version
- name: build cache
run: |
lake build cache
- name: prune ProofWidgets .lake
run: |
# The ProofWidgets release contains not just the `.js` (which we need in order to build)
# but also `.oleans`, which may have been built with the wrong toolchain.
# This removes them.
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
rm -rf .lake/packages/proofwidgets/.lake/build/lib
rm -rf .lake/packages/proofwidgets/.lake/build/ir
- name: get cache
id: get
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
id: build
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
- name: upload cache
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
# but not if any earlier step failed or was cancelled.
# See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
if: ${{ always() && steps.get.outcome == 'success' }}
run: |
# TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
# lake exe cache commit || true
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
# lake exe cache put!
# do not try to upload files just downloaded
lake exe cache put-unpacked
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: check the cache
run: |
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
lake exe cache clean!
rm -rf .lake/build/lib/Mathlib
lake exe cache get || (sleep 1; lake exe cache get)
lake build --no-build
fi
- name: build archive
id: archive
run: |
# Note: we should not be including `Archive` and `Counterexamples` in the cache.
# We do this for now for the sake of not rebuilding them in every CI run
# even when they are not touched.
# Since `Archive` and `Counterexamples` files have very simple dependencies,
# it should be possible to determine whether they need to be built without actually
# storing and transferring oleans over the network.
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
lake exe cache get Archive.lean
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
lake exe cache put Archive.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: build counterexamples
id: counterexamples
run: |
lake exe cache get Counterexamples.lean
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
lake exe cache put Counterexamples.lean
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
- name: check for noisy stdout lines
id: noisy
run: |
buildMsgs="$(
## we exploit `lake`s replay feature: since the cache is present, running
## `lake build` will reproduce all the outputs without having to recompute
lake build Mathlib Archive Counterexamples |
## we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
## are either numbers or ?, and the "Build completed successfully." message.
## We keep the rest, which are actual outputs of the files
awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')"
if [ -n "${buildMsgs}" ]
then
printf $'%s\n' "${buildMsgs}"
exit 1
fi
- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
lake exe checkYaml
- name: verify `lake exe graph` works
run: |
lake exe graph
rm import_graph.dot
- name: test mathlib
id: test
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: lake test
- name: check for unused imports
id: shake
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
uses: liskin/gh-problem-matcher-wrap@v3
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
# Instead we run it in a cron job on master: see `lean4checker.yml`.
# Output is posted to the zulip topic
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
- name: Post comments for lean-pr-testing branch
if: always()
env:
TOKEN: ${{ secrets.LEAN_PR_TESTING }}
GITHUB_CONTEXT: ${{ toJson(github) }}
WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
BUILD_OUTCOME: ${{ steps.build.outcome }}
NOISY_OUTCOME: ${{ steps.noisy.outcome }}
ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
LINT_OUTCOME: ${{ steps.lint.outcome }}
TEST_OUTCOME: ${{ steps.test.outcome }}
run: |
scripts/lean-pr-testing-comments.sh
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- id: PR
uses: 8BitJonny/[email protected]
# TODO: this may not work properly if the same commit is pushed to multiple branches:
# https://github.com/8BitJonny/gh-get-current-pr/issues/8
with:
github-token: ${{ secrets.GITHUB_TOKEN }}
# Only return if PR is still open
filterOutClosed: true
- id: remove_labels
name: Remove "awaiting-CI"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
run: |
curl --request DELETE \
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
uses: GrantBirki/[email protected]
with:
token: ${{ secrets.AUTO_MERGE_TOKEN }}
issue-number: ${{ steps.PR.outputs.number }}
body: |
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
bors merge