From 331bf0f7f2bf5d934bbdaa7695c5e471348d7259 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 9 Nov 2021 22:30:18 -0500
Subject: [PATCH] refactor: reorganize code folder structure

---
 Lake.lean                                     | 28 +-----
 Lake/Build.lean                               | 12 +++
 Lake/{Compile.lean => Build/Actions.lean}     |  2 +-
 Lake/{BuildBin.lean => Build/Binary.lean}     |  4 +-
 Lake/{BuildModule.lean => Build/Module.lean}  | 14 +--
 Lake/{BuildMonad.lean => Build/Monad.lean}    |  8 +-
 .../{BuildPackage.lean => Build/Package.lean} |  7 +-
 Lake/{BuildTop.lean => Build/Recursive.lean}  |  0
 Lake/{ => Build}/Target.lean                  |  4 +-
 .../TargetTypes.lean}                         |  4 +-
 .../{BuildTargets.lean => Build/Targets.lean} |  4 +-
 Lake/{ => Build}/Trace.lean                   |  0
 Lake/CLI.lean                                 |  8 ++
 Lake/{ => CLI}/Help.lean                      |  0
 Lake/{ => CLI}/Init.lean                      |  6 +-
 Lake/{Cli.lean => CLI/Main.lean}              | 16 ++--
 Lake/Config.lean                              | 11 +++
 Lake/{ => Config}/Glob.lean                   |  0
 Lake/{ => Config}/InstallPath.lean            |  0
 Lake/{LeanConfig.lean => Config/Load.lean}    |  4 +-
 Lake/{ => Config}/Package.lean                |  5 +-
 Lake/{ => Config}/Resolve.lean                |  4 +-
 Lake/{ => Config}/SearchPath.lean             |  2 +-
 Lake/DSL.lean                                 | 86 +-----------------
 Lake/{ => DSL}/Attributes.lean                |  0
 Lake/DSL/Commands.lean                        | 89 +++++++++++++++++++
 Lake/LeanVersion.lean                         |  8 +-
 Lake/{ => Util}/Async.lean                    |  0
 Lake/{ => Util}/CliT.lean                     |  0
 Lake/{ => Util}/Git.lean                      |  0
 Lake/{LogMonad.lean => Util/LogT.lean}        |  0
 Lake/{ => Util}/MainM.lean                    |  0
 Lake/{ => Util}/Task.lean                     |  2 +-
 33 files changed, 171 insertions(+), 157 deletions(-)
 create mode 100644 Lake/Build.lean
 rename Lake/{Compile.lean => Build/Actions.lean} (99%)
 rename Lake/{BuildBin.lean => Build/Binary.lean} (98%)
 rename Lake/{BuildModule.lean => Build/Module.lean} (97%)
 rename Lake/{BuildMonad.lean => Build/Monad.lean} (96%)
 rename Lake/{BuildPackage.lean => Build/Package.lean} (99%)
 rename Lake/{BuildTop.lean => Build/Recursive.lean} (100%)
 rename Lake/{ => Build}/Target.lean (99%)
 rename Lake/{BuildTarget.lean => Build/TargetTypes.lean} (96%)
 rename Lake/{BuildTargets.lean => Build/Targets.lean} (98%)
 rename Lake/{ => Build}/Trace.lean (100%)
 create mode 100644 Lake/CLI.lean
 rename Lake/{ => CLI}/Help.lean (100%)
 rename Lake/{ => CLI}/Init.lean (97%)
 rename Lake/{Cli.lean => CLI/Main.lean} (98%)
 create mode 100644 Lake/Config.lean
 rename Lake/{ => Config}/Glob.lean (100%)
 rename Lake/{ => Config}/InstallPath.lean (100%)
 rename Lake/{LeanConfig.lean => Config/Load.lean} (98%)
 rename Lake/{ => Config}/Package.lean (99%)
 rename Lake/{ => Config}/Resolve.lean (97%)
 rename Lake/{ => Config}/SearchPath.lean (98%)
 rename Lake/{ => DSL}/Attributes.lean (100%)
 create mode 100644 Lake/DSL/Commands.lean
 rename Lake/{ => Util}/Async.lean (100%)
 rename Lake/{ => Util}/CliT.lean (100%)
 rename Lake/{ => Util}/Git.lean (100%)
 rename Lake/{LogMonad.lean => Util/LogT.lean} (100%)
 rename Lake/{ => Util}/MainM.lean (100%)
 rename Lake/{ => Util}/Task.lean (98%)

diff --git a/Lake.lean b/Lake.lean
index 828fe72986..6e7bcf82a1 100644
--- 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
diff --git a/Lake/Build.lean b/Lake/Build.lean
new file mode 100644
index 0000000000..48d1962077
--- /dev/null
+++ 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
diff --git a/Lake/Compile.lean b/Lake/Build/Actions.lean
similarity index 99%
rename from Lake/Compile.lean
rename to Lake/Build/Actions.lean
index 6876808a2f..b4c6e8125d 100644
--- a/Lake/Compile.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
diff --git a/Lake/BuildBin.lean b/Lake/Build/Binary.lean
similarity index 98%
rename from Lake/BuildBin.lean
rename to Lake/Build/Binary.lean
index ea7340792b..5c7a9a4515 100644
--- a/Lake/BuildBin.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)
diff --git a/Lake/BuildModule.lean b/Lake/Build/Module.lean
similarity index 97%
rename from Lake/BuildModule.lean
rename to Lake/Build/Module.lean
index 1889755d9c..4e4129477c 100644
--- a/Lake/BuildModule.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
diff --git a/Lake/BuildMonad.lean b/Lake/Build/Monad.lean
similarity index 96%
rename from Lake/BuildMonad.lean
rename to Lake/Build/Monad.lean
index bc8c0cd9af..f916955fa9 100644
--- a/Lake/BuildMonad.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
diff --git a/Lake/BuildPackage.lean b/Lake/Build/Package.lean
similarity index 99%
rename from Lake/BuildPackage.lean
rename to Lake/Build/Package.lean
index f3230f5cae..a9f5811cb7 100644
--- a/Lake/BuildPackage.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
diff --git a/Lake/BuildTop.lean b/Lake/Build/Recursive.lean
similarity index 100%
rename from Lake/BuildTop.lean
rename to Lake/Build/Recursive.lean
diff --git a/Lake/Target.lean b/Lake/Build/Target.lean
similarity index 99%
rename from Lake/Target.lean
rename to Lake/Build/Target.lean
index 3bc2ee6a79..b625666c1e 100644
--- a/Lake/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
diff --git a/Lake/BuildTarget.lean b/Lake/Build/TargetTypes.lean
similarity index 96%
rename from Lake/BuildTarget.lean
rename to Lake/Build/TargetTypes.lean
index c99157282f..e81696fec8 100644
--- a/Lake/BuildTarget.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
diff --git a/Lake/BuildTargets.lean b/Lake/Build/Targets.lean
similarity index 98%
rename from Lake/BuildTargets.lean
rename to Lake/Build/Targets.lean
index 572c566d02..d4607b7309 100644
--- a/Lake/BuildTargets.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
diff --git a/Lake/Trace.lean b/Lake/Build/Trace.lean
similarity index 100%
rename from Lake/Trace.lean
rename to Lake/Build/Trace.lean
diff --git a/Lake/CLI.lean b/Lake/CLI.lean
new file mode 100644
index 0000000000..0e3354fa6a
--- /dev/null
+++ 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
diff --git a/Lake/Help.lean b/Lake/CLI/Help.lean
similarity index 100%
rename from Lake/Help.lean
rename to Lake/CLI/Help.lean
diff --git a/Lake/Init.lean b/Lake/CLI/Init.lean
similarity index 97%
rename from Lake/Init.lean
rename to Lake/CLI/Init.lean
index 759c842bfc..95c0d6efd5 100644
--- a/Lake/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
diff --git a/Lake/Cli.lean b/Lake/CLI/Main.lean
similarity index 98%
rename from Lake/Cli.lean
rename to Lake/CLI/Main.lean
index b457b4be81..b514334141 100644
--- a/Lake/Cli.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)
diff --git a/Lake/Config.lean b/Lake/Config.lean
new file mode 100644
index 0000000000..e7c5fd3d81
--- /dev/null
+++ 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
diff --git a/Lake/Glob.lean b/Lake/Config/Glob.lean
similarity index 100%
rename from Lake/Glob.lean
rename to Lake/Config/Glob.lean
diff --git a/Lake/InstallPath.lean b/Lake/Config/InstallPath.lean
similarity index 100%
rename from Lake/InstallPath.lean
rename to Lake/Config/InstallPath.lean
diff --git a/Lake/LeanConfig.lean b/Lake/Config/Load.lean
similarity index 98%
rename from Lake/LeanConfig.lean
rename to Lake/Config/Load.lean
index dae2e49821..c6576b9c4f 100644
--- a/Lake/LeanConfig.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
diff --git a/Lake/Package.lean b/Lake/Config/Package.lean
similarity index 99%
rename from Lake/Package.lean
rename to Lake/Config/Package.lean
index bc0232e9be..a7746fe7f0 100644
--- a/Lake/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)
diff --git a/Lake/Resolve.lean b/Lake/Config/Resolve.lean
similarity index 97%
rename from Lake/Resolve.lean
rename to Lake/Config/Resolve.lean
index e46bc54ae2..ebb6281029 100644
--- a/Lake/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
 
diff --git a/Lake/SearchPath.lean b/Lake/Config/SearchPath.lean
similarity index 98%
rename from Lake/SearchPath.lean
rename to Lake/Config/SearchPath.lean
index 93e1a7b806..dbbed5e3b7 100644
--- a/Lake/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
diff --git a/Lake/DSL.lean b/Lake/DSL.lean
index a423065aba..9c94f2d842 100644
--- 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
diff --git a/Lake/Attributes.lean b/Lake/DSL/Attributes.lean
similarity index 100%
rename from Lake/Attributes.lean
rename to Lake/DSL/Attributes.lean
diff --git a/Lake/DSL/Commands.lean b/Lake/DSL/Commands.lean
new file mode 100644
index 0000000000..49b0485b3c
--- /dev/null
+++ 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"
diff --git a/Lake/LeanVersion.lean b/Lake/LeanVersion.lean
index 99c8b7f62d..ba26ace91f 100644
--- 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
diff --git a/Lake/Async.lean b/Lake/Util/Async.lean
similarity index 100%
rename from Lake/Async.lean
rename to Lake/Util/Async.lean
diff --git a/Lake/CliT.lean b/Lake/Util/CliT.lean
similarity index 100%
rename from Lake/CliT.lean
rename to Lake/Util/CliT.lean
diff --git a/Lake/Git.lean b/Lake/Util/Git.lean
similarity index 100%
rename from Lake/Git.lean
rename to Lake/Util/Git.lean
diff --git a/Lake/LogMonad.lean b/Lake/Util/LogT.lean
similarity index 100%
rename from Lake/LogMonad.lean
rename to Lake/Util/LogT.lean
diff --git a/Lake/MainM.lean b/Lake/Util/MainM.lean
similarity index 100%
rename from Lake/MainM.lean
rename to Lake/Util/MainM.lean
diff --git a/Lake/Task.lean b/Lake/Util/Task.lean
similarity index 98%
rename from Lake/Task.lean
rename to Lake/Util/Task.lean
index f82fdad312..5eebe134ed 100644
--- a/Lake/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