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

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 2, 2024

Prompted by this Zulip message, 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.


Open in Gitpod

@adomani
Copy link
Collaborator Author

adomani commented Apr 2, 2024

With this PR, the mk_all script becomes part of CI: should it be actionLinted? If so, is it enough to simply move the script to .github/workflows?

@adomani adomani added awaiting-review CI Modifies the continuous integration / deployment setup labels Apr 2, 2024
.github/workflows/build.yml.in Outdated Show resolved Hide resolved
Comment on lines +21 to +24
# assign `targets` to be the input if provided, default to "the usual Mathlib suspects" otherwise
if [ -n "${*}" ]
then
targets=${*}
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.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 7, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 9, 2024
Copy link
Collaborator

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

I think this is a good change and a clear step forward. Thank you for refactoring mathlib's CI!

Re-writing the mk_all script in Lean is another step forward, but I don't see a reason to block this step on that. I have only minor comments - with these addressed (most by simply merging master), I'll approve.

.github/workflows/bors.yml Outdated Show resolved Hide resolved
.github/workflows/bors.yml Outdated Show resolved Hide resolved
.github/workflows/build.yml Outdated Show resolved Hide resolved
.github/workflows/build.yml Outdated Show resolved Hide resolved
.github/workflows/build.yml.in Outdated Show resolved Hide resolved
.github/workflows/nightly_detect_failure.yml Outdated Show resolved Hide resolved
scripts/mk_all.sh Show resolved Hide resolved
scripts/mk_all.sh Show resolved Hide resolved
scripts/mk_all.sh Outdated Show resolved Hide resolved
Comment on lines +21 to +24
# assign `targets` to be the input if provided, default to "the usual Mathlib suspects" otherwise
if [ -n "${*}" ]
then
targets=${*}
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.

@grunweg
Copy link
Collaborator

grunweg commented May 23, 2024

I do wonder about the duplication in mathlib's CI - did you really have to write the same thing four times? But this is beyond this PR...

@grunweg grunweg added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 23, 2024
Copy link
Collaborator Author

@adomani adomani left a comment

Choose a reason for hiding this comment

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

Michael, as usual, thank you so much for your comments!

I have accepted them all and merged master: the PR is much cleaner now!

.github/workflows/bors.yml Outdated Show resolved Hide resolved
.github/workflows/bors.yml Outdated Show resolved Hide resolved
.github/workflows/build.yml Outdated Show resolved Hide resolved
scripts/mk_all.sh Show resolved Hide resolved
scripts/mk_all.sh Show resolved Hide resolved
scripts/mk_all.sh Outdated Show resolved Hide resolved
@adomani adomani added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 23, 2024
@grunweg
Copy link
Collaborator

grunweg commented May 23, 2024

Thanks for so quickly addressing my comments. I think this is worth trying out; see my comment above for details.
maintainer merge

Copy link

🚀 Pull request has been placed on the maintainer queue by grunweg.

Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 24, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 24, 2024
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.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: update mk_all script and use it in CI [Merged by Bors] - chore: update mk_all script and use it in CI May 24, 2024
@mathlib-bors mathlib-bors bot closed this May 24, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/merge_mk_all branch May 24, 2024 04:42
grunweg pushed a commit that referenced this pull request May 24, 2024
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.
callesonne pushed a commit that referenced this pull request Jun 4, 2024
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.
js2357 pushed a commit that referenced this pull request Jun 18, 2024
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Modifies the continuous integration / deployment setup maintainer-merge ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants