Skip to content

[Merged by Bors] - ci: Retry logic for linting step #34059

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
marcelolynch wants to merge 3 commits into from
+100 −20
Closed

[Merged by Bors] - ci: Retry logic for linting step #34059

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
364ab1a
Retry logic for linting step
marcelolynch Jan 16, 2026
b948aab
bump
marcelolynch Jan 16, 2026
0505bca
oops - the bang inverts the return code
marcelolynch Jan 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 25 additions & 5 deletions .github/build.in.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -512,13 +512,18 @@ jobs:
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
timeout-minutes: 30
timeout-minutes: 40
run: |
cd pr-branch
set -o pipefail
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
# We use .lake/ for the output file because landrun restricts /tmp access
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
for attempt in 1 2; do
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
break
fi
status=$?
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
echo ""
echo "=============================================================================="
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
Expand All @@ -531,9 +536,24 @@ jobs:
echo " git push"
echo "=============================================================================="
echo ""
exit 1
fi
exit 1
fi
if [ "$status" -eq 124 ]; then
echo "runLinter timed out (attempt $attempt)."
if [ "$attempt" -lt 2 ]; then
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
pkill -f runLinter || true
else
echo "No stray runLinter processes found."
fi
echo "Retrying runLinter after timeout..."
continue
fi
fi
exit $status
done

- name: end gh-problem-match-wrap for shake and lint steps
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
Expand Down
30 changes: 25 additions & 5 deletions .github/workflows/bors.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -510,7 +510,7 @@
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
continue-on-error: true
shell: bash
run: |

Check warning on line 513 in .github/workflows/bors.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/bors.yml:513:9: shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
Expand All @@ -522,13 +522,18 @@
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
timeout-minutes: 30
timeout-minutes: 40
run: |
cd pr-branch
set -o pipefail
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
# We use .lake/ for the output file because landrun restricts /tmp access
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
for attempt in 1 2; do
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
break
fi
status=$?
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
echo ""
echo "=============================================================================="
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
Expand All @@ -541,9 +546,24 @@
echo " git push"
echo "=============================================================================="
echo ""
exit 1
fi
exit 1
fi
if [ "$status" -eq 124 ]; then
echo "runLinter timed out (attempt $attempt)."
if [ "$attempt" -lt 2 ]; then
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
pkill -f runLinter || true
else
echo "No stray runLinter processes found."
fi
echo "Retrying runLinter after timeout..."
continue
fi
fi
exit $status
done

- name: end gh-problem-match-wrap for shake and lint steps
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
Expand Down Expand Up @@ -572,7 +592,7 @@
- name: list stray runLinter processes
shell: bash
if: always()
run: |

Check warning on line 595 in .github/workflows/bors.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/bors.yml:595:9: shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "No stray runLinter processes found."
Expand Down
30 changes: 25 additions & 5 deletions .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -516,7 +516,7 @@
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
continue-on-error: true
shell: bash
run: |

Check warning on line 519 in .github/workflows/build.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/build.yml:519:9: shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
Expand All @@ -528,13 +528,18 @@
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
timeout-minutes: 30
timeout-minutes: 40
run: |
cd pr-branch
set -o pipefail
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
# We use .lake/ for the output file because landrun restricts /tmp access
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
for attempt in 1 2; do
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
break
fi
status=$?
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
echo ""
echo "=============================================================================="
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
Expand All @@ -547,9 +552,24 @@
echo " git push"
echo "=============================================================================="
echo ""
exit 1
fi
exit 1
fi
if [ "$status" -eq 124 ]; then
echo "runLinter timed out (attempt $attempt)."
if [ "$attempt" -lt 2 ]; then
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
pkill -f runLinter || true
else
echo "No stray runLinter processes found."
fi
echo "Retrying runLinter after timeout..."
continue
fi
fi
exit $status
done

- name: end gh-problem-match-wrap for shake and lint steps
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
Expand Down Expand Up @@ -578,7 +598,7 @@
- name: list stray runLinter processes
shell: bash
if: always()
run: |

Check warning on line 601 in .github/workflows/build.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/build.yml:601:9: shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "No stray runLinter processes found."
Expand Down
30 changes: 25 additions & 5 deletions .github/workflows/build_fork.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -514,7 +514,7 @@
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
continue-on-error: true
shell: bash
run: |

Check warning on line 517 in .github/workflows/build_fork.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/build_fork.yml:517:9: shellcheck reported issue in this script: SC2009:info:2:4: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
Expand All @@ -526,13 +526,18 @@
- name: lint mathlib
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
id: lint
timeout-minutes: 30
timeout-minutes: 40
run: |
cd pr-branch
set -o pipefail
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
# We use .lake/ for the output file because landrun restricts /tmp access
if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
if grep -q "cannot parse arguments" .lake/lint_output.txt; then
for attempt in 1 2; do
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
break
fi
status=$?
if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
echo ""
echo "=============================================================================="
echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
Expand All @@ -545,9 +550,24 @@
echo " git push"
echo "=============================================================================="
echo ""
exit 1
fi
exit 1
fi
if [ "$status" -eq 124 ]; then
echo "runLinter timed out (attempt $attempt)."
if [ "$attempt" -lt 2 ]; then
echo "Checking for runLinter processes..."
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "Killing runLinter processes..."
pkill -f runLinter || true
else
echo "No stray runLinter processes found."
fi
echo "Retrying runLinter after timeout..."
continue
fi
fi
exit $status
done

- name: end gh-problem-match-wrap for shake and lint steps
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
Expand Down Expand Up @@ -576,7 +596,7 @@
- name: list stray runLinter processes
shell: bash
if: always()
run: |

Check warning on line 599 in .github/workflows/build_fork.yml

View workflow job for this annotation

GitHub Actions / actionlint 

[actionlint] reported by reviewdog 🐶
shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]

Raw Output:
i:.github/workflows/build_fork.yml:599:9: shellcheck reported issue in this script: SC2009:info:2:6: Consider using pgrep instead of grepping ps output [shellcheck]
echo "Checking for runLinter processes..."
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
echo "No stray runLinter processes found."
Expand Down