-
Notifications
You must be signed in to change notification settings - Fork 251
200 lines (162 loc) · 6.17 KB
/
bors.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
# 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:
- staging
name: continuous integration (staging)
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/cancel-workflow-action@0.11.0
with:
all_but_latest: true
access_token: ${{ github.token }}
style_lint:
if: github.repository == 'leanprover-community/mathlib4'
name: Lint style
runs-on: bors
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v3
- name: Install bibtool
if: ${{ 'bors' == 'ubuntu-latest' }}
run: |
sudo apt-get update
sudo apt-get install -y bibtool
- name: install Python
if: ${{ 'bors' == 'ubuntu-latest' }}
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: lint
run: |
./scripts/lint-style.sh
- 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@v3
- name: update Mathlib.lean
run: |
git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
- name: update MathlibExtras.lean
run: |
git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
- name: update Mathlib/Tactic.lean
run: |
git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
- name: update Counterexamples.lean
run: |
git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
- name: update Archive.lean
run: |
git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
- name: check that all files are imported
run: git diff --exit-code
build:
if: github.repository == 'leanprover-community/mathlib4'
name: Build
runs-on: bors
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/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@v3
# 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: |
find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
- name: get cache
run: |
lake exe cache clean
lake exe cache get
- name: build mathlib
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: |
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
- name: build library_search cache
run: lake build -KCI MathlibExtras
- name: upload cache
if: always()
run: |
lake exe cache commit || true
lake exe cache put || true
env:
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
- name: build archive
run: lake build Archive
- name: build counterexamples
run: lake build Counterexamples
- name: check declarations in db files
run: |
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
build/bin/checkYaml
- name: test mathlib
run: make -j 8 test
- name: lint mathlib
uses: liskin/gh-problem-matcher-wrap@v2
with:
linters: gcc
run: env LEAN_ABORT_ON_PANIC=1 make lint
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@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 }}'
- 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/comment@v2.0.1
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