diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index eeafbeac95416..a7dab0f417248 100644 --- 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 index 83b6be7ea187b..2b497560d1427 100644 --- 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 index 0ca479fa5c856..669f29d5faff4 100644 --- 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 index c02e0a81d7868..3b7aa7d1af9ae 100644 --- 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 index 9dd40744e8f3f..2dd1c52756af6 100644 --- 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 index d5712ee52b116..b02c9d9787d4f 100755 --- 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 +## +## for each dir in , 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