[Merged by Bors] - feat: `lake exe mk_all` as a Lean executable #11853

adomani · 2024-04-02T16:15:59Z

Running

lake exe mk_all --git

should have the same effect as running

./script/mk_all.sh

that is, it creates the files Mathlib.lean, Mathlib/Tactic.lean, Archive.lean, Counterexamples.lean.

It does not create analogous files for Cache and LongestPole.

lake exe mk_all

is similar, but uses all the .lean files in Mathlib, not just the Git-managed ones.

See #11874 for using the script in CI.

YaelDillies · 2024-04-05T09:07:14Z

@joneugster, do you think the same thing here as on #8361?

joneugster · 2024-04-06T04:58:04Z

Not necessarily. I personally care about import-analysis tools being outside of mathlib because I want to use them in my projects without importing mathlib.

But generally, while having separate packages with useful utilities is nice for projects not depending on mathlib, with the current in-development state of lake, it's still quite tedious to keep all packages in sync and up to date...

And finally, it's quite quick to extract useful stuff out of mathlib, once somebody concretely needs it. (The only reason I see to directly PR to a separate repo is that one can save some reviewer capacity if it's only utility-code)

adomani · 2024-04-06T07:13:57Z

I also think that "import" requirements are quite project-specific.

Even this tool is not just "import all files and/or all libraries":

Cache is not created;
Mathlib/Tactic should also be created.

Std has its own tool that does something way more sophisticated.

It seems like one of these commands that are hard to implement in a way that pleases most projects.

grunweg · 2024-05-24T17:44:55Z

Thanks for the quick response! I'll trust Mario and Kim on getLeanLibs, so this PR looks good to go, from my side.
maintainer merge

github-actions · 2024-05-24T17:45:09Z

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

Vierkantor

This looks plausible enough to me but I don't have any real Lean scripting experience so I'm hesitant to give definitive judgement.

scripts/mk_all.lean

Vierkantor

Thanks for the changes! I'm going to hold off on merging as I said, so let's kick this back on the maintainer queue:

maintainer merge

github-actions · 2024-05-28T10:30:59Z

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

grunweg · 2024-05-29T13:29:32Z

I've proposed moving the common code into Mathlib/Utils in #13339.

kim-em · 2024-05-29T17:01:17Z

bors merge

Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors · 2024-05-29T18:15:35Z

Pull request successfully merged into master.

Build succeeded:

This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Yaël Dillies <[email protected]>

This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

… `scripts` (#13339) With #13245, two scripts in `scripts` would like to use very similar information: move it to a central place instead (a file in `Mathlib/Util`). Suggestions for better locations are welcome! Also, split the `getAll` function in two pieces, getting the file names and transforming this into module names. While #11853 only requires the latter, #13245 needs the former (which is computed anyway). Only accessible the converted module names and converting them back to files would be absurd. - [x] depends on: #11853 which adds these utility functions