Merge branch 'master' into complete-equipartite-subgraph

Author: mitchell-horner

.github/build.in.yml

@@ -38,7 +38,7 @@ 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: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -238,6 +238,51 @@ jobs:
             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
@@ -412,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"
@@ -443,11 +488,13 @@ 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' }}

.github/workflows/bors.yml

@@ -48,7 +48,7 @@ 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: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -248,6 +248,51 @@ jobs:
             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
@@ -422,7 +467,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"
@@ -453,11 +498,13 @@ 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' }}

.github/workflows/build.yml

@@ -55,7 +55,7 @@ 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: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -255,6 +255,51 @@ jobs:
             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
@@ -429,7 +474,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"
@@ -460,11 +505,13 @@ 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' }}

.github/workflows/build_fork.yml

@@ -52,7 +52,7 @@ 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: # note that .pr-branch/.lake must be created in a step below before we use this
@@ -252,6 +252,51 @@ jobs:
             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
@@ -426,7 +471,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"
@@ -457,11 +502,13 @@ 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' }}

.github/workflows/remove_deprecated_decls.yml

@@ -168,13 +168,13 @@ jobs:
       id: get-branch-sha
       run: |
         # Check if the branch exists remotely
-        if git fetch origin "$BRANCH_NAME"; then
-          SHA=$(git rev-parse "origin/$BRANCH_NAME")
+        SHA=$(git ls-remote --heads origin "$BRANCH_NAME" | awk '{print $1}')
+        if [ -n "$SHA" ]; then
           echo "Branch '$BRANCH_NAME' exists with SHA: $SHA"
           echo "sha=$SHA" >> "${GITHUB_OUTPUT}"
         else
           echo "Branch '$BRANCH_NAME' does not exist"
-          echo "sha=" >>" ${GITHUB_OUTPUT}"
+          echo "sha=" >> "${GITHUB_OUTPUT}"
         fi
 
     - name: Get PR

.github/workflows/update_dependencies.yml

@@ -29,13 +29,13 @@ jobs:
         id: get-branch-sha
         run: |
           # Check if the branch exists remotely
-          if git fetch origin "$BRANCH_NAME"; then
-            SHA=$(git rev-parse "origin/$BRANCH_NAME")
+          SHA=$(git ls-remote --heads origin "$BRANCH_NAME" | awk '{print $1}')
+          if [ -n "$SHA" ]; then
             echo "Branch '$BRANCH_NAME' exists with SHA: $SHA"
             echo "sha=$SHA" >> "${GITHUB_OUTPUT}"
           else
             echo "Branch '$BRANCH_NAME' does not exist"
-            echo "sha=" >>" ${GITHUB_OUTPUT}"
+            echo "sha=" >> "${GITHUB_OUTPUT}"
           fi
 
       - name: Get PR and labels

Archive/Hairer.lean

@@ -38,7 +38,7 @@ variable (𝕜 E F) in
 /-- The set of `C^n` functions supported in a set `s`, as a submodule of the space of functions. -/
 def ContDiffSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
   carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
-  add_mem' hf hg := ⟨tsupport_add.trans <| union_subset hf.1 hg.1, hf.2.add hg.2⟩
+  add_mem' hf hg := ⟨(tsupport_add _ _).trans <| union_subset hf.1 hg.1, hf.2.add hg.2⟩
   zero_mem' :=
     ⟨(tsupport_eq_empty_iff.mpr rfl).subset.trans (empty_subset _), contDiff_const (c := 0)⟩
   smul_mem' r f hf :=