Skip to content

Commit 91ec9f6

Browse files
staroperatorstaroperator
committed
Merge branch 'master' into fun_prop_forall
2 parents a8b43f9 + 19e41d0 commit 91ec9f6

3,795 files changed

Lines changed: 36845 additions & 19237 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/actionlint.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,4 @@ self-hosted-runner:
33
- bors
44
- pr
55
- doc-gen
6+
- lean4checker

‎.github/build.in.yml‎

Lines changed: 28 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ jobs:
7878

7979
# Checkout the master branch into a subdirectory
8080
- name: Checkout master branch
81-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
81+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
8282
with:
8383
# Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
8484
# we don't maintain a `master` branch at all.
@@ -88,7 +88,7 @@ jobs:
8888

8989
# Checkout the PR branch into a subdirectory
9090
- name: Checkout PR branch
91-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
91+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
9292
with:
9393
ref: "${{ PR_BRANCH_REF }}"
9494
path: pr-branch
@@ -365,7 +365,7 @@ jobs:
365365
366366
- name: upload artifact containing contents of pr-branch
367367
# temporary measure for debugging no-build failures
368-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
368+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
369369
with:
370370
name: mathlib4_artifact
371371
include-hidden-files: true
@@ -395,7 +395,7 @@ jobs:
395395
# do not try to upload files just downloaded
396396
397397
echo "Uploading cache to Azure..."
398-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
398+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
399399
env:
400400
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
401401

@@ -451,8 +451,8 @@ jobs:
451451
export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
452452
453453
echo "Uploading Archive and Counterexamples cache to Azure..."
454-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
455-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
454+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
455+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
456456
env:
457457
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
458458

@@ -501,7 +501,25 @@ jobs:
501501
id: lint
502502
run: |
503503
cd pr-branch
504-
env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib
504+
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
505+
# We use .lake/ for the output file because landrun restricts /tmp access
506+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
507+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
508+
echo ""
509+
echo "=============================================================================="
510+
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
511+
echo "the --trace flag. Please merge 'master' into your PR branch to get the"
512+
echo "updated linter, then push again."
513+
echo ""
514+
echo "You can do this with:"
515+
echo " git fetch upstream"
516+
echo " git merge upstream/master"
517+
echo " git push"
518+
echo "=============================================================================="
519+
echo ""
520+
fi
521+
exit 1
522+
fi
505523
506524
- name: end gh-problem-match-wrap for shake and lint steps
507525
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -552,7 +570,7 @@ jobs:
552570
runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
553571
steps:
554572

555-
- uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
573+
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
556574
with:
557575
ref: "${{ PR_BRANCH_REF }}"
558576

@@ -600,7 +618,7 @@ jobs:
600618
lake exe graph
601619
602620
- name: upload the import graph
603-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
621+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
604622
with:
605623
name: import-graph
606624
path: import_graph.dot
@@ -704,7 +722,7 @@ jobs:
704722
# unfortunately we cannot query only for 'auto-merge-after-CI' events
705723
# so we have to process this with jq in the next step
706724
id: get-timeline
707-
uses: octokit/graphql-action@abaeca7ba4f0325d63b8de7ef943c2418d161b93 # v3.0.0
725+
uses: octokit/graphql-action@ddde8ebb2493e79f390e6449c725c21663a67505 # v3.0.2
708726
with:
709727
query: |
710728
query($owner: String!, $name: String!, $number: Int!) {

‎.github/workflows/PR_summary.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,15 +17,15 @@ jobs:
1717

1818
steps:
1919
- name: Checkout code
20-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
20+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
2121
with:
2222
ref: ${{ github.event.pull_request.head.sha }}
2323
fetch-depth: 0
2424
path: pr-branch
2525

2626
# Checkout the master branch into a subdirectory
2727
- name: Checkout master branch
28-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
28+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
2929
with:
3030
# When testing the scripts, comment out the "ref: master"
3131
ref: master

‎.github/workflows/actionlint.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ jobs:
1010
runs-on: ubuntu-latest
1111
steps:
1212
- name: Checkout
13-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
13+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
1414

1515
- name: suggester / actionlint
1616
uses: reviewdog/action-actionlint@83e4ed25b168066ad8f62f5afbb29ebd8641d982 # v1.69.1
@@ -22,7 +22,7 @@ jobs:
2222
name: check workflows generated by build.in.yml
2323
runs-on: ubuntu-latest
2424
steps:
25-
- uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
25+
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
2626

2727
- name: update workflows
2828
run: |

‎.github/workflows/add_label_from_diff.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ jobs:
2222
if: github.repository == 'leanprover-community/mathlib4'
2323
steps:
2424
- name: Checkout code
25-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
25+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
2626
with:
2727
ref: ${{ github.event.pull_request.head.sha }}
2828
fetch-depth: 0

‎.github/workflows/auto_assign_reviewers.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ jobs:
1111
name: assign automatically proposed reviewers
1212
runs-on: ubuntu-latest
1313
steps:
14-
- uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
14+
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
1515
with:
1616
ref: master
1717
sparse-checkout: |

‎.github/workflows/bors.yml‎

Lines changed: 28 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ jobs:
8888

8989
# Checkout the master branch into a subdirectory
9090
- name: Checkout master branch
91-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
91+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
9292
with:
9393
# Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
9494
# we don't maintain a `master` branch at all.
@@ -98,7 +98,7 @@ jobs:
9898

9999
# Checkout the PR branch into a subdirectory
100100
- name: Checkout PR branch
101-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
101+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
102102
with:
103103
ref: "${{ github.sha }}"
104104
path: pr-branch
@@ -375,7 +375,7 @@ jobs:
375375
376376
- name: upload artifact containing contents of pr-branch
377377
# temporary measure for debugging no-build failures
378-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
378+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
379379
with:
380380
name: mathlib4_artifact
381381
include-hidden-files: true
@@ -405,7 +405,7 @@ jobs:
405405
# do not try to upload files just downloaded
406406
407407
echo "Uploading cache to Azure..."
408-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
408+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
409409
env:
410410
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
411411

@@ -461,8 +461,8 @@ jobs:
461461
export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
462462
463463
echo "Uploading Archive and Counterexamples cache to Azure..."
464-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
465-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
464+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
465+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
466466
env:
467467
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
468468

@@ -511,7 +511,25 @@ jobs:
511511
id: lint
512512
run: |
513513
cd pr-branch
514-
env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib
514+
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
515+
# We use .lake/ for the output file because landrun restricts /tmp access
516+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
517+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
518+
echo ""
519+
echo "=============================================================================="
520+
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
521+
echo "the --trace flag. Please merge 'master' into your PR branch to get the"
522+
echo "updated linter, then push again."
523+
echo ""
524+
echo "You can do this with:"
525+
echo " git fetch upstream"
526+
echo " git merge upstream/master"
527+
echo " git push"
528+
echo "=============================================================================="
529+
echo ""
530+
fi
531+
exit 1
532+
fi
515533
516534
- name: end gh-problem-match-wrap for shake and lint steps
517535
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -562,7 +580,7 @@ jobs:
562580
runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
563581
steps:
564582

565-
- uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
583+
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
566584
with:
567585
ref: "${{ github.sha }}"
568586

@@ -610,7 +628,7 @@ jobs:
610628
lake exe graph
611629
612630
- name: upload the import graph
613-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
631+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
614632
with:
615633
name: import-graph
616634
path: import_graph.dot
@@ -714,7 +732,7 @@ jobs:
714732
# unfortunately we cannot query only for 'auto-merge-after-CI' events
715733
# so we have to process this with jq in the next step
716734
id: get-timeline
717-
uses: octokit/graphql-action@abaeca7ba4f0325d63b8de7ef943c2418d161b93 # v3.0.0
735+
uses: octokit/graphql-action@ddde8ebb2493e79f390e6449c725c21663a67505 # v3.0.2
718736
with:
719737
query: |
720738
query($owner: String!, $name: String!, $number: Int!) {

‎.github/workflows/build.yml‎

Lines changed: 28 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ jobs:
9494

9595
# Checkout the master branch into a subdirectory
9696
- name: Checkout master branch
97-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
97+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
9898
with:
9999
# Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
100100
# we don't maintain a `master` branch at all.
@@ -104,7 +104,7 @@ jobs:
104104

105105
# Checkout the PR branch into a subdirectory
106106
- name: Checkout PR branch
107-
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
107+
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
108108
with:
109109
ref: "${{ github.sha }}"
110110
path: pr-branch
@@ -381,7 +381,7 @@ jobs:
381381
382382
- name: upload artifact containing contents of pr-branch
383383
# temporary measure for debugging no-build failures
384-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
384+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
385385
with:
386386
name: mathlib4_artifact
387387
include-hidden-files: true
@@ -411,7 +411,7 @@ jobs:
411411
# do not try to upload files just downloaded
412412
413413
echo "Uploading cache to Azure..."
414-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
414+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
415415
env:
416416
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
417417

@@ -467,8 +467,8 @@ jobs:
467467
export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
468468
469469
echo "Uploading Archive and Counterexamples cache to Azure..."
470-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
471-
USE_FRO_CACHE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
470+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
471+
MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
472472
env:
473473
MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
474474

@@ -517,7 +517,25 @@ jobs:
517517
id: lint
518518
run: |
519519
cd pr-branch
520-
env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib
520+
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
521+
# We use .lake/ for the output file because landrun restricts /tmp access
522+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
523+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
524+
echo ""
525+
echo "=============================================================================="
526+
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
527+
echo "the --trace flag. Please merge 'master' into your PR branch to get the"
528+
echo "updated linter, then push again."
529+
echo ""
530+
echo "You can do this with:"
531+
echo " git fetch upstream"
532+
echo " git merge upstream/master"
533+
echo " git push"
534+
echo "=============================================================================="
535+
echo ""
536+
fi
537+
exit 1
538+
fi
521539
522540
- name: end gh-problem-match-wrap for shake and lint steps
523541
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -568,7 +586,7 @@ jobs:
568586
runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
569587
steps:
570588

571-
- uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
589+
- uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
572590
with:
573591
ref: "${{ github.sha }}"
574592

@@ -616,7 +634,7 @@ jobs:
616634
lake exe graph
617635
618636
- name: upload the import graph
619-
uses: actions/upload-artifact@330a01c490aca151604b8cf639adc76d48f6c5d4 # v5.0.0
637+
uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
620638
with:
621639
name: import-graph
622640
path: import_graph.dot
@@ -720,7 +738,7 @@ jobs:
720738
# unfortunately we cannot query only for 'auto-merge-after-CI' events
721739
# so we have to process this with jq in the next step
722740
id: get-timeline
723-
uses: octokit/graphql-action@abaeca7ba4f0325d63b8de7ef943c2418d161b93 # v3.0.0
741+
uses: octokit/graphql-action@ddde8ebb2493e79f390e6449c725c21663a67505 # v3.0.2
724742
with:
725743
query: |
726744
query($owner: String!, $name: String!, $number: Int!) {

0 commit comments

Comments
 (0)