feat: `lake exe mk_all` as a Lean executable

[adomani]

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]

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

[joneugster]

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]

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]

I just reviewed the script (and some CI bits) in #11874. Summarising what I said there: looks very good, I only have minor comments.

[grunweg]

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[bot]]

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

[github-actions[bot]]

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

[grunweg]

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

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style