Skip to content

Commit d58ace0

Browse files
marcelolynchmarcelolynch
committed
Revert "ci: Retry logic for linting step (leanprover-community#34059)"
This reverts commit 9b524ac.
1 parent a0ec512 commit d58ace0

File tree

4 files changed

+20
-100
lines changed

4 files changed

+20
-100
lines changed

‎.github/build.in.yml‎

Lines changed: 5 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -512,18 +512,13 @@ jobs:
512512
- name: lint mathlib
513513
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
514514
id: lint
515-
timeout-minutes: 40
515+
timeout-minutes: 30
516516
run: |
517517
cd pr-branch
518-
set -o pipefail
519518
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
520519
# We use .lake/ for the output file because landrun restricts /tmp access
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=$?
526-
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
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
527522
echo ""
528523
echo "=============================================================================="
529524
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -536,24 +531,9 @@ jobs:
536531
echo " git push"
537532
echo "=============================================================================="
538533
echo ""
539-
exit 1
540-
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
554534
fi
555-
exit $status
556-
done
535+
exit 1
536+
fi
557537
558538
- name: end gh-problem-match-wrap for shake and lint steps
559539
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

‎.github/workflows/bors.yml‎

Lines changed: 5 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -522,18 +522,13 @@ jobs:
522522
- name: lint mathlib
523523
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
524524
id: lint
525-
timeout-minutes: 40
525+
timeout-minutes: 30
526526
run: |
527527
cd pr-branch
528-
set -o pipefail
529528
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
530529
# We use .lake/ for the output file because landrun restricts /tmp access
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=$?
536-
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
530+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
531+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
537532
echo ""
538533
echo "=============================================================================="
539534
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -546,24 +541,9 @@ jobs:
546541
echo " git push"
547542
echo "=============================================================================="
548543
echo ""
549-
exit 1
550-
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
564544
fi
565-
exit $status
566-
done
545+
exit 1
546+
fi
567547
568548
- name: end gh-problem-match-wrap for shake and lint steps
569549
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

‎.github/workflows/build.yml‎

Lines changed: 5 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -528,18 +528,13 @@ jobs:
528528
- name: lint mathlib
529529
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
530530
id: lint
531-
timeout-minutes: 40
531+
timeout-minutes: 30
532532
run: |
533533
cd pr-branch
534-
set -o pipefail
535534
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
536535
# We use .lake/ for the output file because landrun restricts /tmp access
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=$?
542-
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
536+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
537+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
543538
echo ""
544539
echo "=============================================================================="
545540
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -552,24 +547,9 @@ jobs:
552547
echo " git push"
553548
echo "=============================================================================="
554549
echo ""
555-
exit 1
556-
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
570550
fi
571-
exit $status
572-
done
551+
exit 1
552+
fi
573553
574554
- name: end gh-problem-match-wrap for shake and lint steps
575555
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

‎.github/workflows/build_fork.yml‎

Lines changed: 5 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -526,18 +526,13 @@ jobs:
526526
- name: lint mathlib
527527
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
528528
id: lint
529-
timeout-minutes: 40
529+
timeout-minutes: 30
530530
run: |
531531
cd pr-branch
532-
set -o pipefail
533532
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
534533
# We use .lake/ for the output file because landrun restricts /tmp access
535-
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
537-
break
538-
fi
539-
status=$?
540-
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
534+
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
535+
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
541536
echo ""
542537
echo "=============================================================================="
543538
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
@@ -550,24 +545,9 @@ jobs:
550545
echo " git push"
551546
echo "=============================================================================="
552547
echo ""
553-
exit 1
554-
fi
555-
if [ "$status" -eq 124 ]; then
556-
echo "runLinter timed out (attempt $attempt)."
557-
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
565-
echo "Retrying runLinter after timeout..."
566-
continue
567-
fi
568548
fi
569-
exit $status
570-
done
549+
exit 1
550+
fi
571551
572552
- name: end gh-problem-match-wrap for shake and lint steps
573553
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

0 commit comments

Comments
 (0)