[Merged by Bors] - chore: update mk_all script and use it in CI #11849
Conversation
|
With this PR, the |
adomani
added
awaiting-review
CI
| # assign `targets` to be the input if provided, default to "the usual Mathlib suspects" otherwise | ||
| if [ -n "${*}" ] | ||
| then | ||
| targets=${*} |
There was a problem hiding this comment.
I don't know enough bash to review this, but would approve the CI changes.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
There was a problem hiding this comment.
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.
| # assign `targets` to be the input if provided, default to "the usual Mathlib suspects" otherwise | ||
| if [ -n "${*}" ] | ||
| then | ||
| targets=${*} |
There was a problem hiding this comment.
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.
|
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
added
awaiting-author
adomani
added
awaiting-review
and removed
awaiting-author
|
Thanks for so quickly addressing my comments. I think this is worth trying out; see my comment above for details. |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
leanprover-community-mathlib4-bot
added
ready-to-merge
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.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
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.
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.
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.
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_allscript: if you pass it a space-separated list of target dirs, it will produce 'import files' for each dir in the list.