Merge upstream/master, resolve README conflict

Author: kim-em

.devcontainer/Dockerfile

@@ -1,8 +1,6 @@
-FROM mcr.microsoft.com/devcontainers/base:jammy
+FROM mcr.microsoft.com/devcontainers/base:ubuntu
 
 USER vscode
 WORKDIR /home/vscode
 
 RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-
-ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -1,17 +1,20 @@
 {
   "name": "Mathlib4 dev container",
 
-  "image": "ghcr.io/leanprover-community/mathlib4/gitpod",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
 
   "onCreateCommand": "lake exe cache get!",
 
   "hostRequirements": {
-     "cpus": 4
+    "cpus": 4,
+    "memory": "8gb"
   },
 
   "customizations": {
-    "vscode" : {
-      "extensions" : [ "leanprover.lean4" ]
+    "vscode": {
+      "extensions": ["leanprover.lean4"]
     }
   }
 }

.github/build.in.yml

@@ -78,7 +78,7 @@ jobs:
 
       # Checkout the master branch into a subdirectory
       - name: Checkout master branch
-        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
@@ -88,7 +88,7 @@ jobs:
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
-        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           ref: "${{ PR_BRANCH_REF }}"
           path: pr-branch
@@ -495,13 +495,58 @@ jobs:
       #   run: |
       #     cd pr-branch
       #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
-
       - name: lint mathlib
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
+        timeout-minutes: 40
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib
+          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
+          for attempt in 1 2; do
+            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]}
+            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"
+              echo "the --trace flag. Please merge 'master' into your PR branch to get the"
+              echo "updated linter, then push again."
+              echo ""
+              echo "You can do this with:"
+              echo "  git fetch upstream"
+              echo "  git merge upstream/master"
+              echo "  git push"
+              echo "=============================================================================="
+              echo ""
+              exit 1
+            fi
+            if [ "$status" -eq 124 ]; then
+              echo "runLinter timed out (attempt $attempt)."
+              if [ "$attempt" -lt 2 ]; then
+                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
@@ -552,12 +597,12 @@ jobs:
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
-      - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           ref: "${{ PR_BRANCH_REF }}"
 
       - name: Configure Lean
-        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
+        uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
         with:
           auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
           use-github-cache: false
@@ -615,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
@@ -624,34 +669,7 @@ jobs:
           lake build AesopTest
 
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
-      # Instead we run it in a cron job on master: see `lean4checker.yml`.
-      # Output is posted to the zulip topic
-      # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
-
-      - name: checkout lean4checker
-        if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
-        shell: bash
-        run: |
-          git clone https://github.com/leanprover/lean4checker
-          cd lean4checker
-          # Read lean-toolchain file and checkout appropriate branch
-          TOOLCHAIN=$(cat ../lean-toolchain)
-          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
-            VERSION=${TOOLCHAIN#leanprover/lean4:}
-            git checkout "$VERSION"
-          else
-            git checkout master
-          fi
-
-      - name: run leanchecker on itself
-        if: ${{ (always() && needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
-        run: |
-          cd lean4checker
-          # Build lean4checker using the same toolchain
-          cp ../lean-toolchain .
-          lake build
-          lake -q exe lean4checker Lean4Checker
-
+      # Instead we run it in a cron job on master: see `daily.yml`.
   style_lint:
     name: Lint styleJOB_NAME
     if: FORK_CONDITION

.github/workflows/PR_summary.yml

@@ -17,15 +17,15 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
         path: pr-branch
 
     # Checkout the master branch into a subdirectory
     - name: Checkout master branch
-      uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         # When testing the scripts, comment out the "ref: master"
         ref: master
@@ -60,7 +60,7 @@ jobs:
         fi
 
     - name: Set up Python
-      uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.0
+      uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
       with:
         python-version: 3.12
 

.github/workflows/actionlint.yml

@@ -10,10 +10,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@83e4ed25b168066ad8f62f5afbb29ebd8641d982 # v1.69.1
+        uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
         with:
           tool_name: actionlint
           fail_level: error
@@ -22,7 +22,7 @@ jobs:
     name: check workflows generated by build.in.yml
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
       - name: update workflows
         run: |

.github/workflows/add_label_from_diff.yaml

@@ -22,12 +22,12 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: Checkout code
-      uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
     - name: Configure Lean
-      uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
+      uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
       with:
         auto-config: false
         use-github-cache: false
@@ -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/auto_assign_reviewers.yaml

@@ -11,14 +11,14 @@ jobs:
     name: assign automatically proposed reviewers
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           ref: master
           sparse-checkout: |
             scripts/assign_reviewers.py
 
       - name: Set up Python
-        uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.0
+        uses: actions/setup-python@a309ff8b426b58ec0e2a45f0f869d46889d02405 # v6.2.0
         with:
           python-version: '3.x'