Skip to content

Commit 23e2887

Browse files
bryangingechenbryangingechen
committed
ci: rebuild until lake build --no-build succeeds
1 parent 43c857b commit 23e2887

4 files changed

Lines changed: 188 additions & 32 deletions

File tree

‎.github/build.in.yml‎

Lines changed: 47 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -205,8 +205,8 @@ jobs:
205205
run: |
206206
cd pr-branch
207207
208-
echo "Attempting: lake build --no-build Mathlib.Init (this runs under landrun)"
209-
lake build --no-build Mathlib.Init
208+
echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
209+
lake build --no-build -v Mathlib.Init
210210
211211
- name: get cache (3/3 - finalize cache operation)
212212
id: get
@@ -218,7 +218,7 @@ jobs:
218218
219219
../master-branch/.lake/build/bin/cache get
220220
else
221-
echo "WARNING: 'lake build --no-build Mathlib.Init' failed."
221+
echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
222222
echo "No cache for 'Mathlib.Init' available or it could not be prepared."
223223
fi
224224
@@ -248,6 +248,17 @@ jobs:
248248
echo "curl to example.com failed as expected - landrun network isolation is working"
249249
fi
250250
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
251+
counter=0
252+
max_tries=5
253+
# run again in case an olean fails to build properly
254+
while ! lake build --no-build -v Mathlib; do
255+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
256+
counter=$((counter + 1))
257+
if [ $counter -ge $max_tries ]; then
258+
echo "Failed to build good oleans for Mathlib after $max_tries attempts"
259+
exit 1
260+
fi
261+
done
251262
- name: end gh-problem-match-wrap for build step
252263
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
253264
with:
@@ -297,15 +308,43 @@ jobs:
297308
298309
- name: build archive
299310
id: archive
311+
continue-on-error: true
300312
run: |
301313
cd pr-branch
302-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
314+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
315+
counter=0
316+
max_tries=5
317+
# run again in case an olean fails to build properly
318+
while ! lake build --no-build -v Archive; do
319+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
320+
counter=$((counter + 1))
321+
if [ $counter -ge $max_tries ]; then
322+
echo "Failed to build good oleans for Archive after $max_tries attempts"
323+
exit 1
324+
fi
325+
done
303326
304327
- name: build counterexamples
305328
id: counterexamples
329+
continue-on-error: true
306330
run: |
307331
cd pr-branch
308-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
332+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
333+
counter=0
334+
max_tries=5
335+
# run again in case an olean fails to build properly
336+
while ! lake build --no-build -v Archive; do
337+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
338+
counter=$((counter + 1))
339+
if [ $counter -ge $max_tries ]; then
340+
echo "Failed to build good oleans for Counterexamples after $max_tries attempts"
341+
exit 1
342+
fi
343+
done
344+
345+
- name: Check if building Archive or Counterexamples failed
346+
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
347+
run: exit 1
309348

310349
# The cache secrets are available here, so we must not run any untrusted code.
311350
- name: put archive and counterexamples cache
@@ -442,9 +481,9 @@ jobs:
442481
443482
- name: verify that everything was available in the cache
444483
run: |
445-
lake build --no-build Mathlib
446-
lake build --no-build Archive
447-
lake build --no-build Counterexamples
484+
lake build --no-build -v Mathlib
485+
lake build --no-build -v Archive
486+
lake build --no-build -v Counterexamples
448487
449488
- name: check declarations in db files
450489
run: |

‎.github/workflows/bors.yml‎

Lines changed: 47 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -215,8 +215,8 @@ jobs:
215215
run: |
216216
cd pr-branch
217217
218-
echo "Attempting: lake build --no-build Mathlib.Init (this runs under landrun)"
219-
lake build --no-build Mathlib.Init
218+
echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
219+
lake build --no-build -v Mathlib.Init
220220
221221
- name: get cache (3/3 - finalize cache operation)
222222
id: get
@@ -228,7 +228,7 @@ jobs:
228228
229229
../master-branch/.lake/build/bin/cache get
230230
else
231-
echo "WARNING: 'lake build --no-build Mathlib.Init' failed."
231+
echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
232232
echo "No cache for 'Mathlib.Init' available or it could not be prepared."
233233
fi
234234
@@ -258,6 +258,17 @@ jobs:
258258
echo "curl to example.com failed as expected - landrun network isolation is working"
259259
fi
260260
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
261+
counter=0
262+
max_tries=5
263+
# run again in case an olean fails to build properly
264+
while ! lake build --no-build -v Mathlib; do
265+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
266+
counter=$((counter + 1))
267+
if [ $counter -ge $max_tries ]; then
268+
echo "Failed to build good oleans for Mathlib after $max_tries attempts"
269+
exit 1
270+
fi
271+
done
261272
- name: end gh-problem-match-wrap for build step
262273
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
263274
with:
@@ -307,15 +318,43 @@ jobs:
307318
308319
- name: build archive
309320
id: archive
321+
continue-on-error: true
310322
run: |
311323
cd pr-branch
312-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
324+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
325+
counter=0
326+
max_tries=5
327+
# run again in case an olean fails to build properly
328+
while ! lake build --no-build -v Archive; do
329+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
330+
counter=$((counter + 1))
331+
if [ $counter -ge $max_tries ]; then
332+
echo "Failed to build good oleans for Archive after $max_tries attempts"
333+
exit 1
334+
fi
335+
done
313336
314337
- name: build counterexamples
315338
id: counterexamples
339+
continue-on-error: true
316340
run: |
317341
cd pr-branch
318-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
342+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
343+
counter=0
344+
max_tries=5
345+
# run again in case an olean fails to build properly
346+
while ! lake build --no-build -v Archive; do
347+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
348+
counter=$((counter + 1))
349+
if [ $counter -ge $max_tries ]; then
350+
echo "Failed to build good oleans for Counterexamples after $max_tries attempts"
351+
exit 1
352+
fi
353+
done
354+
355+
- name: Check if building Archive or Counterexamples failed
356+
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
357+
run: exit 1
319358

320359
# The cache secrets are available here, so we must not run any untrusted code.
321360
- name: put archive and counterexamples cache
@@ -452,9 +491,9 @@ jobs:
452491
453492
- name: verify that everything was available in the cache
454493
run: |
455-
lake build --no-build Mathlib
456-
lake build --no-build Archive
457-
lake build --no-build Counterexamples
494+
lake build --no-build -v Mathlib
495+
lake build --no-build -v Archive
496+
lake build --no-build -v Counterexamples
458497
459498
- name: check declarations in db files
460499
run: |

‎.github/workflows/build.yml‎

Lines changed: 47 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -222,8 +222,8 @@ jobs:
222222
run: |
223223
cd pr-branch
224224
225-
echo "Attempting: lake build --no-build Mathlib.Init (this runs under landrun)"
226-
lake build --no-build Mathlib.Init
225+
echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
226+
lake build --no-build -v Mathlib.Init
227227
228228
- name: get cache (3/3 - finalize cache operation)
229229
id: get
@@ -235,7 +235,7 @@ jobs:
235235
236236
../master-branch/.lake/build/bin/cache get
237237
else
238-
echo "WARNING: 'lake build --no-build Mathlib.Init' failed."
238+
echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
239239
echo "No cache for 'Mathlib.Init' available or it could not be prepared."
240240
fi
241241
@@ -265,6 +265,17 @@ jobs:
265265
echo "curl to example.com failed as expected - landrun network isolation is working"
266266
fi
267267
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
268+
counter=0
269+
max_tries=5
270+
# run again in case an olean fails to build properly
271+
while ! lake build --no-build -v Mathlib; do
272+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
273+
counter=$((counter + 1))
274+
if [ $counter -ge $max_tries ]; then
275+
echo "Failed to build good oleans for Mathlib after $max_tries attempts"
276+
exit 1
277+
fi
278+
done
268279
- name: end gh-problem-match-wrap for build step
269280
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
270281
with:
@@ -314,15 +325,43 @@ jobs:
314325
315326
- name: build archive
316327
id: archive
328+
continue-on-error: true
317329
run: |
318330
cd pr-branch
319-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
331+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
332+
counter=0
333+
max_tries=5
334+
# run again in case an olean fails to build properly
335+
while ! lake build --no-build -v Archive; do
336+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
337+
counter=$((counter + 1))
338+
if [ $counter -ge $max_tries ]; then
339+
echo "Failed to build good oleans for Archive after $max_tries attempts"
340+
exit 1
341+
fi
342+
done
320343
321344
- name: build counterexamples
322345
id: counterexamples
346+
continue-on-error: true
323347
run: |
324348
cd pr-branch
325-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
349+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
350+
counter=0
351+
max_tries=5
352+
# run again in case an olean fails to build properly
353+
while ! lake build --no-build -v Archive; do
354+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
355+
counter=$((counter + 1))
356+
if [ $counter -ge $max_tries ]; then
357+
echo "Failed to build good oleans for Counterexamples after $max_tries attempts"
358+
exit 1
359+
fi
360+
done
361+
362+
- name: Check if building Archive or Counterexamples failed
363+
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
364+
run: exit 1
326365

327366
# The cache secrets are available here, so we must not run any untrusted code.
328367
- name: put archive and counterexamples cache
@@ -459,9 +498,9 @@ jobs:
459498
460499
- name: verify that everything was available in the cache
461500
run: |
462-
lake build --no-build Mathlib
463-
lake build --no-build Archive
464-
lake build --no-build Counterexamples
501+
lake build --no-build -v Mathlib
502+
lake build --no-build -v Archive
503+
lake build --no-build -v Counterexamples
465504
466505
- name: check declarations in db files
467506
run: |

‎.github/workflows/build_fork.yml‎

Lines changed: 47 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -219,8 +219,8 @@ jobs:
219219
run: |
220220
cd pr-branch
221221
222-
echo "Attempting: lake build --no-build Mathlib.Init (this runs under landrun)"
223-
lake build --no-build Mathlib.Init
222+
echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
223+
lake build --no-build -v Mathlib.Init
224224
225225
- name: get cache (3/3 - finalize cache operation)
226226
id: get
@@ -232,7 +232,7 @@ jobs:
232232
233233
../master-branch/.lake/build/bin/cache get
234234
else
235-
echo "WARNING: 'lake build --no-build Mathlib.Init' failed."
235+
echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
236236
echo "No cache for 'Mathlib.Init' available or it could not be prepared."
237237
fi
238238
@@ -262,6 +262,17 @@ jobs:
262262
echo "curl to example.com failed as expected - landrun network isolation is working"
263263
fi
264264
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
265+
counter=0
266+
max_tries=5
267+
# run again in case an olean fails to build properly
268+
while ! lake build --no-build -v Mathlib; do
269+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
270+
counter=$((counter + 1))
271+
if [ $counter -ge $max_tries ]; then
272+
echo "Failed to build good oleans for Mathlib after $max_tries attempts"
273+
exit 1
274+
fi
275+
done
265276
- name: end gh-problem-match-wrap for build step
266277
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
267278
with:
@@ -311,15 +322,43 @@ jobs:
311322
312323
- name: build archive
313324
id: archive
325+
continue-on-error: true
314326
run: |
315327
cd pr-branch
316-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
328+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
329+
counter=0
330+
max_tries=5
331+
# run again in case an olean fails to build properly
332+
while ! lake build --no-build -v Archive; do
333+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Archive"
334+
counter=$((counter + 1))
335+
if [ $counter -ge $max_tries ]; then
336+
echo "Failed to build good oleans for Archive after $max_tries attempts"
337+
exit 1
338+
fi
339+
done
317340
318341
- name: build counterexamples
319342
id: counterexamples
343+
continue-on-error: true
320344
run: |
321345
cd pr-branch
322-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
346+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
347+
counter=0
348+
max_tries=5
349+
# run again in case an olean fails to build properly
350+
while ! lake build --no-build -v Archive; do
351+
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail Counterexamples"
352+
counter=$((counter + 1))
353+
if [ $counter -ge $max_tries ]; then
354+
echo "Failed to build good oleans for Counterexamples after $max_tries attempts"
355+
exit 1
356+
fi
357+
done
358+
359+
- name: Check if building Archive or Counterexamples failed
360+
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
361+
run: exit 1
323362

324363
# The cache secrets are available here, so we must not run any untrusted code.
325364
- name: put archive and counterexamples cache
@@ -456,9 +495,9 @@ jobs:
456495
457496
- name: verify that everything was available in the cache
458497
run: |
459-
lake build --no-build Mathlib
460-
lake build --no-build Archive
461-
lake build --no-build Counterexamples
498+
lake build --no-build -v Mathlib
499+
lake build --no-build -v Archive
500+
lake build --no-build -v Counterexamples
462501
463502
- name: check declarations in db files
464503
run: |

0 commit comments

Comments
 (0)