From eef91c7760f547b4dad0ecef17c084eb97a954ce Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 15 May 2022 17:07:30 +0200
Subject: [PATCH] perf: do not import Lean.Elab.Frontend from Lake

---
 Lake.lean                | 1 -
 Lake/Config.lean         | 2 --
 Lake/Config/Glob.lean    | 3 +--
 Lake/Config/Package.lean | 2 --
 Lake/DSL/Commands.lean   | 2 +-
 Lake/Main.lean           | 1 +
 6 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/Lake.lean b/Lake.lean
index 6e7bcf82a19c7..1475725368872 100644
--- a/Lake.lean
+++ b/Lake.lean
@@ -6,5 +6,4 @@ Authors: Mac Malone
 import Lake.Build
 import Lake.Config
 import Lake.DSL
-import Lake.CLI
 import Lake.Version
diff --git a/Lake/Config.lean b/Lake/Config.lean
index 3d4966752f6ef..696ee8b589f5d 100644
--- a/Lake/Config.lean
+++ b/Lake/Config.lean
@@ -10,6 +10,4 @@ import Lake.Config.Script
 import Lake.Config.Package
 import Lake.Config.Monad
 import Lake.Config.SearchPath
-import Lake.Config.Resolve
-import Lake.Config.Load
 import Lake.Config.Util
diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean
index ef31f354dbd27..18be1ab7a2088 100644
--- a/Lake/Config/Glob.lean
+++ b/Lake/Config/Glob.lean
@@ -3,8 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Mac Malone
 -/
-import Lean.Data.Name
-import Lean.Elab.Import
+import Lean.Util.Path
 
 open Lean (Name)
 open System (FilePath)
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 7ae7e4f0cf88c..e67d44cb1d072 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -3,8 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lean.Data.Name
-import Lean.Elab.Import
 import Std.Data.HashMap
 import Lake.Build.TargetTypes
 import Lake.Config.Glob
diff --git a/Lake/DSL/Commands.lean b/Lake/DSL/Commands.lean
index fb59940bf2f1a..4401520f29591 100644
--- a/Lake/DSL/Commands.lean
+++ b/Lake/DSL/Commands.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.Parser
+import Lean.Parser.Command
 import Lake.Config.Package
 import Lake.DSL.Attributes
 
diff --git a/Lake/Main.lean b/Lake/Main.lean
index 30779fdf04ab6..620b9bd485f3a 100644
--- a/Lake/Main.lean
+++ b/Lake/Main.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake
+import Lake.CLI
 
 def main (args : List String) : IO UInt32 := do
   Lake.cli args -- should not throw errors (outside user code)