diff --git a/.github/build.in.yml b/.github/build.in.yml
index 812edb223ab591..f3005eff6954f8 100644
--- a/.github/build.in.yml
+++ b/.github/build.in.yml
@@ -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"
@@ -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
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index ecc444cdfa9d33..8c57847e7ffcf3 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -522,13 +522,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"
@@ -541,9 +546,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
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 0af22c62c87eaa..1a5d757bf8a94b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -528,13 +528,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"
@@ -547,9 +552,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
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index cc7d6dcce0d2fc..fd73680e4f7f16 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -526,13 +526,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"
@@ -545,9 +550,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