Skip to content

Commit

Permalink
chore: don't import Lake under Mathlib (#13779)
Browse files Browse the repository at this point in the history
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]>
  • Loading branch information
2 people authored and AntoineChambert-Loir committed Jun 20, 2024
1 parent d0c24eb commit 1b4df4f
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 17 deletions.
16 changes: 0 additions & 16 deletions Mathlib/Util/GetAllModules.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kim Morrison, Damiano Testa
-/

import Lean.Util.Path
import Lake.CLI.Main


/-!
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 17 additions & 0 deletions scripts/mk_all.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

/-!
Expand All @@ -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. -/
Expand Down

0 comments on commit 1b4df4f

Please sign in to comment.