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.

Sign up for GitHub

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

Jump to bottom

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

Closed
wants to merge 11 commits into from
Closed

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
55e19e9
Update mk_all script
adomani Apr 2, 2024
28dd50b
Use mk_all in CI
adomani Apr 2, 2024
36a5e34
Typo
adomani Apr 2, 2024
f0590b0
Merge remote-tracking branch 'origin/master' into adomani/merge_mk_all
adomani May 7, 2024
ae1480a
Merge remote-tracking branch 'origin/master' into adomani/merge_mk_all
adomani May 9, 2024
906a036
remove chmod
adomani May 9, 2024
c5627d3
remove mathlibextras and update action
adomani May 9, 2024
dfa2266
really remove chmod
adomani May 9, 2024
19b31d7
remove one more
adomani May 9, 2024
003dcfc
Merge remote-tracking branch 'origin/master' into adomani/merge_mk_all
adomani May 23, 2024
e160b37
Michael's comments
adomani May 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 3 additions & 15 deletions .github/workflows/bors.yml
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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 •
edited
Loading

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 •
edited
Loading

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