Trigger CI for leanprover-community/batteries#813

Author: leanprover-community-mathlib4-bot

.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:

.github/build.in.yml

@@ -4,6 +4,14 @@
 ### NB: and regenerate those files by manually running
 ### NB: .github/workflows/mk_build_yml.sh
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -119,15 +127,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          # 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: |
@@ -156,6 +155,10 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
+      - name: print the sizes of the oleans
+        run: |
+          du .lake/build/lib/Mathlib || echo "This code should be unreachable"
+
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
         # but not if any earlier step failed or was cancelled.
@@ -237,13 +240,23 @@ 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: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -256,7 +269,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake

.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"

.github/workflows/PR_summary.yml

@@ -5,6 +5,7 @@ on:
 
 jobs:
   build:
+    name: "post-or-update-summary-comment"
     runs-on: ubuntu-latest
 
     steps:

.github/workflows/add_label_from_comment.yml

@@ -27,7 +27,7 @@ jobs:
         run: |
           {
             cat scripts/bench_summary.lean
-            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4"' "${PR}"
+            printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4" %s' "${PR}" "${{ github.run_id }}"
           } |
             lake env lean --stdin
         env:

.github/workflows/add_label_from_review.yml

@@ -14,6 +14,14 @@ on:
 
 name: continuous integration (staging)
 
+env:
+  # Disable Lake's automatic fetching of cloud builds.
+  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
+  # This is because Mathlib's Cache assumes all build aritfacts present in the build directory
+  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
+  # not necessarily satisfy this property.
+  LAKE_NO_CACHE: true
+
 jobs:
   # Cancels previous runs of jobs in this file
   cancel:
@@ -129,15 +137,6 @@ jobs:
         run: |
           lake build cache
 
-      - name: prune ProofWidgets .lake
-        run: |
-          # 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: |
@@ -166,6 +165,10 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
+      - name: print the sizes of the oleans
+        run: |
+          du .lake/build/lib/Mathlib || echo "This code should be unreachable"
+
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
         # but not if any earlier step failed or was cancelled.
@@ -247,13 +250,23 @@ 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: verify `lake exe graph` works
-        run: |
-          lake exe graph
-          rm import_graph.dot
+      - name: generate our import graph
+        run: lake exe graph
+
+      - name: upload the import graph
+        uses: actions/upload-artifact@v4
+        with:
+          name: import-graph
+          path: import_graph.dot
+          ## the default is 90, but we build often, so unless there's a reason
+          ## to care about old copies in the future, just say 7 days for now
+          retention-days: 7
+
+      - name: clean up the import graph file
+        run: rm import_graph.dot
 
       - name: build everything
         # make sure everything is available for test/import_all.lean
@@ -266,7 +279,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake