refactor: reorganize code folder structure

2021-11-09 22:30:18 -05:00 · 2021-11-09 22:30:18 -05:00 · 331bf0f7f2
commit 331bf0f7f2
parent ce7779890b
33 changed files with 171 additions and 157 deletions
--- a/Lake.lean
+++ b/Lake.lean
@ -3,30 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Async
-import Lake.Attributes
-import Lake.BuildBin
-import Lake.BuildModule
-import Lake.BuildMonad
-import Lake.BuildPackage
-import Lake.BuildTarget
-import Lake.BuildTargets
-import Lake.BuildTop
-import Lake.Cli
-import Lake.CliT
-import Lake.Compile
+import Lake.Build
+import Lake.Config
 import Lake.DSL
-import Lake.Git
-import Lake.Glob
-import Lake.Help
-import Lake.Init
-import Lake.InstallPath
-import Lake.LeanConfig
-import Lake.LeanVersion
-import Lake.Package
-import Lake.Resolve
-import Lake.SearchPath
-import Lake.Target
-import Lake.Task
-import Lake.Trace
+import Lake.CLI
 import Lake.Version
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@ -0,0 +1,12 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.Monad
+import Lake.Build.Actions
+import Lake.Build.TargetTypes
+import Lake.Build.Targets
+import Lake.Build.Module
+import Lake.Build.Package
+import Lake.Build.Binary
--- a/Lake/Build/Actions.lean
+++ b/Lake/Build/Actions.lean
@ -3,7 +3,7 @@ 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 Lake.BuildMonad
+import Lake.Build.Monad

 namespace Lake
 open System
--- a/Lake/Build/Binary.lean
+++ b/Lake/Build/Binary.lean
@ -3,8 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.BuildPackage
-import Lake.BuildTargets
+import Lake.Build.Package
+import Lake.Build.Targets

 open System
 open Lean (Name)
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@ -1,15 +1,15 @@
 /-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
+Authors: Sebastian Ullrich, Mac Malone
 -/
 import Lean.Data.Name
 import Lean.Elab.Import
-import Lake.Target
-import Lake.BuildTarget
-import Lake.BuildTop
-import Lake.Compile
-import Lake.Package
+import Lake.Build.Target
+import Lake.Build.Actions
+import Lake.Build.Recursive
+import Lake.Build.TargetTypes
+import Lake.Config.Package

 open System
 open Lean hiding SearchPath
--- a/Lake/Build/Monad.lean
+++ b/Lake/Build/Monad.lean
@ -3,10 +3,10 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Task
-import Lake.Trace
-import Lake.LogMonad
-import Lake.InstallPath
+import Lake.Util.Task
+import Lake.Build.Trace
+import Lake.Util.LogT
+import Lake.Config.InstallPath

 open System
 namespace Lake
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@ -5,10 +5,9 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lean.Data.Name
 import Lean.Elab.Import
-import Lake.Target
-import Lake.BuildModule
-import Lake.Resolve
-import Lake.Package
+import Lake.Config.Package
+import Lake.Config.Resolve
+import Lake.Build.Module

 open System
 open Lean hiding SearchPath
--- a/Lake/Build/Recursive.lean
+++ b/Lake/Build/Recursive.lean
--- a/Lake/Build/Target.lean
+++ b/Lake/Build/Target.lean
@ -3,8 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Task
-import Lake.Trace
+import Lake.Util.Task
+import Lake.Build.Trace

 open System
 namespace Lake
--- a/Lake/Build/TargetTypes.lean
+++ b/Lake/Build/TargetTypes.lean
@ -3,8 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Target
-import Lake.BuildMonad
+import Lake.Build.Monad
+import Lake.Build.Target

 open System
 namespace Lake
--- a/Lake/Build/Targets.lean
+++ b/Lake/Build/Targets.lean
@ -3,8 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Compile
-import Lake.BuildTarget
+import Lake.Build.Actions
+import Lake.Build.TargetTypes

 open System
 namespace Lake
--- a/Lake/Build/Trace.lean
+++ b/Lake/Build/Trace.lean
--- a/Lake/CLI.lean
+++ b/Lake/CLI.lean
@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.CLI.Help
+import Lake.CLI.Init
+import Lake.CLI.Main
--- a/Lake/CLI/Help.lean
+++ b/Lake/CLI/Help.lean
--- a/Lake/CLI/Init.lean
+++ b/Lake/CLI/Init.lean
@ -3,9 +3,9 @@ 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 Lake.Git
-import Lake.Package
-import Lake.LeanConfig
+import Lake.Util.Git
+import Lake.Config.Package
+import Lake.Config.Load

 namespace Lake
 open Git System
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean.Util.Paths
-import Lake.Init
-import Lake.Help
-import Lake.BuildBin
-import Lake.LeanConfig
-import Lake.SearchPath
-import Lake.InstallPath
-import Lake.MainM
-import Lake.CliT
+import Lake.Config.Load
+import Lake.Config.SearchPath
+import Lake.Config.InstallPath
+import Lake.Util.MainM
+import Lake.Util.CliT
+import Lake.CLI.Init
+import Lake.CLI.Help
+import Lake.Build

 open System
 open Lean (Name LeanPaths Json toJson)
--- a/Lake/Config.lean
+++ b/Lake/Config.lean
@ -0,0 +1,11 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Config.Glob
+import Lake.Config.InstallPath
+import Lake.Config.Package
+import Lake.Config.SearchPath
+import Lake.Config.Resolve
+import Lake.Config.Load
--- a/Lake/Config/Glob.lean
+++ b/Lake/Config/Glob.lean
--- a/Lake/Config/InstallPath.lean
+++ b/Lake/Config/InstallPath.lean
--- a/Lake/Config/Load.lean
+++ b/Lake/Config/Load.lean
@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean.Elab.Frontend
-import Lake.Package
-import Lake.Attributes
+import Lake.DSL.Attributes
+import Lake.Config.Package

 namespace Lake
 open Lean System
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@ -7,9 +7,8 @@ import Lean.Data.Name
 import Lean.Elab.Import
 import Std.Data.HashMap
 import Lake.LeanVersion
-import Lake.BuildTarget
-import Lake.MainM
-import Lake.Glob
+import Lake.Build.TargetTypes
+import Lake.Config.Glob

 open Std System
 open Lean (Name NameMap)
--- a/Lake/Config/Resolve.lean
+++ b/Lake/Config/Resolve.lean
@ -3,8 +3,8 @@ 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 Lake.Git
-import Lake.LeanConfig
+import Lake.Util.Git
+import Lake.Config.Load

 open System

--- a/Lake/Config/SearchPath.lean
+++ b/Lake/Config/SearchPath.lean
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean.Util.Path
-import Lake.InstallPath
+import Lake.Config.InstallPath

 open System
 namespace Lake
--- a/Lake/DSL.lean
+++ b/Lake/DSL.lean
@ -3,87 +3,5 @@ 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 Lake.Package
-import Lake.Attributes
-
-open Lean Parser Command
-namespace Lake.DSL
-
-syntax structVal :=
-  "{" manyIndent(group(Term.structInstField ", "?)) "}"
-
-syntax declValDo :=
-  ppSpace Term.do (Term.whereDecls)?
-
-syntax declValStruct :=
-  ppSpace structVal (Term.whereDecls)?
-
-- # Packages
-
-syntax packageDeclWithBinders :=
-  (ppSpace "(" Term.simpleBinder ")")? -- dir
-  (ppSpace "(" Term.simpleBinder ")")? -- args
-  (declValSimple <|> declValStruct <|> declValDo)
-
-syntax packageDeclTyped :=
-  Term.typeSpec declValSimple
-
-syntax packageDeclSpec :=
-  ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)?
-
-scoped syntax (name := packageDecl)
-(docComment)? "package " packageDeclSpec : command
-
-def expandPackageBinders
-: (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax)
-| none,     none      => do let hole ← `(_); (false, hole, hole)
-| some dir, none      => do (true, dir, ← `(_))
-| none,     some args => do (true, ← `(_), args)
-| some dir, some args => do (true, dir, args)
-
-def mkPackageDef (id : Syntax) (defn : Syntax) (doc? : Option Syntax)
-(dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do
-  let (hasBinders, dir, args) ← expandPackageBinders dir? args?
-  if hasBinders then
-    `($[$doc?:docComment]? @[«package»] def $id : Packager :=
-        (fun $dir $args => $defn) $[$wds?]?)
-  else
-    `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := $defn $[$wds?]?)
-
-@[macro packageDecl]
-def expandPackageDecl : Macro
-| `($[$doc?:docComment]? package $id:ident) =>
-  `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := {name := $(quote id.getId)})
-| `($[$doc?:docComment]? package $id:ident where $[$ds]*) =>
-  `($[$doc?:docComment]? @[«package»] def $id : PackageConfig where
-      name := $(quote id.getId) $[$ds]*)
-| `($[$doc?:docComment]? package $id:ident : $ty := $defn $[$wds?]?) =>
-  `($[$doc?:docComment]? @[«package»] def $id : $ty := $defn $[$wds?]?)
-| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
-  mkPackageDef id defn doc? dir? args? wds?
-| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
-  mkPackageDef id (← `({ name := $(quote id.getId), $[$fs]* })) doc? dir? args? wds?
-| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
-  let (_, dir, args) ← expandPackageBinders dir? args?
-  `($[$doc?:docComment]? @[«package»] def $id : IOPackager :=
-      (fun $dir $args => do $seq) $[$wds?]?)
-| stx => Macro.throwErrorAt stx "ill-formed package declaration"
-
-- # Scripts
-
-syntax scriptDeclSpec :=
-  ident (ppSpace "(" Term.simpleBinder ")")? (declValSimple <|> declValDo)
-
-scoped syntax (name := scriptDecl)
-(docComment)? "script " scriptDeclSpec : command
-
-@[macro scriptDecl]
-def expandScriptDecl : Macro
-| `($[$doc?:docComment]? script $id:ident $[($args?)]? do $seq $[$wds?]?) => do
-  let args := args?.getD (← `(_))
-  `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => do $seq $[$wds?]?)
-| `($[$doc?:docComment]? script $id:ident $[($args?)]? := $defn $[$wds?]?) => do
-  let args := args?.getD (← `(_))
-  `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
-| stx => Macro.throwErrorAt stx "ill-formed script declaration"
+import Lake.DSL.Attributes
+import Lake.DSL.Commands
--- a/Lake/DSL/Attributes.lean
+++ b/Lake/DSL/Attributes.lean
--- a/Lake/DSL/Commands.lean
+++ b/Lake/DSL/Commands.lean
@ -0,0 +1,89 @@
+/-
+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 Lake.Config.Package
+import Lake.DSL.Attributes
+
+open Lean Parser Command
+namespace Lake.DSL
+
+syntax structVal :=
+  "{" manyIndent(group(Term.structInstField ", "?)) "}"
+
+syntax declValDo :=
+  ppSpace Term.do (Term.whereDecls)?
+
+syntax declValStruct :=
+  ppSpace structVal (Term.whereDecls)?
+
+-- # Packages
+
+syntax packageDeclWithBinders :=
+  (ppSpace "(" Term.simpleBinder ")")? -- dir
+  (ppSpace "(" Term.simpleBinder ")")? -- args
+  (declValSimple <|> declValStruct <|> declValDo)
+
+syntax packageDeclTyped :=
+  Term.typeSpec declValSimple
+
+syntax packageDeclSpec :=
+  ident (Term.whereDecls <|> packageDeclTyped <|> packageDeclWithBinders)?
+
+scoped syntax (name := packageDecl)
+(docComment)? "package " packageDeclSpec : command
+
+def expandPackageBinders
+: (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax)
+| none,     none      => do let hole ← `(_); (false, hole, hole)
+| some dir, none      => do (true, dir, ← `(_))
+| none,     some args => do (true, ← `(_), args)
+| some dir, some args => do (true, dir, args)
+
+def mkPackageDef (id : Syntax) (defn : Syntax) (doc? : Option Syntax)
+(dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do
+  let (hasBinders, dir, args) ← expandPackageBinders dir? args?
+  if hasBinders then
+    `($[$doc?:docComment]? @[«package»] def $id : Packager :=
+        (fun $dir $args => $defn) $[$wds?]?)
+  else
+    `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := $defn $[$wds?]?)
+
+@[macro packageDecl]
+def expandPackageDecl : Macro
+| `($[$doc?:docComment]? package $id:ident) =>
+  `($[$doc?:docComment]? @[«package»] def $id : PackageConfig := {name := $(quote id.getId)})
+| `($[$doc?:docComment]? package $id:ident where $[$ds]*) =>
+  `($[$doc?:docComment]? @[«package»] def $id : PackageConfig where
+      name := $(quote id.getId) $[$ds]*)
+| `($[$doc?:docComment]? package $id:ident : $ty := $defn $[$wds?]?) =>
+  `($[$doc?:docComment]? @[«package»] def $id : $ty := $defn $[$wds?]?)
+| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
+  mkPackageDef id defn doc? dir? args? wds?
+| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
+  mkPackageDef id (← `({ name := $(quote id.getId), $[$fs]* })) doc? dir? args? wds?
+| `($[$doc?:docComment]? package $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
+  let (_, dir, args) ← expandPackageBinders dir? args?
+  `($[$doc?:docComment]? @[«package»] def $id : IOPackager :=
+      (fun $dir $args => do $seq) $[$wds?]?)
+| stx => Macro.throwErrorAt stx "ill-formed package declaration"
+
+-- # Scripts
+
+syntax scriptDeclSpec :=
+  ident (ppSpace "(" Term.simpleBinder ")")? (declValSimple <|> declValDo)
+
+scoped syntax (name := scriptDecl)
+(docComment)? "script " scriptDeclSpec : command
+
+@[macro scriptDecl]
+def expandScriptDecl : Macro
+| `($[$doc?:docComment]? script $id:ident $[($args?)]? do $seq $[$wds?]?) => do
+  let args := args?.getD (← `(_))
+  `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => do $seq $[$wds?]?)
+| `($[$doc?:docComment]? script $id:ident $[($args?)]? := $defn $[$wds?]?) => do
+  let args := args?.getD (← `(_))
+  `($[$doc?:docComment]? @[«script»] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
+| stx => Macro.throwErrorAt stx "ill-formed script declaration"
--- a/Lake/LeanVersion.lean
+++ b/Lake/LeanVersion.lean
@ -8,15 +8,15 @@ namespace Lake
 def leanVersionStringCore :=
  s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}"

-def origin := "leanprover/lean4"
+def leanOrigin := "leanprover/lean4"

 def leanVersionString :=
  if Lean.version.isRelease then
-    s!"{origin}:{leanVersionStringCore}"
+    s!"{leanOrigin}:{leanVersionStringCore}"
  else if Lean.version.specialDesc ≠ "" then
-    s!"{origin}:{Lean.version.specialDesc}"
+    s!"{leanOrigin}:{Lean.version.specialDesc}"
  else
-    s!"{origin}:master"
+    s!"{leanOrigin}:master"

 def uiLeanVersionString :=
 if Lean.version.isRelease then
--- a/Lake/Util/Async.lean
+++ b/Lake/Util/Async.lean
--- a/Lake/Util/CliT.lean
+++ b/Lake/Util/CliT.lean
--- a/Lake/Util/Git.lean
+++ b/Lake/Util/Git.lean
--- a/Lake/Util/LogT.lean
+++ b/Lake/Util/LogT.lean
--- a/Lake/Util/MainM.lean
+++ b/Lake/Util/MainM.lean
--- a/Lake/Util/Task.lean
+++ b/Lake/Util/Task.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 Lake.Async
+import Lake.Util.Async

 namespace Lake