Skip to content

Commit

Permalink
perf: do not import Lean.Elab.Frontend from Lake
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner authored and tydeu committed May 15, 2022
1 parent d961d8c commit eef91c7
Show file tree
Hide file tree
Showing 6 changed files with 3 additions and 8 deletions.
1 change: 0 additions & 1 deletion Lake.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,4 @@ Authors: Mac Malone
import Lake.Build
import Lake.Config
import Lake.DSL
import Lake.CLI
import Lake.Version
2 changes: 0 additions & 2 deletions Lake/Config.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 1 addition & 2 deletions Lake/Config/Glob.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 0 additions & 2 deletions Lake/Config/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Lake/DSL/Commands.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
1 change: 1 addition & 0 deletions Lake/Main.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: 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)

0 comments on commit eef91c7

Please sign in to comment.