forked from leanprover-community/mathlib3
-
Notifications
You must be signed in to change notification settings - Fork 0
248 lines (206 loc) · 8.07 KB
/
build_fork.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
# 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 GitHub-hosted workers and will only 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.*'
name: continuous integration (mathlib forks)
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/[email protected]
with:
all_but_latest: true
access_token: ${{ github.token }}
style_lint:
if: github.repository != 'leanprover-community/mathlib'
name: Lint style (fork)
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- name: install Python
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
uses: actions/setup-python@v2
with:
python-version: 3.8
- name: lint
run: |
./scripts/lint-style.sh
build:
if: github.repository != 'leanprover-community/mathlib'
name: Build mathlib (fork)
runs-on: ubuntu-latest
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@v2
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: ${{ ! 0 }}
uses: actions/setup-python@v1
with:
python-version: 3.8
- name: try to find olean cache
run: ./scripts/fetch_olean_cache.sh
- name: leanpkg build
id: build
run: |
leanpkg configure
echo "::set-output name=started::true"
lean --json -T100000 --make src | python3 scripts/detect_errors.py
lean --json -T100000 --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 "::set-output name=artifact_name::precompiled-mathlib-$short_lean_version-$git_hash"
- 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' && ${{ 0 }}
run: rm /tmp/tmp-* || true
lint:
name: Lint mathlib (fork)
runs-on: ubuntu-latest
needs: build
# skip on master branch
if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
steps:
- name: clean build directory
if: ${{ 0 }}
run: rm -rf ./* ./.??*
- name: retrieve build
uses: actions/download-artifact@v2
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/Kha/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
tests:
name: Run tests (fork)
runs-on: ubuntu-latest
needs: build
# skip on master branch
if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'
steps:
- name: clean build directory
if: ${{ 0 }}
run: rm -rf ./* ./.??*
- name: retrieve build
uses: actions/download-artifact@v2
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/Kha/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: ${{ ! 0 }}
uses: actions/setup-python@v1
with:
python-version: 3.8
- name: install Python dependencies
if: ${{ ! 0 }}
run: python3 -m pip install --upgrade pip pyyaml
- name: tests
run: |
set -o pipefail
lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py
- uses: actions/setup-java@v2
if: ${{ ! 0 }}
with:
distribution: 'adopt'
java-version: '16'
- name: install trepplein
run: |
trepplein_version=1.0
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
final:
name: Post-CI job (fork)
if: github.repository != 'leanprover-community/mathlib'
needs: [style_lint, build, lint, tests]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- 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 }}'