Merge branch 'leanprover-community:master' into lowerlimittop

Author: CoolRmal

.docker/gitpod-blueprint/Dockerfile

@@ -10,7 +10,7 @@ FROM ubuntu:jammy
 USER root
 
 ENV DEBIAN_FRONTEND=noninteractive
-RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev python3 python3-pip python3-requests -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git bash-completion texlive texlive-xetex latexmk graphviz graphviz-dev tzdata python3 python3-pip python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group

.docker/gitpod/Dockerfile

@@ -9,7 +9,7 @@ FROM ubuntu:jammy
 USER root
 
 ENV DEBIAN_FRONTEND=noninteractive
-RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-pip python3-requests -y && apt-get clean
+RUN apt-get update && apt-get install sudo git curl git tzdata bash-completion python3 python3-pip python3-requests -y && apt-get clean
 
 RUN useradd -l -u 33333 -G sudo -md /home/gitpod -s /bin/bash -p gitpod gitpod \
     # passwordless sudo for users in the 'sudo' group

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,8 +1,11 @@
 
 ---
-<!-- The text above the `---` will become the commit message when your
-PR is merged. Please leave a blank newline before the `---`, otherwise
-GitHub will format the text above it as a title.
+<!-- Your PR title will become the first line of the commit message.
+
+In this box, the text above the `---` (if not empty) will be appended
+to the commit message, and can be used to give additional context or
+details. Please leave a blank newline before the `---`, otherwise GitHub
+will format the text above it as a title.
 
 For details on the "pull request lifecycle" in mathlib, please see:
 https://leanprover-community.github.io/contribute/index.html

.github/build.in.yml

@@ -15,7 +15,7 @@ env:
 concurrency:
   # label each workflow run; only the latest with each label will run
   # workflows on master get more expressive labels
-  group: ${{ github.workflow }}-${{ github.ref }}-${{ (contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
   # cancel any running workflow with the same label
   cancel-in-progress: true
 
@@ -38,12 +38,23 @@ jobs:
       lint-outcome: ${{ steps.lint.outcome }}
       mk_all-outcome: ${{ steps.mk_all.outcome }}
       noisy-outcome: ${{ steps.noisy.outcome }}
-      shake-outcome: ${{ steps.shake.outcome }}
+      # shake-outcome: ${{ steps.shake.outcome }}
       test-outcome: ${{ steps.test.outcome }}
     defaults: # On Hoskinson runners, landrun is already installed.
-      run:
+      run: # note that .pr-branch/.lake must be created in a step below before we use this
         shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
     steps:
+      - name: job info
+        env:
+          WORKFLOW: ${{ github.workflow }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+          REF: ${{ github.ref }}
+          EVENT_NAME: ${{ github.event_name }}
+          RUN_ID: ${{ github.run_id }}
+          CONCURRENCY_GROUP: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
+        shell: bash # there is no script body, so this is safe to "run" outside landrun.
+        run: |
+          # We just populate the env vars for this step to make them viewable in the logs
       - name: cleanup
         shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
         run: |
@@ -67,7 +78,7 @@ jobs:
 
       # Checkout the master branch into a subdirectory
       - name: Checkout master branch
-        uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
         with:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
@@ -77,7 +88,7 @@ jobs:
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
-        uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
         with:
           ref: "${{ PR_BRANCH_REF }}"
           path: pr-branch
@@ -212,7 +223,7 @@ jobs:
 
           # Extract all inputRevs from the manifest
           invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
-            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?)$' || true)
+            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?(\+[a-zA-Z0-9.-]+)?)$' || true)
 
           if [ -n "$invalid_revs" ]; then
             echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
@@ -221,12 +232,57 @@ jobs:
             echo "All inputRevs must be one of:"
             echo "  - 'main'"
             echo "  - 'master'"
-            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3 or v1.2.3-pre)"
+            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3, v1.2.3-pre, or v1.2.3+build)"
             exit 1
           else
             echo "✅ All inputRevs in lake-manifest.json are valid"
           fi
 
+      - name: verify ProofWidgets lean-toolchain matches on versioned releases
+        # Only enforce this on the main mathlib4 repository, not on nightly-testing
+        if: github.repository == 'leanprover-community/mathlib4'
+        shell: bash
+        run: |
+          cd pr-branch
+
+          # Read the lean-toolchain file
+          TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
+          echo "Lean toolchain: $TOOLCHAIN"
+
+          # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
+          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
+            echo "✓ Detected versioned Lean release: $TOOLCHAIN"
+            echo "Verifying ProofWidgets lean-toolchain matches..."
+
+            # Check if ProofWidgets lean-toolchain exists
+            if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
+              echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
+              echo "This file should be created by 'lake env' during dependency download."
+              exit 1
+            fi
+
+            # Read ProofWidgets lean-toolchain
+            PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
+            echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"
+
+            # Compare the two
+            if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
+              echo "❌ Error: Lean toolchain mismatch!"
+              echo "  Main lean-toolchain: $TOOLCHAIN"
+              echo "  ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
+              echo ""
+              echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
+              echo "the ProofWidgets dependency must use the same toolchain."
+              echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
+              exit 1
+            else
+              echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
+            fi
+          else
+            echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
+            echo "Skipping ProofWidgets toolchain verification."
+          fi
+
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
         shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
@@ -295,7 +351,7 @@ jobs:
           echo "::endgroup::"
 
           ../master-branch/scripts/lake-build-with-retry.sh Mathlib
-          # results of build at pr-branch/.lake/build_summary_Mathlib*.json
+          # results of build at pr-branch/.lake/build_summary_Mathlib.json
       - name: end gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -364,15 +420,15 @@ jobs:
         run: |
           cd pr-branch
           ../master-branch/scripts/lake-build-with-retry.sh Archive
-          # results of build at pr-branch/.lake/build_summary_Archive*.json
+          # results of build at pr-branch/.lake/build_summary_Archive.json
 
       - name: build counterexamples
         id: counterexamples
         continue-on-error: true
         run: |
           cd pr-branch
           ../master-branch/scripts/lake-build-with-retry.sh Counterexamples
-          # results of build at pr-branch/.lake/build_summary_Counterexamples*.json
+          # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
       - name: Check if building Archive or Counterexamples failed
         if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
@@ -401,7 +457,7 @@ jobs:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
       - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
-        if: always()
+        if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
         run: |
           if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
             echo "Please run 'lake exe mk_all' to regenerate the import all files"
@@ -419,7 +475,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          lake --iofail test
+          ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -432,18 +488,20 @@ jobs:
           action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
           linters: gcc
 
-      - name: check for unused imports
-        id: shake
-        run: |
-          cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+      # With the arrival of the module system, the old `shake` is no longer functional.
+      # This will be replaced soon.
+      # - name: check for unused imports
+      #   id: shake
+      #   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
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+          env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib
 
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -494,7 +552,7 @@ jobs:
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
 
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      - uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
         with:
           ref: "${{ PR_BRANCH_REF }}"
 
@@ -630,15 +688,6 @@ jobs:
           echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
           echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
 
-      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
-        name: If `bench-after-CI` is present, add a `!bench` comment.
-        uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
-        with:
-          token: ${{ secrets.AUTO_MERGE_TOKEN }}
-          issue-number: ${{ steps.PR.outputs.number }}
-          body: |
-            !bench
-
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -655,7 +704,7 @@ jobs:
         # unfortunately we cannot query only for 'auto-merge-after-CI' events
         # so we have to process this with jq in the next step
         id: get-timeline
-        uses: octokit/graphql-action@8ad880e4d437783ea2ab17010324de1075228110 # v2.3.2
+        uses: octokit/graphql-action@abaeca7ba4f0325d63b8de7ef943c2418d161b93 # v3.0.0
         with:
           query: |
             query($owner: String!, $name: String!, $number: Int!) {

.github/workflows/PR_summary.yml

@@ -17,15 +17,15 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
       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@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
       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@e797f83bcb11b83ae66e0230d6156d7c80228e7c # v6.0.0
+      uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.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@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
 
       - name: suggester / actionlint
-        uses: reviewdog/action-actionlint@f00ad0691526c10be4021a91b2510f0a769b14d0 # v1.68.0
+        uses: reviewdog/action-actionlint@83e4ed25b168066ad8f62f5afbb29ebd8641d982 # v1.69.1
         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@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      - uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
 
       - name: update workflows
         run: |

.github/workflows/add_label_from_diff.yaml

@@ -22,7 +22,7 @@ jobs:
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: Checkout code
-      uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0

.github/workflows/auto_assign_reviewers.yaml

@@ -11,14 +11,14 @@ jobs:
     name: assign automatically proposed reviewers
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+      - uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 # v6.0.0
         with:
           ref: master
           sparse-checkout: |
             scripts/assign_reviewers.py
 
       - name: Set up Python
-        uses: actions/setup-python@e797f83bcb11b83ae66e0230d6156d7c80228e7c # v6.0.0
+        uses: actions/setup-python@83679a892e2d95755f2dac6acb0bfd1e9ac5d548 # v6.1.0
         with:
           python-version: '3.x'