Merge remote-tracking branch 'origin/master' into chrisflav-std-smoot…

…h-unramified-prereqs
leanprover-community · Jan 7, 2025 · 4aef670 · 4aef670
2 parents d752d6c + 9e3f841
commit 4aef670
Show file tree

Hide file tree

Showing 2,532 changed files with 70,715 additions and 33,074 deletions.
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md
@@ -20,7 +20,7 @@ If you are moving or deleting declarations, please include these lines at the bo
 (that is, before the `---`) using the following format:
 
 Moves:
-- Vector.* -> Mathlib.Vector.*
+- Vector.* -> List.Vector.*
 - ...
 
 Deletions:

diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -12,19 +12,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+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) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: Lint styleJOB_NAME
@@ -127,16 +123,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |
@@ -250,7 +236,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -3,7 +3,8 @@ version: 2  # Specifies the version of the Dependabot configuration file format
 updates:
   # Configuration for dependency updates
   - package-ecosystem: "github-actions"  # Specifies the ecosystem to check for updates
-    directory: "/"  # Specifies the directory to check for dependencies; "/" means the root directory
+    directories: 
+      - "/.github/*" # covers `build.in.yml` as well, which is not in `.github/workflows/` because it shouldn't be run in CI.
     schedule:
       # Check for updates to GitHub Actions every month
       interval: "monthly"
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -22,19 +22,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+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) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style
@@ -137,16 +133,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |
@@ -260,7 +246,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -29,19 +29,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+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) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style
@@ -144,16 +140,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |
@@ -267,7 +253,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -26,19 +26,15 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/[email protected]
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+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) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Lint style (fork)
@@ -141,16 +137,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          lake build proofwidgets:release
-          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
-          # but also `.oleans`, which may have been built with the wrong toolchain.
-          # This removes them.
-          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
-          rm -rf .lake/packages/proofwidgets/.lake/build/lib
-          rm -rf .lake/packages/proofwidgets/.lake/build/ir
-
       - name: get cache
         id: get
         run: |
@@ -264,7 +250,7 @@ jobs:
 
       - name: check declarations in db files
         run: |
-          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
           lake exe check-yaml
 
       - name: generate our import graph