ci: detect and kill stray runLinter processes before linting (#34011)

Part of an investigation of hanging 'lint mathlib' steps across workflows. We have noticed stray instances of these processes active in subsequent runs. Let's see if the hangs can be mitigated by killing these before starting the linting step. This would point to some synchronization issue between these stray instances - a bit of a long shot, but worth a try.

Identifying where these strays are coming from might also give some insight. System logs show that sometimes these processes are affected by the Linux OOM killer.

Author: marcelolynch

.github/build.in.yml

@@ -496,6 +496,19 @@ jobs:
       #     cd pr-branch
       #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
 
+      - name: kill stray runLinter processes
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          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
+
       - name: lint mathlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
@@ -546,6 +559,15 @@ jobs:
             exit 1
           fi
 
+      - name: list stray runLinter processes
+        shell: bash
+        if: always()
+        run: |
+          echo "Checking for runLinter processes..."
+          if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
+            echo "No stray runLinter processes found."
+          fi
+
       - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         shell: bash

.github/workflows/bors.yml

@@ -506,6 +506,19 @@ jobs:
       #     cd pr-branch
       #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
 
+      - name: kill stray runLinter processes
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          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
+
       - name: lint mathlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
@@ -556,6 +569,15 @@ jobs:
             exit 1
           fi
 
+      - name: list stray runLinter processes
+        shell: bash
+        if: always()
+        run: |
+          echo "Checking for runLinter processes..."
+          if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
+            echo "No stray runLinter processes found."
+          fi
+
       - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         shell: bash

.github/workflows/build.yml

@@ -512,6 +512,19 @@ jobs:
       #     cd pr-branch
       #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
 
+      - name: kill stray runLinter processes
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          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
+
       - name: lint mathlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
@@ -562,6 +575,15 @@ jobs:
             exit 1
           fi
 
+      - name: list stray runLinter processes
+        shell: bash
+        if: always()
+        run: |
+          echo "Checking for runLinter processes..."
+          if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
+            echo "No stray runLinter processes found."
+          fi
+
       - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         shell: bash

.github/workflows/build_fork.yml

@@ -510,6 +510,19 @@ jobs:
       #     cd pr-branch
       #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
 
+      - name: kill stray runLinter processes
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          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
+
       - name: lint mathlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
@@ -560,6 +573,15 @@ jobs:
             exit 1
           fi
 
+      - name: list stray runLinter processes
+        shell: bash
+        if: always()
+        run: |
+          echo "Checking for runLinter processes..."
+          if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
+            echo "No stray runLinter processes found."
+          fi
+
       - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         shell: bash