Skip to content

Commit dd6c37f

Browse files
marcelolynchmarcelolynch
committed
ci: Tidy up CI after investigation (leanprover-community#34494)
Clean up some steps now that we're done with the runLinter hang investigation. We should keep the retry+timeout+kill for the sake of forks (but down to 10min because we know the step shouldn't take more than 5).
1 parent f156c64 commit dd6c37f

4 files changed

Lines changed: 60 additions & 124 deletions

File tree

‎.github/build.in.yml‎

Lines changed: 15 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -495,20 +495,6 @@ jobs:
495495
# run: |
496496
# cd pr-branch
497497
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
498-
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-
512498
- name: lint mathlib
513499
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
514500
id: lint
@@ -519,7 +505,7 @@ jobs:
519505
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
520506
# We use .lake/ for the output file because landrun restricts /tmp access
521507
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
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
523509
break
524510
fi
525511
status=${PIPESTATUS[0]}
@@ -541,20 +527,27 @@ jobs:
541527
if [ "$status" -eq 124 ]; then
542528
echo "runLinter timed out (attempt $attempt)."
543529
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
551530
echo "Retrying runLinter after timeout..."
552531
continue
553532
fi
554533
fi
555534
exit $status
556535
done
557536
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."
549+
fi
550+
558551
- name: end gh-problem-match-wrap for shake and lint steps
559552
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
560553
with:
@@ -579,15 +572,6 @@ jobs:
579572
exit 1
580573
fi
581574
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-
591575
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
592576
if: always()
593577
shell: bash

‎.github/workflows/bors.yml‎

Lines changed: 15 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -505,20 +505,6 @@ jobs:
505505
# run: |
506506
# cd pr-branch
507507
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
508-
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-
522508
- name: lint mathlib
523509
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
524510
id: lint
@@ -529,7 +515,7 @@ jobs:
529515
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
530516
# We use .lake/ for the output file because landrun restricts /tmp access
531517
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
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
533519
break
534520
fi
535521
status=${PIPESTATUS[0]}
@@ -551,20 +537,27 @@ jobs:
551537
if [ "$status" -eq 124 ]; then
552538
echo "runLinter timed out (attempt $attempt)."
553539
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
561540
echo "Retrying runLinter after timeout..."
562541
continue
563542
fi
564543
fi
565544
exit $status
566545
done
567546
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."
559+
fi
560+
568561
- name: end gh-problem-match-wrap for shake and lint steps
569562
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
570563
with:
@@ -589,15 +582,6 @@ jobs:
589582
exit 1
590583
fi
591584
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-
601585
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
602586
if: always()
603587
shell: bash

‎.github/workflows/build.yml‎

Lines changed: 15 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -511,20 +511,6 @@ jobs:
511511
# run: |
512512
# cd pr-branch
513513
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
514-
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-
528514
- name: lint mathlib
529515
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
530516
id: lint
@@ -535,7 +521,7 @@ jobs:
535521
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
536522
# We use .lake/ for the output file because landrun restricts /tmp access
537523
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
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
539525
break
540526
fi
541527
status=${PIPESTATUS[0]}
@@ -557,20 +543,27 @@ jobs:
557543
if [ "$status" -eq 124 ]; then
558544
echo "runLinter timed out (attempt $attempt)."
559545
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
567546
echo "Retrying runLinter after timeout..."
568547
continue
569548
fi
570549
fi
571550
exit $status
572551
done
573552
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."
565+
fi
566+
574567
- name: end gh-problem-match-wrap for shake and lint steps
575568
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
576569
with:
@@ -595,15 +588,6 @@ jobs:
595588
exit 1
596589
fi
597590
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-
607591
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
608592
if: always()
609593
shell: bash

‎.github/workflows/build_fork.yml‎

Lines changed: 15 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -509,20 +509,6 @@ jobs:
509509
# run: |
510510
# cd pr-branch
511511
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
512-
513-
- name: kill stray runLinter processes
514-
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
515-
continue-on-error: true
516-
shell: bash
517-
run: |
518-
echo "Checking for runLinter processes..."
519-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
520-
echo "Killing runLinter processes..."
521-
pkill -f runLinter || true
522-
else
523-
echo "No stray runLinter processes found."
524-
fi
525-
526512
- name: lint mathlib
527513
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
528514
id: lint
@@ -533,7 +519,7 @@ jobs:
533519
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
534520
# We use .lake/ for the output file because landrun restricts /tmp access
535521
for attempt in 1 2; do
536-
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
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
537523
break
538524
fi
539525
status=${PIPESTATUS[0]}
@@ -555,20 +541,27 @@ jobs:
555541
if [ "$status" -eq 124 ]; then
556542
echo "runLinter timed out (attempt $attempt)."
557543
if [ "$attempt" -lt 2 ]; then
558-
echo "Checking for runLinter processes..."
559-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
560-
echo "Killing runLinter processes..."
561-
pkill -f runLinter || true
562-
else
563-
echo "No stray runLinter processes found."
564-
fi
565544
echo "Retrying runLinter after timeout..."
566545
continue
567546
fi
568547
fi
569548
exit $status
570549
done
571550
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."
563+
fi
564+
572565
- name: end gh-problem-match-wrap for shake and lint steps
573566
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
574567
with:
@@ -593,15 +586,6 @@ jobs:
593586
exit 1
594587
fi
595588
596-
- name: list stray runLinter processes
597-
shell: bash
598-
if: always()
599-
run: |
600-
echo "Checking for runLinter processes..."
601-
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
602-
echo "No stray runLinter processes found."
603-
fi
604-
605589
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
606590
if: always()
607591
shell: bash

0 commit comments

Comments
 (0)