chore: don't import Lake under Mathlib (#13779)

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. 




Co-authored-by: Matthew Robert Ballard <[email protected]>

Mathlib/Util/GetAllModules.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kim Morrison, Damiano Testa
 -/
 
 import Lean.Util.Path
-import Lake.CLI.Main
 
 
 /-!
@@ -55,18 +54,3 @@ def getAllModules (git : Bool) (ml : String) : IO (Array String) := do
   return ← files.mapM fun f => do
      return (← moduleNameOfFileName f none).toString
 
-open Lake in
-/-- `getLeanLibs` returns the names (as an `Array` of `String`s) of all the libraries
-on which the current project depends.
-If the current project is `mathlib`, then it excludes the libraries `Cache` and `LongestPole` and
-it includes `Mathlib/Tactic`. -/
-def getLeanLibs : IO (Array String) := do
-  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
-  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
-  let ws ← MonadError.runEIO (MainM.runLogIO (loadWorkspace config)).toEIO
-  let package := ws.root
-  let libs := (package.leanLibs.map (·.name)).map (·.toString)
-  return if package.name == `mathlib then
-    libs.erase "Cache" |>.erase "LongestPole" |>.push ("Mathlib".push pathSeparator ++ "Tactic")
-  else
-    libs

lakefile.lean

@@ -36,7 +36,7 @@ require importGraph from git "https://github.com/leanprover-community/import-gra
 lean_lib Mathlib
 
 -- NB. When adding further libraries, check if they should be excluded from `getLeanLibs` in
--- `Mathlib/Util/GetAllModules.lean`.
+-- `scripts/mk_all.lean`.
 lean_lib Cache
 lean_lib LongestPole
 lean_lib Archive

scripts/mk_all.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Damiano Testa
 -/
 import Cli.Basic
+import Lake.CLI.Main
 import Mathlib.Util.GetAllModules
 
 /-!
@@ -15,6 +16,22 @@ This file declares a command to gather all Lean files from a folder into a singl
 
 open Lean System.FilePath
 
+open Lake in
+/-- `getLeanLibs` returns the names (as an `Array` of `String`s) of all the libraries
+on which the current project depends.
+If the current project is `mathlib`, then it excludes the libraries `Cache` and `LongestPole` and
+it includes `Mathlib/Tactic`. -/
+def getLeanLibs : IO (Array String) := do
+  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
+  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+  let ws ← MonadError.runEIO (MainM.runLogIO (loadWorkspace config)).toEIO
+  let package := ws.root
+  let libs := (package.leanLibs.map (·.name)).map (·.toString)
+  return if package.name == `mathlib then
+    libs.erase "Cache" |>.erase "LongestPole" |>.push ("Mathlib".push pathSeparator ++ "Tactic")
+  else
+    libs
+
 open IO.FS IO.Process Name Cli in
 /-- Implementation of the `mk_all` command line program.
 The exit code is the number of files that the command updates/creates. -/