Skip to content

Commit 2975ae5

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#11994 
2 parents ab90fb0 + e0bf30b commit 2975ae5

File tree

1,852 files changed

+39996
-19239
lines changed

Some content is hidden

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

1,852 files changed

+39996
-19239
lines changed

‎.github/build.in.yml‎

Lines changed: 31 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -495,16 +495,21 @@ jobs:
495495
# run: |
496496
# cd pr-branch
497497
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
498-
499498
- name: lint mathlib
500499
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
501500
id: lint
501+
timeout-minutes: 40
502502
run: |
503503
cd pr-branch
504+
set -o pipefail
504505
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
505506
# 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
507+
for attempt in 1 2; do
508+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
509+
break
510+
fi
511+
status=${PIPESTATUS[0]}
512+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
508513
echo ""
509514
echo "=============================================================================="
510515
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -517,8 +522,30 @@ jobs:
517522
echo " git push"
518523
echo "=============================================================================="
519524
echo ""
525+
exit 1
520526
fi
521-
exit 1
527+
if [ "$status" -eq 124 ]; then
528+
echo "runLinter timed out (attempt $attempt)."
529+
if [ "$attempt" -lt 2 ]; then
530+
echo "Retrying runLinter after timeout..."
531+
continue
532+
fi
533+
fi
534+
exit $status
535+
done
536+
537+
# We need to separate this step from the previous script because it needs to run outside of landrun
538+
- name: kill stray runLinter processes
539+
if: ${{ steps.lint.outcome == 'failure' }}
540+
continue-on-error: true
541+
shell: bash
542+
run: |
543+
echo "Checking for runLinter processes..."
544+
if pgrep -af runLinter; then
545+
echo "Killing runLinter processes..."
546+
pkill -f runLinter || true
547+
else
548+
echo "No stray runLinter processes found."
522549
fi
523550
524551
- name: end gh-problem-match-wrap for shake and lint steps

‎.github/workflows/bors.yml‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -505,16 +505,21 @@ jobs:
505505
# run: |
506506
# cd pr-branch
507507
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
508-
509508
- name: lint mathlib
510509
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
511510
id: lint
511+
timeout-minutes: 40
512512
run: |
513513
cd pr-branch
514+
set -o pipefail
514515
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
515516
# 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
517+
for attempt in 1 2; do
518+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
519+
break
520+
fi
521+
status=${PIPESTATUS[0]}
522+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
518523
echo ""
519524
echo "=============================================================================="
520525
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -527,8 +532,30 @@ jobs:
527532
echo " git push"
528533
echo "=============================================================================="
529534
echo ""
535+
exit 1
530536
fi
531-
exit 1
537+
if [ "$status" -eq 124 ]; then
538+
echo "runLinter timed out (attempt $attempt)."
539+
if [ "$attempt" -lt 2 ]; then
540+
echo "Retrying runLinter after timeout..."
541+
continue
542+
fi
543+
fi
544+
exit $status
545+
done
546+
547+
# We need to separate this step from the previous script because it needs to run outside of landrun
548+
- name: kill stray runLinter processes
549+
if: ${{ steps.lint.outcome == 'failure' }}
550+
continue-on-error: true
551+
shell: bash
552+
run: |
553+
echo "Checking for runLinter processes..."
554+
if pgrep -af runLinter; then
555+
echo "Killing runLinter processes..."
556+
pkill -f runLinter || true
557+
else
558+
echo "No stray runLinter processes found."
532559
fi
533560
534561
- name: end gh-problem-match-wrap for shake and lint steps
@@ -652,34 +679,7 @@ jobs:
652679
lake build AesopTest
653680
654681
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
655-
# Instead we run it in a cron job on master: see `lean4checker.yml`.
656-
# Output is posted to the zulip topic
657-
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
658-
659-
- name: checkout lean4checker
660-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
661-
shell: bash
662-
run: |
663-
git clone https://github.com/leanprover/lean4checker
664-
cd lean4checker
665-
# Read lean-toolchain file and checkout appropriate branch
666-
TOOLCHAIN=$(cat ../lean-toolchain)
667-
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
668-
VERSION=${TOOLCHAIN#leanprover/lean4:}
669-
git checkout "$VERSION"
670-
else
671-
git checkout master
672-
fi
673-
674-
- name: run leanchecker on itself
675-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
676-
run: |
677-
cd lean4checker
678-
# Build lean4checker using the same toolchain
679-
cp ../lean-toolchain .
680-
lake build
681-
lake -q exe lean4checker Lean4Checker
682-
682+
# Instead we run it in a cron job on master: see `daily.yml`.
683683
style_lint:
684684
name: Lint style
685685
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

‎.github/workflows/build.yml‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -511,16 +511,21 @@ jobs:
511511
# run: |
512512
# cd pr-branch
513513
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
514-
515514
- name: lint mathlib
516515
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
517516
id: lint
517+
timeout-minutes: 40
518518
run: |
519519
cd pr-branch
520+
set -o pipefail
520521
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
521522
# 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
523+
for attempt in 1 2; do
524+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
525+
break
526+
fi
527+
status=${PIPESTATUS[0]}
528+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
524529
echo ""
525530
echo "=============================================================================="
526531
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -533,8 +538,30 @@ jobs:
533538
echo " git push"
534539
echo "=============================================================================="
535540
echo ""
541+
exit 1
536542
fi
537-
exit 1
543+
if [ "$status" -eq 124 ]; then
544+
echo "runLinter timed out (attempt $attempt)."
545+
if [ "$attempt" -lt 2 ]; then
546+
echo "Retrying runLinter after timeout..."
547+
continue
548+
fi
549+
fi
550+
exit $status
551+
done
552+
553+
# We need to separate this step from the previous script because it needs to run outside of landrun
554+
- name: kill stray runLinter processes
555+
if: ${{ steps.lint.outcome == 'failure' }}
556+
continue-on-error: true
557+
shell: bash
558+
run: |
559+
echo "Checking for runLinter processes..."
560+
if pgrep -af runLinter; then
561+
echo "Killing runLinter processes..."
562+
pkill -f runLinter || true
563+
else
564+
echo "No stray runLinter processes found."
538565
fi
539566
540567
- name: end gh-problem-match-wrap for shake and lint steps
@@ -658,34 +685,7 @@ jobs:
658685
lake build AesopTest
659686
660687
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
661-
# Instead we run it in a cron job on master: see `lean4checker.yml`.
662-
# Output is posted to the zulip topic
663-
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
664-
665-
- name: checkout lean4checker
666-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
667-
shell: bash
668-
run: |
669-
git clone https://github.com/leanprover/lean4checker
670-
cd lean4checker
671-
# Read lean-toolchain file and checkout appropriate branch
672-
TOOLCHAIN=$(cat ../lean-toolchain)
673-
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
674-
VERSION=${TOOLCHAIN#leanprover/lean4:}
675-
git checkout "$VERSION"
676-
else
677-
git checkout master
678-
fi
679-
680-
- name: run leanchecker on itself
681-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
682-
run: |
683-
cd lean4checker
684-
# Build lean4checker using the same toolchain
685-
cp ../lean-toolchain .
686-
lake build
687-
lake -q exe lean4checker Lean4Checker
688-
688+
# Instead we run it in a cron job on master: see `daily.yml`.
689689
style_lint:
690690
name: Lint style
691691
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

‎.github/workflows/build_fork.yml‎

Lines changed: 32 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -509,16 +509,21 @@ jobs:
509509
# run: |
510510
# cd pr-branch
511511
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
512-
513512
- name: lint mathlib
514513
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
515514
id: lint
515+
timeout-minutes: 40
516516
run: |
517517
cd pr-branch
518+
set -o pipefail
518519
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
519520
# We use .lake/ for the output file because landrun restricts /tmp access
520-
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
521-
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
521+
for attempt in 1 2; do
522+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
523+
break
524+
fi
525+
status=${PIPESTATUS[0]}
526+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
522527
echo ""
523528
echo "=============================================================================="
524529
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -531,8 +536,30 @@ jobs:
531536
echo " git push"
532537
echo "=============================================================================="
533538
echo ""
539+
exit 1
534540
fi
535-
exit 1
541+
if [ "$status" -eq 124 ]; then
542+
echo "runLinter timed out (attempt $attempt)."
543+
if [ "$attempt" -lt 2 ]; then
544+
echo "Retrying runLinter after timeout..."
545+
continue
546+
fi
547+
fi
548+
exit $status
549+
done
550+
551+
# We need to separate this step from the previous script because it needs to run outside of landrun
552+
- name: kill stray runLinter processes
553+
if: ${{ steps.lint.outcome == 'failure' }}
554+
continue-on-error: true
555+
shell: bash
556+
run: |
557+
echo "Checking for runLinter processes..."
558+
if pgrep -af runLinter; then
559+
echo "Killing runLinter processes..."
560+
pkill -f runLinter || true
561+
else
562+
echo "No stray runLinter processes found."
536563
fi
537564
538565
- name: end gh-problem-match-wrap for shake and lint steps
@@ -656,34 +683,7 @@ jobs:
656683
lake build AesopTest
657684
658685
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
659-
# Instead we run it in a cron job on master: see `lean4checker.yml`.
660-
# Output is posted to the zulip topic
661-
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
662-
663-
- name: checkout lean4checker
664-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
665-
shell: bash
666-
run: |
667-
git clone https://github.com/leanprover/lean4checker
668-
cd lean4checker
669-
# Read lean-toolchain file and checkout appropriate branch
670-
TOOLCHAIN=$(cat ../lean-toolchain)
671-
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
672-
VERSION=${TOOLCHAIN#leanprover/lean4:}
673-
git checkout "$VERSION"
674-
else
675-
git checkout master
676-
fi
677-
678-
- name: run leanchecker on itself
679-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
680-
run: |
681-
cd lean4checker
682-
# Build lean4checker using the same toolchain
683-
cp ../lean-toolchain .
684-
lake build
685-
lake -q exe lean4checker Lean4Checker
686-
686+
# Instead we run it in a cron job on master: see `daily.yml`.
687687
style_lint:
688688
name: Lint style (fork)
689689
if: github.event.pull_request.head.repo.fork && github.repository != 'leanprover-community/mathlib4-nightly-testing'

0 commit comments

Comments
 (0)