fix: reduce imports for scripts (#6716)

As [noted on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20exe.20cache.20get.20broken.3F/near/386489865), a from-scratch build of mathlib after `lake exe cache get` will compile all of `Std` due to some unnecessary imports. With a few well chosen import reductions we only end up having to compile ~20 files instead of ~300 files (compile meaning `Compiling`, generating the arch-dependent `.o` files that are not in the cache).
leanprover-community · Aug 24, 2023 · 891adb3 · 891adb3
1 parent f5f38ed
commit 891adb3
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 3 deletions.
diff --git a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+import Mathlib.Init.Align
 import Mathlib.CategoryTheory.Abelian.Exact
 import Mathlib.CategoryTheory.Over
 import Mathlib.Algebra.Category.ModuleCat.EpiMono

diff --git a/Mathlib/Data/Real/CauSeq.lean b/Mathlib/Data/Real/CauSeq.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.GroupTheory.GroupAction.Pi
+import Mathlib.Init.Align
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Ring
 

diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import Mathlib.Init.Align
 import Mathlib.Topology.LocalHomeomorph
 
 #align_import geometry.manifold.charted_space from "leanprover-community/mathlib"@"431589bce478b2229eba14b14a283250428217db"

diff --git a/Mathlib/Tactic/ToLevel.lean b/Mathlib/Tactic/ToLevel.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import Lean
-import Mathlib.Init.Align
+import Mathlib.Mathport.Rename
 import Mathlib.Tactic.PPWithUniv
 
 /-! # `ToLevel` class

diff --git a/scripts/checkYaml.lean b/scripts/checkYaml.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 
-import Mathlib.Tactic.Basic
 import Mathlib.Tactic.ToExpr
 
 /-! # Script to check `undergrad.yaml`, `overview.yaml`, and `100.yaml`
@@ -15,7 +14,7 @@ It verifies that the referenced declarations exist.
 -/
 
 open IO.FS Lean Lean.Elab
-open Lean Core Elab Command Std.Tactic.Lint
+open Lean Core Elab Command
 
 abbrev DBFile := Array (String × Name)