Merge branch 'master' into zfset_omega

Author: staroperator

.github/build.in.yml

@@ -495,20 +495,6 @@ jobs:
       #   run: |
       #     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
@@ -519,7 +505,7 @@ jobs:
           # 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
           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
+            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
               break
             fi
             status=${PIPESTATUS[0]}
@@ -541,20 +527,27 @@ jobs:
             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
 
+      # We need to separate this step from the previous script because it needs to run outside of landrun
+      - name: kill stray runLinter processes
+        if: ${{ steps.lint.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          echo "Checking for runLinter processes..."
+          if pgrep -af runLinter; then
+            echo "Killing runLinter processes..."
+            pkill -f runLinter || true
+          else
+            echo "No stray runLinter processes found."
+          fi
+
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -579,15 +572,6 @@ 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
@@ -676,7 +660,7 @@ jobs:
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work
         run: |
-          lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: build AesopTest (nightly-testing only)
         # Only run on the mathlib4-nightly-testing repository

.github/workflows/add_label_from_diff.yaml

@@ -40,7 +40,7 @@ jobs:
         labels="$(lake exe autolabel)"
         printf '%s\n' "${labels}"
         # extract
-        label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')"
+        label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')"
         printf 'label: "%s"\n' "${label}"
         if [ -n "${label}" ]
         then

.github/workflows/bors.yml

@@ -505,20 +505,6 @@ jobs:
       #   run: |
       #     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
@@ -529,7 +515,7 @@ jobs:
           # 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
           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
+            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
               break
             fi
             status=${PIPESTATUS[0]}
@@ -551,20 +537,27 @@ jobs:
             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
 
+      # We need to separate this step from the previous script because it needs to run outside of landrun
+      - name: kill stray runLinter processes
+        if: ${{ steps.lint.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          echo "Checking for runLinter processes..."
+          if pgrep -af runLinter; then
+            echo "Killing runLinter processes..."
+            pkill -f runLinter || true
+          else
+            echo "No stray runLinter processes found."
+          fi
+
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -589,15 +582,6 @@ 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
@@ -686,7 +670,7 @@ jobs:
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work
         run: |
-          lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: build AesopTest (nightly-testing only)
         # Only run on the mathlib4-nightly-testing repository

.github/workflows/build.yml

@@ -511,20 +511,6 @@ jobs:
       #   run: |
       #     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
@@ -535,7 +521,7 @@ jobs:
           # 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
           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
+            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
               break
             fi
             status=${PIPESTATUS[0]}
@@ -557,20 +543,27 @@ jobs:
             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
 
+      # We need to separate this step from the previous script because it needs to run outside of landrun
+      - name: kill stray runLinter processes
+        if: ${{ steps.lint.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          echo "Checking for runLinter processes..."
+          if pgrep -af runLinter; then
+            echo "Killing runLinter processes..."
+            pkill -f runLinter || true
+          else
+            echo "No stray runLinter processes found."
+          fi
+
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -595,15 +588,6 @@ 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
@@ -692,7 +676,7 @@ jobs:
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work
         run: |
-          lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: build AesopTest (nightly-testing only)
         # Only run on the mathlib4-nightly-testing repository

.github/workflows/build_fork.yml

@@ -509,20 +509,6 @@ jobs:
       #   run: |
       #     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
@@ -533,7 +519,7 @@ jobs:
           # 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
           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
+            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
               break
             fi
             status=${PIPESTATUS[0]}
@@ -555,20 +541,27 @@ jobs:
             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
 
+      # We need to separate this step from the previous script because it needs to run outside of landrun
+      - name: kill stray runLinter processes
+        if: ${{ steps.lint.outcome == 'failure' }}
+        continue-on-error: true
+        shell: bash
+        run: |
+          echo "Checking for runLinter processes..."
+          if pgrep -af runLinter; then
+            echo "Killing runLinter processes..."
+            pkill -f runLinter || true
+          else
+            echo "No stray runLinter processes found."
+          fi
+
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -593,15 +586,6 @@ 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
@@ -690,7 +674,7 @@ jobs:
         # make sure everything is available for test/import_all.lean
         # and that miscellaneous executables still work
         run: |
-          lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
+          lake build Batteries Qq Aesop ProofWidgets Plausible
 
       - name: build AesopTest (nightly-testing only)
         # Only run on the mathlib4-nightly-testing repository

.github/workflows/daily.yml

@@ -22,12 +22,12 @@ permissions:
 
 jobs:
   check-leanchecker:
-    runs-on: lean4checker
+    runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     strategy:
       fail-fast: false
       matrix:
-        branch_type: [nightly] #[master, nightly]  # TODO: reactivate master when leanchecker has landed there (also below)
+        branch_type: [master, nightly]
     steps:
       # Checkout repository, so that we can fetch tags to decide which branch we want.
       - name: Checkout branch or tag
@@ -79,7 +79,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        branch_type: [nightly]  # [master, nightly]
+        branch_type: [master, nightly]
     steps:
       - name: Checkout repository
         uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1