-
Notifications
You must be signed in to change notification settings - Fork 297
286 lines (238 loc) · 9.47 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
# 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'
# do not build lean-x.y.z branch used by leanpkg
- 'lean-3.*'
# ignore staging branch used by bors, this is handled by bors.yml
- 'staging'
name: continuous integration
jobs:
# Cancels previous runs of jobs in this file
cancel:
if: github.repository == 'leanprover-community/mathlib'
name: 'Cancel Previous Runs (CI)'
runs-on: ubuntu-latest
# timeout-minutes: 3
steps:
- uses: styfle/cancel-workflow-action@0.11.0
with:
all_but_latest: true
access_token: ${{ github.token }}
style_lint:
if: github.repository == 'leanprover-community/mathlib'
name: Lint style
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- name: Install bibtool
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: lint style
run: |
./scripts/lint-style.sh
- name: lint references.bib
run: |
./scripts/lint-bib.sh
build:
if: github.repository == 'leanprover-community/mathlib'
name: Build mathlib
runs-on: pr
env:
# number of commits to check for olean cache
GIT_HISTORY_DEPTH: 20
outputs:
artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
steps:
- uses: actions/checkout@v3
with:
fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: try to find olean cache
run: ./scripts/fetch_olean_cache.sh
- name: leanpkg build
id: build
run: |
set -o pipefail
leanpkg configure
echo "started=true" >> $GITHUB_OUTPUT
lean --json -T100000 --make src | python3 scripts/detect_errors.py
lean --json -T400000 --make src | python3 scripts/detect_errors.py
- name: push release to azure
if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
run: |
archive_name="$(git rev-parse HEAD).tar.gz"
find src/ -name "*.olean" -o -name ".noisy_files" | tar czf "$archive_name" -T -
azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
archive_name="$(git rev-parse HEAD).tar.xz"
find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
- name: setup precompiled zip file
if: always() && steps.build.outputs.started == 'true'
id: setup_precompiled
run: |
touch workspace.tar
tar -cf workspace.tar --exclude=*.tar* .
git_hash="$(git log -1 --pretty=format:%h)"
echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT
- name: upload precompiled mathlib zip file
if: always() && steps.build.outputs.started == 'true'
uses: actions/upload-artifact@v2
with:
name: ${{ steps.setup_precompiled.outputs.artifact_name }}
path: workspace.tar
- name: cleanup after upload step
# cf. https://github.com/actions/upload-artifact/issues/256
if: always() && steps.build.outputs.started == 'true' && ${{ 1 }}
run: rm /tmp/tmp-* || true
- name: clean up working directory and elan
if: always() && ${{ 1 }}
run: rm -rf * $HOME/.elan
lint:
name: Lint mathlib
runs-on: pr
needs: build
# skip on master branch
if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
steps:
- name: clean build directory
if: ${{ 1 }}
run: rm -rf ./* ./.??*
- name: retrieve build
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}
- name: untar build
run: tar -xf workspace.tar
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: lint
run: |
./scripts/mk_all.sh
lean --run scripts/lint_mathlib.lean --github
- name: clean up working directory and elan
if: always() && ${{ 1 }}
run: rm -rf * $HOME/.elan
tests:
name: Run tests
runs-on: pr
needs: build
# skip on master branch
if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
steps:
- name: clean build directory
if: ${{ 1 }}
run: rm -rf ./* ./.??*
- name: retrieve build
uses: actions/download-artifact@v3
with:
name: ${{ needs.build.outputs.artifact_name }}
- name: untar build
run: tar -xf workspace.tar
- name: install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: install Python
if: ${{ ! 1 }}
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: install Python dependencies
if: ${{ ! 1 }}
run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools
- name: tests
run: |
set -o pipefail
lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
- name: check archive and counterexample directories have unique identifiers
run: |
pip install mathlibtools
(cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
(cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
python -m mathlibtools.leanproject mk-all
echo "import all" >> all_all.lean
echo "import counterexamples_all" >> all_all.lean
echo "import archive_all" >> all_all.lean
echo "path ./archive" >> leanpkg.path
echo "path ./counterexamples" >> leanpkg.path
lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py
- uses: actions/setup-java@v2
if: ${{ ! 1 }}
with:
distribution: 'adopt'
java-version: '16'
- name: install trepplein
run: |
trepplein_version=1.1
wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
unzip trepplein-$trepplein_version.zip
echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH
- name: export as low-level text file
run: lean --recursive --export=mathlib.txt src/
- name: trepplein
run: trepplein mathlib.txt
- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
bash scripts/mk_all.sh
lean --run scripts/yaml_check.lean
- name: clean up working directory and elan
if: always() && ${{ 1 }}
run: rm -rf * $HOME/.elan
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib'
needs: [style_lint, build, lint, tests]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- id: PR
uses: 8BitJonny/gh-get-current-pr@2.2.0
# 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 }}'