Trigger CI for leanprover-community/batteries#1055

.github/build.in.yml

@@ -156,6 +156,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.
@@ -266,7 +270,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake

.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/bench_summary_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/bors.yml

@@ -166,6 +166,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.
@@ -276,7 +280,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake

.github/workflows/build.yml

@@ -173,6 +173,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.
@@ -283,7 +287,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake

.github/workflows/build_fork.yml

@@ -170,6 +170,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.
@@ -280,7 +284,7 @@ jobs:
         with:
           linters: gcc
           run:
-            lake test
+            lake --iofail test
 
       - name: check for unused imports
         id: shake