feat: lake exe mk_all in CI (#11874)

This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.



Co-authored-by: Yaël Dillies <[email protected]>

.github/workflows/bors.yml

@@ -64,24 +64,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_imported:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: Check all files imported
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
-        run: |
-          ./scripts/mk_all.sh
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -152,7 +134,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          ./scripts/mk_all.sh Mathlib
+          lake exe mk_all --lib Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -166,6 +148,12 @@ jobs:
           lean --version
           lake --version
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all
+
+      - name: check_imported
+        run: git diff --exit-code
+
       - name: build cache
         run: |
           lake build cache
@@ -319,7 +307,7 @@ jobs:
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'
-    needs: [style_lint, build, check_imported]
+    needs: [style_lint, build]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4

.github/workflows/build.yml

@@ -71,24 +71,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_imported:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: Check all files imported
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
-        run: |
-          ./scripts/mk_all.sh
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -159,7 +141,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          ./scripts/mk_all.sh Mathlib
+          lake exe mk_all --lib Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -173,6 +155,12 @@ jobs:
           lean --version
           lake --version
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all
+
+      - name: check_imported
+        run: git diff --exit-code
+
       - name: build cache
         run: |
           lake build cache
@@ -326,7 +314,7 @@ jobs:
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'
-    needs: [style_lint, build, check_imported]
+    needs: [style_lint, build]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4

.github/workflows/build.yml.in

@@ -50,24 +50,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_imported:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: Check all files importedJOB_NAME
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
-        run: |
-          ./scripts/mk_all.sh
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: check workflowsJOB_NAME
@@ -138,7 +120,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          ./scripts/mk_all.sh Mathlib
+          lake exe mk_all --lib Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -152,6 +134,12 @@ jobs:
           lean --version
           lake --version
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all
+
+      - name: check_imported
+        run: git diff --exit-code
+
       - name: build cache
         run: |
           lake build cache
@@ -305,7 +293,7 @@ jobs:
   final:
     name: Post-CI jobJOB_NAME
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    needs: [style_lint, build, check_imported]
+    needs: [style_lint, build]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4

.github/workflows/build_fork.yml

@@ -68,24 +68,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_imported:
-    if: github.repository != 'leanprover-community/mathlib4'
-    name: Check all files imported (fork)
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
-        run: |
-          ./scripts/mk_all.sh
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository != 'leanprover-community/mathlib4'
     name: check workflows (fork)
@@ -156,7 +138,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          ./scripts/mk_all.sh Mathlib
+          lake exe mk_all --lib Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
@@ -170,6 +152,12 @@ jobs:
           lean --version
           lake --version
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all
+
+      - name: check_imported
+        run: git diff --exit-code
+
       - name: build cache
         run: |
           lake build cache
@@ -323,7 +311,7 @@ jobs:
   final:
     name: Post-CI job (fork)
     if: github.repository != 'leanprover-community/mathlib4'
-    needs: [style_lint, build, check_imported]
+    needs: [style_lint, build]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4