Skip to content

Commit 82e59b7

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Trigger CI for leanprover/lean4#2603 
2 parents 144715b + 9bb8b57 commit 82e59b7

File tree

569 files changed

+10773
-5002
lines changed

Some content is hidden

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

569 files changed

+10773
-5002
lines changed

‎.github/workflows/bors.yml

+35-10
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,8 @@ jobs:
142142
lake exe cache clean
143143
# We've been seeing many failures at this step recently because of network errors.
144144
# As a band-aid, we try twice.
145-
lake exe cache get || lake exe cache get
145+
# The 'sleep 1' is small pause to let the network recover.
146+
lake exe cache get || (sleep 1; lake exe cache get)
146147
147148
- name: build mathlib
148149
id: build
@@ -165,16 +166,21 @@ jobs:
165166
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
166167
# lake exe cache pack! || true
167168
lake exe cache commit || true
168-
lake exe cache put || true
169+
# try twice in case of network errors
170+
lake exe cache put || (sleep 1; lake exe cache put) || true
169171
env:
170172
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
171173

172174
- name: check the cache
173175
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 $! ))
176+
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
177+
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
178+
if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
179+
lake exe cache get || (sleep 1; lake exe cache get)
180+
# We pipe the output of `lake build` to a file,
181+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
182+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
183+
fi
178184
179185
- name: build archive
180186
run: |
@@ -185,17 +191,18 @@ jobs:
185191
# it should be possible to determine whether they need to be built without actually
186192
# storing and transferring oleans over the network.
187193
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
188-
lake exe cache get Archive.lean
194+
# We retry twice in case of network errors.
195+
lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
189196
lake build Archive
190-
lake exe cache put Archive.lean
197+
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
191198
env:
192199
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
193200

194201
- name: build counterexamples
195202
run: |
196-
lake exe cache get Counterexamples.lean
203+
lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
197204
lake build Counterexamples
198-
lake exe cache put Counterexamples.lean
205+
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
199206
env:
200207
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
201208

@@ -204,6 +211,11 @@ jobs:
204211
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
205212
lake exe checkYaml
206213
214+
- name: verify `lake exe graph` works
215+
run: |
216+
lake exe graph
217+
rm import_graph.dot
218+
207219
- name: test mathlib
208220
id: test
209221
run: make -j 8 test
@@ -215,6 +227,19 @@ jobs:
215227
linters: gcc
216228
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
217229

230+
- name: check environments using lean4checker
231+
id: lean4checker
232+
run: |
233+
git clone https://github.com/leanprover/lean4checker
234+
cd lean4checker
235+
# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
236+
# we just keep rebuilding until it works!
237+
# I'll try to come up with something better.
238+
until lake build > /dev/null 2>&1; do :; done
239+
./test.sh
240+
cd ..
241+
lake env lean4checker/build/bin/lean4checker
242+
218243
- name: Post comments for lean-pr-testing branch
219244
if: always()
220245
env:

‎.github/workflows/build.yml

+35-10
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,8 @@ jobs:
148148
lake exe cache clean
149149
# We've been seeing many failures at this step recently because of network errors.
150150
# As a band-aid, we try twice.
151-
lake exe cache get || lake exe cache get
151+
# The 'sleep 1' is small pause to let the network recover.
152+
lake exe cache get || (sleep 1; lake exe cache get)
152153
153154
- name: build mathlib
154155
id: build
@@ -171,16 +172,21 @@ jobs:
171172
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
172173
# lake exe cache pack! || true
173174
lake exe cache commit || true
174-
lake exe cache put || true
175+
# try twice in case of network errors
176+
lake exe cache put || (sleep 1; lake exe cache put) || true
175177
env:
176178
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
177179

178180
- name: check the cache
179181
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 $! ))
182+
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
183+
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
184+
if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
185+
lake exe cache get || (sleep 1; lake exe cache get)
186+
# We pipe the output of `lake build` to a file,
187+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
188+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
189+
fi
184190
185191
- name: build archive
186192
run: |
@@ -191,17 +197,18 @@ jobs:
191197
# it should be possible to determine whether they need to be built without actually
192198
# storing and transferring oleans over the network.
193199
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
194-
lake exe cache get Archive.lean
200+
# We retry twice in case of network errors.
201+
lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
195202
lake build Archive
196-
lake exe cache put Archive.lean
203+
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
197204
env:
198205
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
199206

200207
- name: build counterexamples
201208
run: |
202-
lake exe cache get Counterexamples.lean
209+
lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
203210
lake build Counterexamples
204-
lake exe cache put Counterexamples.lean
211+
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
205212
env:
206213
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
207214

@@ -210,6 +217,11 @@ jobs:
210217
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
211218
lake exe checkYaml
212219
220+
- name: verify `lake exe graph` works
221+
run: |
222+
lake exe graph
223+
rm import_graph.dot
224+
213225
- name: test mathlib
214226
id: test
215227
run: make -j 8 test
@@ -221,6 +233,19 @@ jobs:
221233
linters: gcc
222234
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
223235

236+
- name: check environments using lean4checker
237+
id: lean4checker
238+
run: |
239+
git clone https://github.com/leanprover/lean4checker
240+
cd lean4checker
241+
# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
242+
# we just keep rebuilding until it works!
243+
# I'll try to come up with something better.
244+
until lake build > /dev/null 2>&1; do :; done
245+
./test.sh
246+
cd ..
247+
lake env lean4checker/build/bin/lean4checker
248+
224249
- name: Post comments for lean-pr-testing branch
225250
if: always()
226251
env:

‎.github/workflows/build.yml.in

+35-10
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,8 @@ jobs:
128128
lake exe cache clean
129129
# We've been seeing many failures at this step recently because of network errors.
130130
# As a band-aid, we try twice.
131-
lake exe cache get || lake exe cache get
131+
# The 'sleep 1' is small pause to let the network recover.
132+
lake exe cache get || (sleep 1; lake exe cache get)
132133

133134
- name: build mathlib
134135
id: build
@@ -151,16 +152,21 @@ jobs:
151152
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
152153
# lake exe cache pack! || true
153154
lake exe cache commit || true
154-
lake exe cache put || true
155+
# try twice in case of network errors
156+
lake exe cache put || (sleep 1; lake exe cache put) || true
155157
env:
156158
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
157159

158160
- name: check the cache
159161
run: |
160-
lake exe cache get
161-
# We pipe the output of `lake build` to a file,
162-
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
163-
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
162+
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
163+
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
164+
if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
165+
lake exe cache get || (sleep 1; lake exe cache get)
166+
# We pipe the output of `lake build` to a file,
167+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
168+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
169+
fi
164170

165171
- name: build archive
166172
run: |
@@ -171,17 +177,18 @@ jobs:
171177
# it should be possible to determine whether they need to be built without actually
172178
# storing and transferring oleans over the network.
173179
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
174-
lake exe cache get Archive.lean
180+
# We retry twice in case of network errors.
181+
lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
175182
lake build Archive
176-
lake exe cache put Archive.lean
183+
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
177184
env:
178185
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
179186

180187
- name: build counterexamples
181188
run: |
182-
lake exe cache get Counterexamples.lean
189+
lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
183190
lake build Counterexamples
184-
lake exe cache put Counterexamples.lean
191+
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
185192
env:
186193
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
187194

@@ -190,6 +197,11 @@ jobs:
190197
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
191198
lake exe checkYaml
192199

200+
- name: verify `lake exe graph` works
201+
run: |
202+
lake exe graph
203+
rm import_graph.dot
204+
193205
- name: test mathlib
194206
id: test
195207
run: make -j 8 test
@@ -201,6 +213,19 @@ jobs:
201213
linters: gcc
202214
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
203215

216+
- name: check environments using lean4checker
217+
id: lean4checker
218+
run: |
219+
git clone https://github.com/leanprover/lean4checker
220+
cd lean4checker
221+
# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
222+
# we just keep rebuilding until it works!
223+
# I'll try to come up with something better.
224+
until lake build > /dev/null 2>&1; do :; done
225+
./test.sh
226+
cd ..
227+
lake env lean4checker/build/bin/lean4checker
228+
204229
- name: Post comments for lean-pr-testing branch
205230
if: always()
206231
env:

‎.github/workflows/build_fork.yml

+35-10
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,8 @@ jobs:
146146
lake exe cache clean
147147
# We've been seeing many failures at this step recently because of network errors.
148148
# As a band-aid, we try twice.
149-
lake exe cache get || lake exe cache get
149+
# The 'sleep 1' is small pause to let the network recover.
150+
lake exe cache get || (sleep 1; lake exe cache get)
150151
151152
- name: build mathlib
152153
id: build
@@ -169,16 +170,21 @@ jobs:
169170
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
170171
# lake exe cache pack! || true
171172
lake exe cache commit || true
172-
lake exe cache put || true
173+
# try twice in case of network errors
174+
lake exe cache put || (sleep 1; lake exe cache put) || true
173175
env:
174176
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
175177

176178
- name: check the cache
177179
run: |
178-
lake exe cache get
179-
# We pipe the output of `lake build` to a file,
180-
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
181-
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
180+
# Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
181+
# the cache mechanism is unreliable, so we don't test it if we are on such a branch.
182+
if [[ ! `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
183+
lake exe cache get || (sleep 1; lake exe cache get)
184+
# We pipe the output of `lake build` to a file,
185+
# and if we find " Building Mathlib" in that file we kill `lake build`, and error.
186+
lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
187+
fi
182188
183189
- name: build archive
184190
run: |
@@ -189,17 +195,18 @@ jobs:
189195
# it should be possible to determine whether they need to be built without actually
190196
# storing and transferring oleans over the network.
191197
# Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
192-
lake exe cache get Archive.lean
198+
# We retry twice in case of network errors.
199+
lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
193200
lake build Archive
194-
lake exe cache put Archive.lean
201+
lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
195202
env:
196203
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
197204

198205
- name: build counterexamples
199206
run: |
200-
lake exe cache get Counterexamples.lean
207+
lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
201208
lake build Counterexamples
202-
lake exe cache put Counterexamples.lean
209+
lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
203210
env:
204211
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
205212

@@ -208,6 +215,11 @@ jobs:
208215
python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
209216
lake exe checkYaml
210217
218+
- name: verify `lake exe graph` works
219+
run: |
220+
lake exe graph
221+
rm import_graph.dot
222+
211223
- name: test mathlib
212224
id: test
213225
run: make -j 8 test
@@ -219,6 +231,19 @@ jobs:
219231
linters: gcc
220232
run: env LEAN_ABORT_ON_PANIC=1 lake exe runMathlibLinter
221233

234+
- name: check environments using lean4checker
235+
id: lean4checker
236+
run: |
237+
git clone https://github.com/leanprover/lean4checker
238+
cd lean4checker
239+
# Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
240+
# we just keep rebuilding until it works!
241+
# I'll try to come up with something better.
242+
until lake build > /dev/null 2>&1; do :; done
243+
./test.sh
244+
cd ..
245+
lake env lean4checker/build/bin/lean4checker
246+
222247
- name: Post comments for lean-pr-testing branch
223248
if: always()
224249
env:

‎Archive/Imo/Imo2021Q1.lean

+3-2
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ Then, by the Pigeonhole principle, at least two numbers in the triplet must lie
4040
which finishes the proof.
4141
-/
4242

43+
open Finset
4344

4445
namespace Imo2021Q1
4546

@@ -123,8 +124,8 @@ theorem imo2021_q1 :
123124
have hBsub : B ⊆ Finset.Icc n (2 * n) := by
124125
intro c hcB; simpa only [Finset.mem_Icc] using h₂ c hcB
125126
have hB' : 2 * 1 < (B ∩ (Finset.Icc n (2 * n) \ A) ∪ B ∩ A).card := by
126-
rw [← Finset.inter_distrib_left, Finset.sdiff_union_self_eq_union,
127-
Finset.union_eq_left_iff_subset.mpr hA, (Finset.inter_eq_left_iff_subset _ _).mpr hBsub]
127+
rw [←inter_distrib_left, sdiff_union_self_eq_union, union_eq_left.2 hA,
128+
inter_eq_left.2 hBsub]
128129
exact Nat.succ_le_iff.mp hB
129130
-- Since B has cardinality greater or equal to 3, there must exist a subset C ⊆ B such that
130131
-- for any A ⊆ [n, 2n], either C ⊆ A or C ⊆ [n, 2n] \ A and C has cardinality greater

0 commit comments

Comments
 (0)