Skip to content

Commit 2bdf289

Browse files
CoolRmalCoolRmal
authored
Merge branch 'leanprover-community:master' into main
2 parents 1e509db + 168b9cf commit 2bdf289

1,736 files changed

Lines changed: 36025 additions & 17717 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/build.in.yml‎

Lines changed: 48 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -496,15 +496,34 @@ jobs:
496496
# cd pr-branch
497497
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
498498

499+
- name: kill stray runLinter processes
500+
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
501+
continue-on-error: true
502+
shell: bash
503+
run: |
504+
echo "Checking for runLinter processes..."
505+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
506+
echo "Killing runLinter processes..."
507+
pkill -f runLinter || true
508+
else
509+
echo "No stray runLinter processes found."
510+
fi
511+
499512
- name: lint mathlib
500513
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
501514
id: lint
515+
timeout-minutes: 40
502516
run: |
503517
cd pr-branch
518+
set -o pipefail
504519
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
505520
# 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
521+
for attempt in 1 2; do
522+
if timeout 15m 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
508527
echo ""
509528
echo "=============================================================================="
510529
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -517,9 +536,24 @@ jobs:
517536
echo " git push"
518537
echo "=============================================================================="
519538
echo ""
539+
exit 1
520540
fi
521-
exit 1
522-
fi
541+
if [ "$status" -eq 124 ]; then
542+
echo "runLinter timed out (attempt $attempt)."
543+
if [ "$attempt" -lt 2 ]; then
544+
echo "Checking for runLinter processes..."
545+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
546+
echo "Killing runLinter processes..."
547+
pkill -f runLinter || true
548+
else
549+
echo "No stray runLinter processes found."
550+
fi
551+
echo "Retrying runLinter after timeout..."
552+
continue
553+
fi
554+
fi
555+
exit $status
556+
done
523557
524558
- name: end gh-problem-match-wrap for shake and lint steps
525559
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -545,6 +579,15 @@ jobs:
545579
exit 1
546580
fi
547581
582+
- name: list stray runLinter processes
583+
shell: bash
584+
if: always()
585+
run: |
586+
echo "Checking for runLinter processes..."
587+
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
588+
echo "No stray runLinter processes found."
589+
fi
590+
548591
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
549592
if: always()
550593
shell: bash
@@ -642,34 +685,7 @@ jobs:
642685
lake build AesopTest
643686
644687
# We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
645-
# Instead we run it in a cron job on master: see `lean4checker.yml`.
646-
# Output is posted to the zulip topic
647-
# https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
648-
649-
- name: checkout lean4checker
650-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
651-
shell: bash
652-
run: |
653-
git clone https://github.com/leanprover/lean4checker
654-
cd lean4checker
655-
# Read lean-toolchain file and checkout appropriate branch
656-
TOOLCHAIN=$(cat ../lean-toolchain)
657-
if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
658-
VERSION=${TOOLCHAIN#leanprover/lean4:}
659-
git checkout "$VERSION"
660-
else
661-
git checkout master
662-
fi
663-
664-
- name: run leanchecker on itself
665-
if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
666-
run: |
667-
cd lean4checker
668-
# Build lean4checker using the same toolchain
669-
cp ../lean-toolchain .
670-
lake build
671-
lake -q exe lean4checker Lean4Checker
672-
688+
# Instead we run it in a cron job on master: see `daily.yml`.
673689
style_lint:
674690
name: Lint styleJOB_NAME
675691
if: FORK_CONDITION

‎.github/workflows/bors.yml‎

Lines changed: 48 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -506,15 +506,34 @@ jobs:
506506
# cd pr-branch
507507
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
508508

509+
- name: kill stray runLinter processes
510+
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
511+
continue-on-error: true
512+
shell: bash
513+
run: |
514+
echo "Checking for runLinter processes..."
515+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
516+
echo "Killing runLinter processes..."
517+
pkill -f runLinter || true
518+
else
519+
echo "No stray runLinter processes found."
520+
fi
521+
509522
- name: lint mathlib
510523
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
511524
id: lint
525+
timeout-minutes: 40
512526
run: |
513527
cd pr-branch
528+
set -o pipefail
514529
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
515530
# 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
531+
for attempt in 1 2; do
532+
if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
533+
break
534+
fi
535+
status=${PIPESTATUS[0]}
536+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
518537
echo ""
519538
echo "=============================================================================="
520539
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -527,9 +546,24 @@ jobs:
527546
echo " git push"
528547
echo "=============================================================================="
529548
echo ""
549+
exit 1
530550
fi
531-
exit 1
532-
fi
551+
if [ "$status" -eq 124 ]; then
552+
echo "runLinter timed out (attempt $attempt)."
553+
if [ "$attempt" -lt 2 ]; then
554+
echo "Checking for runLinter processes..."
555+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
556+
echo "Killing runLinter processes..."
557+
pkill -f runLinter || true
558+
else
559+
echo "No stray runLinter processes found."
560+
fi
561+
echo "Retrying runLinter after timeout..."
562+
continue
563+
fi
564+
fi
565+
exit $status
566+
done
533567
534568
- name: end gh-problem-match-wrap for shake and lint steps
535569
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -555,6 +589,15 @@ jobs:
555589
exit 1
556590
fi
557591
592+
- name: list stray runLinter processes
593+
shell: bash
594+
if: always()
595+
run: |
596+
echo "Checking for runLinter processes..."
597+
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
598+
echo "No stray runLinter processes found."
599+
fi
600+
558601
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
559602
if: always()
560603
shell: bash
@@ -652,34 +695,7 @@ jobs:
652695
lake build AesopTest
653696
654697
# 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-
698+
# Instead we run it in a cron job on master: see `daily.yml`.
683699
style_lint:
684700
name: Lint style
685701
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

‎.github/workflows/build.yml‎

Lines changed: 48 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -512,15 +512,34 @@ jobs:
512512
# cd pr-branch
513513
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
514514

515+
- name: kill stray runLinter processes
516+
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
517+
continue-on-error: true
518+
shell: bash
519+
run: |
520+
echo "Checking for runLinter processes..."
521+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
522+
echo "Killing runLinter processes..."
523+
pkill -f runLinter || true
524+
else
525+
echo "No stray runLinter processes found."
526+
fi
527+
515528
- name: lint mathlib
516529
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
517530
id: lint
531+
timeout-minutes: 40
518532
run: |
519533
cd pr-branch
534+
set -o pipefail
520535
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
521536
# 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
537+
for attempt in 1 2; do
538+
if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
539+
break
540+
fi
541+
status=${PIPESTATUS[0]}
542+
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
524543
echo ""
525544
echo "=============================================================================="
526545
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -533,9 +552,24 @@ jobs:
533552
echo " git push"
534553
echo "=============================================================================="
535554
echo ""
555+
exit 1
536556
fi
537-
exit 1
538-
fi
557+
if [ "$status" -eq 124 ]; then
558+
echo "runLinter timed out (attempt $attempt)."
559+
if [ "$attempt" -lt 2 ]; then
560+
echo "Checking for runLinter processes..."
561+
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
562+
echo "Killing runLinter processes..."
563+
pkill -f runLinter || true
564+
else
565+
echo "No stray runLinter processes found."
566+
fi
567+
echo "Retrying runLinter after timeout..."
568+
continue
569+
fi
570+
fi
571+
exit $status
572+
done
539573
540574
- name: end gh-problem-match-wrap for shake and lint steps
541575
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -561,6 +595,15 @@ jobs:
561595
exit 1
562596
fi
563597
598+
- name: list stray runLinter processes
599+
shell: bash
600+
if: always()
601+
run: |
602+
echo "Checking for runLinter processes..."
603+
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
604+
echo "No stray runLinter processes found."
605+
fi
606+
564607
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
565608
if: always()
566609
shell: bash
@@ -658,34 +701,7 @@ jobs:
658701
lake build AesopTest
659702
660703
# 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-
704+
# Instead we run it in a cron job on master: see `daily.yml`.
689705
style_lint:
690706
name: Lint style
691707
if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'

0 commit comments

Comments
 (0)