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: Michael Rothgang <rothgami@math.hu-berlin.de> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
leanprover-community · Jun 7, 2024 · c6c28c0 · c6c28c0
1 parent 6b50dc5
commit c6c28c0
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 83 deletions.
diff --git a/.github/workflows/bors.yml b/.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

diff --git a/.github/workflows/build.yml b/.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

diff --git a/.github/workflows/build.yml.in b/.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

diff --git a/.github/workflows/build_fork.yml b/.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

diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
@@ -57,9 +57,18 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: import files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
+      - name: install elan
         run: |
-          ./scripts/mk_all.sh
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all
+
+      - name: check_imported
+        run: git diff --exit-code
 
       - name: suggester / import list
         uses: reviewdog/action-suggester@v1

diff --git a/bors.toml b/bors.toml
@@ -1,4 +1,4 @@
-status = ["Build", "Lint style", "Check all files imported"]
+status = ["Build", "Lint style"]
 use_squash_merge = true
 timeout_sec = 28800
 block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI"]