Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: update mk_all script and use it in CI #11849

Closed
wants to merge 11 commits into from
18 changes: 3 additions & 15 deletions .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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: |
Expand Down
18 changes: 3 additions & 15 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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: |
Expand Down
18 changes: 3 additions & 15 deletions .github/workflows/build.yml.in
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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: |
Expand Down
18 changes: 3 additions & 15 deletions .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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: |
Expand Down
16 changes: 2 additions & 14 deletions .github/workflows/lint_and_suggest_pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -57,21 +57,9 @@ jobs:

- uses: actions/checkout@v4

- name: update Mathlib.lean
- name: import files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
adomani marked this conversation as resolved.
Show resolved Hide resolved
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
Expand Down
33 changes: 32 additions & 1 deletion scripts/mk_all.sh
Original file line number Diff line number Diff line change
@@ -1,6 +1,37 @@
#! /usr/bin/env bash

adomani marked this conversation as resolved.
Show resolved Hide resolved
# 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`
adomani marked this conversation as resolved.
Show resolved Hide resolved
##
## 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=${*}
Comment on lines +25 to +28
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know enough bash to review this, but would approve the CI changes.

Copy link
Collaborator Author

@adomani adomani Apr 18, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If it helps, -n checks whether the variable is assigned and non empty. $* means "all arguments passed to the function".

Basically, either the user passes some arguments and the script uses those, or, we use the default set of arguments.

Copy link
Collaborator

@grunweg grunweg May 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've looked at this enough to convince myself this should do what it says.

I do think bash scripts are not nice to maintain long-term --- but since #11874 is rewriting this in Lean, I am not worried about that. Short-term, this seems fine and like a clear step forward.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thinking about this again, I don't see the use case for passing arguments to this script. Unless there's a strong reason for it that I haven't thought about, I'd revert that part. The main selling point of this script is that it's simple and fast, IMO.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The reason I added that option is for downstream projects that can target whichever folder they want. This was before the lean script, though.

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
Loading