chore: update mk_all script and use it in CI (#11849)

Prompted by [this Zulip message](https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/430753770), I unified all the uses that I could find of "list all files in some dir and create an 'import file' for them". In the process, I added a slight flexibility to the `mk_all` script: if you pass it a space-separated list of target dirs, it will produce 'import files' for each dir in the list.
leanprover-community · Jun 4, 2024 · 613a154 · 613a154
1 parent 0e249c5
commit 613a154
Show file tree

Hide file tree

Showing 6 changed files with 46 additions and 75 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -75,21 +75,9 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
+      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
         run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
+          ./scripts/mk_all.sh
 
       - name: check that all files are imported
         run: git diff --exit-code
@@ -164,7 +152,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          ./scripts/mk_all.sh Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -82,21 +82,9 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
+      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
         run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
+          ./scripts/mk_all.sh
 
       - name: check that all files are imported
         run: git diff --exit-code
@@ -171,7 +159,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          ./scripts/mk_all.sh Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -61,21 +61,9 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
+      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
         run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
+          ./scripts/mk_all.sh
 
       - name: check that all files are imported
         run: git diff --exit-code
@@ -150,7 +138,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          ./scripts/mk_all.sh Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -79,21 +79,9 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
+      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
         run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
+          ./scripts/mk_all.sh
 
       - name: check that all files are imported
         run: git diff --exit-code
@@ -168,7 +156,7 @@ jobs:
       # but verify that this didn't change anything in the `check_imported` job.
       - name: update Mathlib.lean
         run: |
-          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          ./scripts/mk_all.sh Mathlib
 
       - name: If using a lean-pr-release toolchain, uninstall
         run: |

diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
@@ -57,21 +57,9 @@ jobs:
 
       - uses: actions/checkout@v4
 
-      - name: update Mathlib.lean
+      - name: import files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
         run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
+          ./scripts/mk_all.sh
 
       - name: suggester / import list
         uses: reviewdog/action-suggester@v1

diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh
@@ -1,6 +1,37 @@
 #! /usr/bin/env bash
+
+# Generate a file importing all the files of a Lean folder.
+# By default, it generates the files for the libraries
+# `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean` and `Counterexamples.lean`.
+
+##  Standard use:
+##  ./scripts/mk_all.sh
+##
+##  updates `Mathlib` `Mathlib/Tactic` `Counterexamples` `Archive`
+##
+##  Advanced use:
+##  ./scripts/mk_all.sh <space_separated_list_of_dirs>
+##
+##  for each dir in <space_separated_list_of_dirs>, create a file with all the imports of the dir
+##
+##  The two commands
+##  ./scripts/mk_all.sh
+##  ./scripts/mk_all.sh Mathlib Mathlib/Tactic Counterexamples Archive
+##
+##  are equivalent.
+
 cd "$(git rev-parse --show-toplevel)" || exit 1
-for gp in Mathlib Mathlib/Tactic Counterexamples Archive
+
+# assign `targets` to be the input if provided, default to "the usual Mathlib suspects" otherwise
+if [ -n "${*}" ]
+then
+  targets=${*}
+else
+  targets="Mathlib Mathlib/Tactic Counterexamples Archive"
+fi
+
+## Note: *no* quotes around `${targets}`, since we want the spaces to matter
+for gp in ${targets}
 do
   git ls-files "$gp/*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > "$gp.lean"
 done