Skip to content

Commit 907b351

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#8947 
2 parents 14b9014 + a7a2298 commit 907b351

File tree

334 files changed

+10603
-4715
lines changed

Some content is hidden

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

334 files changed

+10603
-4715
lines changed

‎.github/build.in.yml

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,11 @@ jobs:
4848
- name: cleanup
4949
shell: bash # This *just* deletes old files, so is safe to run outside landrun.
5050
run: |
51-
find . -name . -o -prune -exec rm -rf -- {} +
51+
if ! find . -mindepth 1 -exec rm -rf -- {} +; then
52+
echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
53+
sleep 5
54+
find . -mindepth 1 -exec rm -rf -- {} +
55+
fi
5256
# Delete all but the 5 most recent toolchains.
5357
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
5458
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -68,6 +72,7 @@ jobs:
6872
with:
6973
ref: master
7074
path: master-branch
75+
repository: leanprover-community/mathlib4
7176

7277
# Checkout the PR branch into a subdirectory
7378
- name: Checkout PR branch
@@ -268,7 +273,7 @@ jobs:
268273
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
269274
# ../master-branch/.lake/build/bin/cache put!
270275
# do not try to upload files just downloaded
271-
../master-branch/.lake/build/bin/cache put-unpacked
276+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
272277
env:
273278
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
274279
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -325,8 +330,8 @@ jobs:
325330
shell: bash
326331
run: |
327332
cd pr-branch
328-
../master-branch/.lake/build/bin/cache put Archive.lean
329-
../master-branch/.lake/build/bin/cache put Counterexamples.lean
333+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
334+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
330335
env:
331336
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
332337
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -413,6 +418,7 @@ jobs:
413418
COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }}
414419
LINT_OUTCOME: ${{ steps.lint.outcome }}
415420
TEST_OUTCOME: ${{ steps.test.outcome }}
421+
NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
416422
run: |
417423
master-branch/scripts/lean-pr-testing-comments.sh lean
418424
master-branch/scripts/lean-pr-testing-comments.sh batteries
@@ -425,6 +431,8 @@ jobs:
425431
steps:
426432

427433
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
434+
with:
435+
ref: "${{ PR_BRANCH_REF }}"
428436

429437
- name: Configure Lean
430438
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -504,10 +512,11 @@ jobs:
504512
if: FORK_CONDITION
505513
runs-on: ubuntu-latest
506514
steps:
507-
- uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
515+
- uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
508516
with:
509517
mode: check
510518
lint-bib-file: true
519+
ref: ${{ PR_BRANCH_REF }}
511520

512521
build_and_lint:
513522
name: CI Success

‎.github/workflows/bors.yml

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,11 @@ jobs:
5858
- name: cleanup
5959
shell: bash # This *just* deletes old files, so is safe to run outside landrun.
6060
run: |
61-
find . -name . -o -prune -exec rm -rf -- {} +
61+
if ! find . -mindepth 1 -exec rm -rf -- {} +; then
62+
echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
63+
sleep 5
64+
find . -mindepth 1 -exec rm -rf -- {} +
65+
fi
6266
# Delete all but the 5 most recent toolchains.
6367
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
6468
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -78,6 +82,7 @@ jobs:
7882
with:
7983
ref: master
8084
path: master-branch
85+
repository: leanprover-community/mathlib4
8186

8287
# Checkout the PR branch into a subdirectory
8388
- name: Checkout PR branch
@@ -278,7 +283,7 @@ jobs:
278283
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
279284
# ../master-branch/.lake/build/bin/cache put!
280285
# do not try to upload files just downloaded
281-
../master-branch/.lake/build/bin/cache put-unpacked
286+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
282287
env:
283288
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
284289
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -335,8 +340,8 @@ jobs:
335340
shell: bash
336341
run: |
337342
cd pr-branch
338-
../master-branch/.lake/build/bin/cache put Archive.lean
339-
../master-branch/.lake/build/bin/cache put Counterexamples.lean
343+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
344+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
340345
env:
341346
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
342347
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -423,6 +428,7 @@ jobs:
423428
COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }}
424429
LINT_OUTCOME: ${{ steps.lint.outcome }}
425430
TEST_OUTCOME: ${{ steps.test.outcome }}
431+
NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
426432
run: |
427433
master-branch/scripts/lean-pr-testing-comments.sh lean
428434
master-branch/scripts/lean-pr-testing-comments.sh batteries
@@ -435,6 +441,8 @@ jobs:
435441
steps:
436442

437443
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
444+
with:
445+
ref: "${{ github.sha }}"
438446

439447
- name: Configure Lean
440448
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -514,10 +522,11 @@ jobs:
514522
if: github.repository == 'leanprover-community/mathlib4'
515523
runs-on: ubuntu-latest
516524
steps:
517-
- uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
525+
- uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
518526
with:
519527
mode: check
520528
lint-bib-file: true
529+
ref: ${{ github.sha }}
521530

522531
build_and_lint:
523532
name: CI Success

‎.github/workflows/build.yml

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ permissions:
4545

4646
jobs:
4747
build:
48-
if: github.repository == 'leanprover-community/mathlib4'
48+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
4949
name: Build
5050
runs-on: pr
5151
outputs:
@@ -65,7 +65,11 @@ jobs:
6565
- name: cleanup
6666
shell: bash # This *just* deletes old files, so is safe to run outside landrun.
6767
run: |
68-
find . -name . -o -prune -exec rm -rf -- {} +
68+
if ! find . -mindepth 1 -exec rm -rf -- {} +; then
69+
echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
70+
sleep 5
71+
find . -mindepth 1 -exec rm -rf -- {} +
72+
fi
6973
# Delete all but the 5 most recent toolchains.
7074
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
7175
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -85,6 +89,7 @@ jobs:
8589
with:
8690
ref: master
8791
path: master-branch
92+
repository: leanprover-community/mathlib4
8893

8994
# Checkout the PR branch into a subdirectory
9095
- name: Checkout PR branch
@@ -285,7 +290,7 @@ jobs:
285290
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
286291
# ../master-branch/.lake/build/bin/cache put!
287292
# do not try to upload files just downloaded
288-
../master-branch/.lake/build/bin/cache put-unpacked
293+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
289294
env:
290295
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
291296
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -342,8 +347,8 @@ jobs:
342347
shell: bash
343348
run: |
344349
cd pr-branch
345-
../master-branch/.lake/build/bin/cache put Archive.lean
346-
../master-branch/.lake/build/bin/cache put Counterexamples.lean
350+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
351+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
347352
env:
348353
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
349354
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -430,18 +435,21 @@ jobs:
430435
COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }}
431436
LINT_OUTCOME: ${{ steps.lint.outcome }}
432437
TEST_OUTCOME: ${{ steps.test.outcome }}
438+
NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
433439
run: |
434440
master-branch/scripts/lean-pr-testing-comments.sh lean
435441
master-branch/scripts/lean-pr-testing-comments.sh batteries
436442
437443
post_steps:
438444
name: Post-Build Step
439-
if: github.repository == 'leanprover-community/mathlib4'
445+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
440446
needs: [build]
441447
runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
442448
steps:
443449

444450
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
451+
with:
452+
ref: "${{ github.sha }}"
445453

446454
- name: Configure Lean
447455
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -518,17 +526,18 @@ jobs:
518526
519527
style_lint:
520528
name: Lint style
521-
if: github.repository == 'leanprover-community/mathlib4'
529+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
522530
runs-on: ubuntu-latest
523531
steps:
524-
- uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
532+
- uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
525533
with:
526534
mode: check
527535
lint-bib-file: true
536+
ref: ${{ github.sha }}
528537

529538
build_and_lint:
530539
name: CI Success
531-
if: github.repository == 'leanprover-community/mathlib4'
540+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
532541
needs: [style_lint, post_steps]
533542
runs-on: ubuntu-latest
534543
steps:
@@ -538,7 +547,7 @@ jobs:
538547
539548
final:
540549
name: Post-CI job
541-
if: github.repository == 'leanprover-community/mathlib4'
550+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
542551
needs: [style_lint, build, post_steps]
543552
runs-on: ubuntu-latest
544553
steps:

‎.github/workflows/build_fork.yml

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,11 @@ jobs:
6262
- name: cleanup
6363
shell: bash # This *just* deletes old files, so is safe to run outside landrun.
6464
run: |
65-
find . -name . -o -prune -exec rm -rf -- {} +
65+
if ! find . -mindepth 1 -exec rm -rf -- {} +; then
66+
echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
67+
sleep 5
68+
find . -mindepth 1 -exec rm -rf -- {} +
69+
fi
6670
# Delete all but the 5 most recent toolchains.
6771
# Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
6872
# Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
@@ -82,6 +86,7 @@ jobs:
8286
with:
8387
ref: master
8488
path: master-branch
89+
repository: leanprover-community/mathlib4
8590

8691
# Checkout the PR branch into a subdirectory
8792
- name: Checkout PR branch
@@ -282,7 +287,7 @@ jobs:
282287
# run this in CI if it gets an incorrect lake hash for existing cache files somehow
283288
# ../master-branch/.lake/build/bin/cache put!
284289
# do not try to upload files just downloaded
285-
../master-branch/.lake/build/bin/cache put-unpacked
290+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
286291
env:
287292
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
288293
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -339,8 +344,8 @@ jobs:
339344
shell: bash
340345
run: |
341346
cd pr-branch
342-
../master-branch/.lake/build/bin/cache put Archive.lean
343-
../master-branch/.lake/build/bin/cache put Counterexamples.lean
347+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Archive.lean
348+
../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put Counterexamples.lean
344349
env:
345350
MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
346351
MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
@@ -427,6 +432,7 @@ jobs:
427432
COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }}
428433
LINT_OUTCOME: ${{ steps.lint.outcome }}
429434
TEST_OUTCOME: ${{ steps.test.outcome }}
435+
NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
430436
run: |
431437
master-branch/scripts/lean-pr-testing-comments.sh lean
432438
master-branch/scripts/lean-pr-testing-comments.sh batteries
@@ -439,6 +445,8 @@ jobs:
439445
steps:
440446

441447
- uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
448+
with:
449+
ref: "${{ github.event.pull_request.head.sha }}"
442450

443451
- name: Configure Lean
444452
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
@@ -518,10 +526,11 @@ jobs:
518526
if: github.event.pull_request.head.repo.fork
519527
runs-on: ubuntu-latest
520528
steps:
521-
- uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
529+
- uses: leanprover-community/lint-style-action@d29fb3b12c1c834450680b3c544f63fe0237a2e2 # 2025-06-20
522530
with:
523531
mode: check
524532
lint-bib-file: true
533+
ref: ${{ github.event.pull_request.head.sha }}
525534

526535
build_and_lint:
527536
name: CI Success

‎.github/workflows/daily.yml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,10 @@ name: Daily CI Workflow
33
# running some expensive CI checks that we don't want to run on every PR.
44
# It reports results via Zulip.
55

6+
# This script requires that the ZULIP_API_KEY secret is available in both
7+
# `leanprover-community/mathlib4` and `leanprover-community/mathlib4-nightly-testing`
8+
# repositories.
9+
610
on:
711
schedule:
812
- cron: '0 0 * * *' # Runs at 00:00 UTC every day
@@ -15,7 +19,7 @@ env:
1519
jobs:
1620
check-lean4checker:
1721
runs-on: ubuntu-latest
18-
if: github.repository == 'leanprover-community/mathlib4'
22+
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
1923
strategy:
2024
matrix:
2125
branch_type: [master, nightly]

‎.github/workflows/discover-lean-pr-testing.yml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,12 @@ on:
1010
jobs:
1111
discover-lean-pr-testing:
1212
runs-on: ubuntu-latest
13+
if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
1314

1415
steps:
1516
- name: Checkout mathlib4 repository
1617
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
1718
with:
18-
repository: leanprover-community/mathlib4
1919
ref: nightly-testing
2020
fetch-depth: 0 # Fetch all branches
2121

@@ -177,7 +177,7 @@ jobs:
177177
COMPARE_BASE="$LATEST_TAG"
178178
fi
179179
180-
GITHUB_DIFF="https://github.com/leanprover-community/mathlib4/compare/$COMPARE_BASE...lean-pr-testing-$PR_NUMBER"
180+
GITHUB_DIFF="https://github.com/${{ github.repository }}/compare/$COMPARE_BASE...lean-pr-testing-$PR_NUMBER"
181181
182182
echo "Attempting to merge branch: $BRANCH (PR #$PR_NUMBER)"
183183
echo "Using diff URL: $GITHUB_DIFF (comparing with $COMPARE_BASE)"
@@ -217,7 +217,7 @@ jobs:
217217
if [ -n "$SUCCESSFUL_MERGES" ]; then
218218
MESSAGE+=$'### ✅ Successfully merged branches into \'nightly-testing\':\n\n'
219219
for MERGE_INFO in $SUCCESSFUL_MERGES; do
220-
IFS='|' read -r PR_NUMBER GITHUB_DIFF BRANCH <<< "$MERGE_INFO"
220+
IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
221221
MESSAGE+=$(printf -- '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
222222
done
223223
MESSAGE+=$'\n'
@@ -229,7 +229,7 @@ jobs:
229229
if [ -n "$FAILED_MERGES" ]; then
230230
MESSAGE+=$'### ❌ Failed merges:\n\nThe following branches need to be merged manually into \'nightly-testing\':\n\n'
231231
for MERGE_INFO in $FAILED_MERGES; do
232-
IFS='|' read -r PR_NUMBER GITHUB_DIFF BRANCH <<< "$MERGE_INFO"
232+
IFS='|' read -r PR_NUMBER GITHUB_DIFF _ <<< "$MERGE_INFO"
233233
MESSAGE+=$(printf '- [lean-pr-testing-%s](%s) (adaptations for lean#%s)' "$PR_NUMBER" "$GITHUB_DIFF" "$PR_NUMBER")$'\n\n'
234234
MESSAGE+=$'```bash\n'
235235
MESSAGE+=$(printf 'scripts/merge-lean-testing-pr.sh %s' "$PR_NUMBER")$'\n'

0 commit comments

Comments
 (0)