[Merged by Bors] - chore: don't import Lake under Mathlib

[mattrobball]

The Lake.CLI.Main import was slowing down linting by ~90s/~15% on its own. We move the function getLeanLibs back to scripts/mk_all.lean to avoid the import.

---

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 51d110d.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9d4d9e4.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
- build       linting          5.2%
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.6%

[mattrobball]

!bench

[grunweg]

Thanks a lot for investigating this - I would have been (and still am) completely stumped by them!

[leanprover-bot]

Here are the benchmark results for commit 87579f6.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
- build       linting          7.2%
+ lint        instructions   -12.5%
+ lint        wall-clock     -13.8%

[mattrobball]

Adding the file to nolints.json with all linters didn't make a difference in the regression

[mattrobball]

Oh wait. I'm reading this wrong. The file itself is fine.

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit d2f495e.
There were no significant changes against commit bffb043.

[mattrobball]

Until it is added to Mathlib.lean, and then even blacklisting all the linters in nolints.json doesn't help

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 18cb303.
There were significant changes against commit bffb043:

  Benchmark   Metric    Change
  ============================
- build       linting     6.9%

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9ab3ce4.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

[mattrobball]

!bench

[github-actions]

PR summary 3d9182a4a1

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Util.GetAllModules	2	1	-1 (-50.00%)

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[grunweg]

Wow, thanks a lot for finding this! As a next step, I'll augment the Python lint to complain about any lake imports in Mathlib, referring to this issue :-)

This PR is just code motion, so looks fine to me. My original use-case #13245 doesn't need getLeanLibs anyway (and its proposed replacement won't either), so moving this function back looks good to me.

[grunweg]

Actually, since you marked this as awaiting-review and CI on this was successful previously, let me go straight to
maintainer merge

[github-actions]

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

[leanprover-bot]

Here are the benchmark results for commit 16c93ae.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

[robertylewis]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style