From cd2b72c170e19416d10ad533d7a41134daa8a8fd Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Fri, 14 Jun 2024 15:32:54 +0000 Subject: [PATCH] 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 <100034030+mattrobball@users.noreply.github.com> --- Mathlib/Util/GetAllModules.lean | 16 ---------------- lakefile.lean | 2 +- scripts/mk_all.lean | 17 +++++++++++++++++ 3 files changed, 18 insertions(+), 17 deletions(-) diff --git a/Mathlib/Util/GetAllModules.lean b/Mathlib/Util/GetAllModules.lean index 0e17c91446379a..daeb1a2c59e20f 100644 --- a/Mathlib/Util/GetAllModules.lean +++ b/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 diff --git a/lakefile.lean b/lakefile.lean index 4b1ad1961db300..dca2169610d184 100644 --- a/lakefile.lean +++ b/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 diff --git a/scripts/mk_all.lean b/scripts/mk_all.lean index 037296860c1ebd..691979b1ad64a7 100644 --- a/scripts/mk_all.lean +++ b/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. -/