Skip to content

Commit 066a706

Browse files
mattrobballmattrobball
committed
Merge branch 'master' into mrb/kaehler_speedup
2 parents 9905ec3 + a526f3e commit 066a706

3,148 files changed

Lines changed: 72631 additions & 36491 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/bors.yml‎

Lines changed: 87 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -37,11 +37,12 @@ jobs:
3737
3838
- uses: actions/checkout@v3
3939

40-
- name: Install bibtool
41-
if: ${{ 'bors' == 'ubuntu-latest' }}
42-
run: |
43-
sudo apt-get update
44-
sudo apt-get install -y bibtool
40+
# Run the case checker action
41+
- name: Check Case Sensitivity
42+
uses: credfeto/action-case-checker@v1.3.0
43+
44+
- name: Look for ignored files
45+
uses: credfeto/action-no-ignored-files@v1.1.0
4546

4647
- name: install Python
4748
if: ${{ 'bors' == 'ubuntu-latest' }}
@@ -53,6 +54,12 @@ jobs:
5354
run: |
5455
./scripts/lint-style.sh
5556
57+
- name: Install bibtool
58+
if: ${{ 'bors' == 'ubuntu-latest' }}
59+
run: |
60+
sudo apt-get update
61+
sudo apt-get install -y bibtool
62+
5663
- name: lint references.bib
5764
run: |
5865
./scripts/lint-bib.sh
@@ -99,11 +106,19 @@ jobs:
99106
- name: cleanup
100107
run: |
101108
find . -name . -o -prune -exec rm -rf -- {} +
109+
# Delete all but the 10 most recent toolchains.
110+
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
111+
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
112+
cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
113+
114+
# The Hoskinson runners may not have jq installed, so do that now.
115+
- name: 'Setup jq'
116+
uses: dcarbone/install-jq-action@v1.0.1
102117

103118
- name: install elan
104119
run: |
105120
set -o pipefail
106-
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
121+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
107122
./elan-init -y --default-toolchain none
108123
echo "$HOME/.elan/bin" >> $GITHUB_PATH
109124
@@ -115,12 +130,22 @@ jobs:
115130
run: |
116131
find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
117132
133+
- name: If using a lean-pr-release toolchain, uninstall
134+
run: |
135+
if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
136+
echo "Uninstalling transient toolchain `cat lean-toolchain`"
137+
elan toolchain uninstall `cat lean-toolchain`
138+
fi
139+
118140
- name: get cache
119141
run: |
120142
lake exe cache clean
121-
lake exe cache get
143+
# We've been seeing many failures at this step recently because of network errors.
144+
# As a band-aid, we try twice.
145+
lake exe cache get || lake exe cache get
122146
123147
- name: build mathlib
148+
id: build
124149
uses: liskin/gh-problem-matcher-wrap@v2
125150
with:
126151
linters: gcc
@@ -137,30 +162,70 @@ jobs:
137162
- name: upload cache
138163
if: always()
139164
run: |
165+
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
166+
# lake exe cache pack! || true
140167
lake exe cache commit || true
141168
lake exe cache put || true
142169
env:
143170
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
144171

172+
- name: check the cache
173+
run: |
174+
lake exe cache get
175+
# We pipe the output of `lake build` to a file,
176+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
177+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
178+
145179
- name: build archive
146-
run: lake build Archive
180+
run: |
181+
# Note: we should not be including `Archive` and `Countexamples` in the cache.
182+
# We do this for now for the sake of not rebuilding them in every CI run
183+
# even when they are not touched.
184+
# Since `Archive` and `Counterexamples` files have very simple dependencies,
185+
# it should be possible to determine whether they need to be built without actually
186+
# storing and transferring oleans over the network.
187+
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
188+
lake exe cache get Archive.lean
189+
lake build Archive
190+
lake exe cache put Archive.lean
191+
env:
192+
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
147193

148194
- name: build counterexamples
149-
run: lake build Counterexamples
195+
run: |
196+
lake exe cache get Counterexamples.lean
197+
lake build Counterexamples
198+
lake exe cache put Counterexamples.lean
199+
env:
200+
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
150201

151202
- name: check declarations in db files
152203
run: |
153204
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
154-
build/bin/checkYaml
205+
lake exe checkYaml
155206
156207
- name: test mathlib
208+
id: test
157209
run: make -j 8 test
158210

159211
- name: lint mathlib
212+
id: lint
160213
uses: liskin/gh-problem-matcher-wrap@v2
161214
with:
162215
linters: gcc
163-
run: env LEAN_ABORT_ON_PANIC=1 make lint
216+
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
217+
218+
- name: Post comments for lean-pr-testing branch
219+
if: always()
220+
env:
221+
TOKEN: ${{ secrets.LEAN_PR_TESTING }}
222+
GITHUB_CONTEXT: ${{ toJson(github) }}
223+
WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
224+
LINT_OUTCOME: ${{ steps.lint.outcome }}
225+
TEST_OUTCOME: ${{ steps.test.outcome }}
226+
BUILD_OUTCOME: ${{ steps.build.outcome }}
227+
run: |
228+
scripts/lean-pr-testing-comments.sh
164229
165230
final:
166231
name: Post-CI job
@@ -187,3 +252,14 @@ jobs:
187252
curl --request DELETE \
188253
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
189254
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
255+
256+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
257+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
258+
uses: GrantBirki/comment@v2.0.1
259+
with:
260+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
261+
issue-number: ${{ steps.PR.outputs.number }}
262+
body: |
263+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
264+
265+
bors merge

‎.github/workflows/build.yml‎

Lines changed: 87 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -43,11 +43,12 @@ jobs:
4343
4444
- uses: actions/checkout@v3
4545

46-
- name: Install bibtool
47-
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
48-
run: |
49-
sudo apt-get update
50-
sudo apt-get install -y bibtool
46+
# Run the case checker action
47+
- name: Check Case Sensitivity
48+
uses: credfeto/action-case-checker@v1.3.0
49+
50+
- name: Look for ignored files
51+
uses: credfeto/action-no-ignored-files@v1.1.0
5152

5253
- name: install Python
5354
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
@@ -59,6 +60,12 @@ jobs:
5960
run: |
6061
./scripts/lint-style.sh
6162
63+
- name: Install bibtool
64+
if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
65+
run: |
66+
sudo apt-get update
67+
sudo apt-get install -y bibtool
68+
6269
- name: lint references.bib
6370
run: |
6471
./scripts/lint-bib.sh
@@ -105,11 +112,19 @@ jobs:
105112
- name: cleanup
106113
run: |
107114
find . -name . -o -prune -exec rm -rf -- {} +
115+
# Delete all but the 10 most recent toolchains.
116+
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
117+
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
118+
cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +11 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"' || true
119+
120+
# The Hoskinson runners may not have jq installed, so do that now.
121+
- name: 'Setup jq'
122+
uses: dcarbone/install-jq-action@v1.0.1
108123

109124
- name: install elan
110125
run: |
111126
set -o pipefail
112-
curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
127+
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
113128
./elan-init -y --default-toolchain none
114129
echo "$HOME/.elan/bin" >> $GITHUB_PATH
115130
@@ -121,12 +136,22 @@ jobs:
121136
run: |
122137
find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
123138
139+
- name: If using a lean-pr-release toolchain, uninstall
140+
run: |
141+
if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
142+
echo "Uninstalling transient toolchain `cat lean-toolchain`"
143+
elan toolchain uninstall `cat lean-toolchain`
144+
fi
145+
124146
- name: get cache
125147
run: |
126148
lake exe cache clean
127-
lake exe cache get
149+
# We've been seeing many failures at this step recently because of network errors.
150+
# As a band-aid, we try twice.
151+
lake exe cache get || lake exe cache get
128152
129153
- name: build mathlib
154+
id: build
130155
uses: liskin/gh-problem-matcher-wrap@v2
131156
with:
132157
linters: gcc
@@ -143,30 +168,70 @@ jobs:
143168
- name: upload cache
144169
if: always()
145170
run: |
171+
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
172+
# lake exe cache pack! || true
146173
lake exe cache commit || true
147174
lake exe cache put || true
148175
env:
149176
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
150177

178+
- name: check the cache
179+
run: |
180+
lake exe cache get
181+
# We pipe the output of `lake build` to a file,
182+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
183+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
184+
151185
- name: build archive
152-
run: lake build Archive
186+
run: |
187+
# Note: we should not be including `Archive` and `Countexamples` in the cache.
188+
# We do this for now for the sake of not rebuilding them in every CI run
189+
# even when they are not touched.
190+
# Since `Archive` and `Counterexamples` files have very simple dependencies,
191+
# it should be possible to determine whether they need to be built without actually
192+
# storing and transferring oleans over the network.
193+
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
194+
lake exe cache get Archive.lean
195+
lake build Archive
196+
lake exe cache put Archive.lean
197+
env:
198+
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
153199

154200
- name: build counterexamples
155-
run: lake build Counterexamples
201+
run: |
202+
lake exe cache get Counterexamples.lean
203+
lake build Counterexamples
204+
lake exe cache put Counterexamples.lean
205+
env:
206+
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
156207

157208
- name: check declarations in db files
158209
run: |
159210
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
160-
build/bin/checkYaml
211+
lake exe checkYaml
161212
162213
- name: test mathlib
214+
id: test
163215
run: make -j 8 test
164216

165217
- name: lint mathlib
218+
id: lint
166219
uses: liskin/gh-problem-matcher-wrap@v2
167220
with:
168221
linters: gcc
169-
run: env LEAN_ABORT_ON_PANIC=1 make lint
222+
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
223+
224+
- name: Post comments for lean-pr-testing branch
225+
if: always()
226+
env:
227+
TOKEN: ${{ secrets.LEAN_PR_TESTING }}
228+
GITHUB_CONTEXT: ${{ toJson(github) }}
229+
WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
230+
LINT_OUTCOME: ${{ steps.lint.outcome }}
231+
TEST_OUTCOME: ${{ steps.test.outcome }}
232+
BUILD_OUTCOME: ${{ steps.build.outcome }}
233+
run: |
234+
scripts/lean-pr-testing-comments.sh
170235
171236
final:
172237
name: Post-CI job
@@ -193,3 +258,14 @@ jobs:
193258
curl --request DELETE \
194259
--url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
195260
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
261+
262+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
263+
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
264+
uses: GrantBirki/comment@v2.0.1
265+
with:
266+
token: ${{ secrets.AUTO_MERGE_TOKEN }}
267+
issue-number: ${{ steps.PR.outputs.number }}
268+
body: |
269+
As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
270+
271+
bors merge

0 commit comments

Comments
 (0)