Commit 2024-06-14 15:55 f43a3d28

View on Github →

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.

Estimated changes

Modified Mathlib/Util/GetAllModules.lean

deleted def getLeanLibs

Modified lakefile.lean

Modified scripts/mk_all.lean

added def getLeanLibs