refactor: move config loading code into its own directory

Lake/CLI/Init.lean

@@ -6,7 +6,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 import Lake.Util.Git
 import Lake.Config.Package
 import Lake.Config.Workspace
-import Lake.Config.Load
+import Lake.Load.Config
 
 namespace Lake
 open Git System

Lake/CLI/Main.lean

@@ -3,9 +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.Config.Load
-import Lake.Config.Manifest
-import Lake.Config.Resolve
+import Lake.Load
 import Lake.Util.Error
 import Lake.Util.MainM
 import Lake.Util.Cli
@@ -14,52 +12,13 @@ import Lake.CLI.Help
 import Lake.CLI.Build
 import Lake.CLI.Error
 
+-- # CLI
+
 open System
 open Lean (Json toJson fromJson?)
 
 namespace Lake
 
--- # Loading a Workspace
-
-structure LoadConfig where
-  env : Lake.Env
-  rootDir : FilePath
-  configFile : FilePath
-  options : NameMap String
-
-def loadPkg (config : LoadConfig) : LogIO Package := do
-  Lean.searchPathRef.set config.env.leanSearchPath
-  Package.load config.rootDir config.options config.configFile
-
-def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do
-  if let Except.ok contents ← IO.FS.readFile manifestFile  |>.toBaseIO then
-    match Json.parse contents with
-    | Except.ok json =>
-      match fromJson? json with
-      | Except.ok (manifest : Manifest) =>
-        return manifest.toMap
-      | Except.error e =>
-        logWarning s!"improperly formatted package manifest: {e}"
-        return {}
-    | Except.error e =>
-      logWarning s!"invalid JSON in package manifest: {e}"
-      return {}
-  else
-    return {}
-
-def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
-  let root ← loadPkg config
-  let ws : Workspace := {root, env := config.env}
-  let manifestMap ← loadManifestMap ws.manifestFile
-  let (packageMap, resolvedMap) ← resolveDeps ws root updateDeps |>.run manifestMap
-  unless resolvedMap.isEmpty do
-    let json := Json.pretty <| toJson <| Manifest.fromMap resolvedMap
-    IO.FS.writeFile ws.manifestFile <| json.push '\n'
-  let packageMap := packageMap.insert root.name root
-  return {ws with packageMap}
-
--- # CLI
-
 -- ## General options for top-level `lake`
 
 structure LakeOptions where

Lake/Load.lean

@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Load.Workspace

Lake/Load/Config.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Data.Name
+import Lake.Config.Env
+
+namespace Lake
+open System Lean
+
+/-- Context for loading a Lake configuration. -/
+structure LoadConfig where
+  env : Lake.Env
+  rootDir : FilePath
+  configFile : FilePath
+  options : NameMap String
+
+/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
+def defaultConfigFile : FilePath := "lakefile.lean"

Lake/Load/Materialize.lean

@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Git
-import Lake.Util.EStateT
-import Lake.Util.StoreInsts
-import Lake.Config.Load
-import Lake.Config.Manifest
-import Lake.Config.Workspace
-import Lake.Build.Topological
+import Lake.Load.Manifest
+import Lake.Config.Dependency
 
-open Std System
+open Std System Lean
 
 namespace Lake
 
+abbrev ResolveM := StateT (NameMap PackageEntry) <| LogIO
+
 /-- Update the Git package in `repo` to `rev` if not already at it. -/
 def updateGitPkg (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
   let rev ← repo.findRemoteRevision rev?
@@ -30,8 +28,6 @@ def cloneGitPkg (repo : GitRepo) (url : String) (rev? : Option String) : LogIO P
     let hash ← repo.parseRemoteRevision rev
     repo.checkoutDetach hash
 
-abbrev ResolveM := StateT (NameMap PackageEntry) <| LogIO
-
 /--
 Materializes a Git package in `dir`, cloning and/or updating it as necessary.
 
@@ -85,47 +81,16 @@ def materializeGitPkg (name : String) (dir : FilePath)
     modify (·.insert name {name, url, rev})
 
 /--
-Materializes a `Dependency` relative to the given `Package`,
-downloading and/or updating it as necessary.
+Materializes a `Dependency`, downloading nd/or updating it as necessary.
+Local dependencies are materialized relative to `localRoot` and remote
+dependencies are stored in `packagesDir`.
 -/
-def materializeDep (ws : Workspace)
-(pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM FilePath :=
+def materializeDep (packagesDir localRoot : FilePath)
+(dep : Dependency) (shouldUpdate := true) : ResolveM FilePath :=
   match dep.src with
-  | Source.path dir => return pkg.dir / dir
+  | Source.path dir => return localRoot / dir
   | Source.git url rev? subDir? => do
     let name := dep.name.toString (escape := false)
-    let gitDir := ws.packagesDir / name
+    let gitDir := packagesDir / name
     materializeGitPkg name gitDir url rev? shouldUpdate
     return match subDir? with | some subDir => gitDir / subDir | none => gitDir
-
-/--
-Resolves a `Dependency` relative to the given `Package`
-in the same `Workspace`, downloading and/or updating it as necessary.
--/
-def resolveDep (ws : Workspace)
-(pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM Package := do
-  let dir ← materializeDep ws pkg dep shouldUpdate
-  let depPkg ← Package.load dir dep.options
-  unless depPkg.name == dep.name do
-    throw <| IO.userError <|
-      s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
-      s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"
-  return depPkg
-
-/--
-Resolves the package's dependencies,
-downloading and/or updating them as necessary.
--/
-def resolveDeps (ws : Workspace) (pkg : Package)
-(shouldUpdate := true) : ResolveM (NameMap Package) := do
-  let resolve dep resolve := do
-    let pkg ← resolveDep ws pkg dep shouldUpdate
-    pkg.dependencies.forM fun dep => discard <| resolve dep
-    return pkg
-  let (res, map) ← EStateT.run (mkRBMap _ _ Lean.Name.quickCmp) <|
-    pkg.dependencies.forM fun dep => discard <| buildTop Dependency.name resolve dep
-  match res with
-  | Except.ok _ => return map
-  | Except.error cycle => do
-    let cycle := cycle.map (s!"  {·}")
-    error s!"dependency cycle detected:\n{"\n".intercalate cycle}"

Lake/Load/Package.lean

@@ -8,6 +8,7 @@ import Lake.DSL.Attributes
 import Lake.DSL.Extensions
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
+import Lake.Load.Config
 
 namespace Lake
 open Lean System
@@ -15,9 +16,6 @@ open Lean System
 /-- Main module `Name` of a Lake configuration file. -/
 def configModuleName : Name := `lakefile
 
-/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
-def defaultConfigFile : FilePath := "lakefile.lean"
-
 deriving instance BEq, Hashable for Import
 
 /- Cache for the imported header environment of Lake configuration files. -/

Lake/Load/Resolve.lean

@@ -0,0 +1,47 @@
+/-
+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.Util.EStateT
+import Lake.Util.StoreInsts
+import Lake.Load.Package
+import Lake.Load.Materialize
+import Lake.Config.Workspace
+import Lake.Build.Topological
+
+open Std System
+
+namespace Lake
+
+/--
+Resolves a `Dependency` relative to the given `Package`
+in the same `Workspace`, downloading and/or updating it as necessary.
+-/
+def resolveDep (ws : Workspace)
+(pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM Package := do
+  let dir ← materializeDep ws.packagesDir pkg.dir dep shouldUpdate
+  let depPkg ← Package.load dir dep.options
+  unless depPkg.name == dep.name do
+    throw <| IO.userError <|
+      s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
+      s!"but resolved dependency has name {depPkg.name} (in {depPkg.dir})"
+  return depPkg
+
+/--
+Resolves the package's dependencies,
+downloading and/or updating them as necessary.
+-/
+def resolveDeps (ws : Workspace) (pkg : Package)
+(shouldUpdate := true) : ResolveM (NameMap Package) := do
+  let resolve dep resolve := do
+    let pkg ← resolveDep ws pkg dep shouldUpdate
+    pkg.dependencies.forM fun dep => discard <| resolve dep
+    return pkg
+  let (res, map) ← EStateT.run (mkRBMap _ _ Lean.Name.quickCmp) <|
+    pkg.dependencies.forM fun dep => discard <| buildTop Dependency.name resolve dep
+  match res with
+  | Except.ok _ => return map
+  | Except.error cycle => do
+    let cycle := cycle.map (s!"  {·}")
+    error s!"dependency cycle detected:\n{"\n".intercalate cycle}"

Lake/Load/Workspace.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Load.Resolve
+
+open System
+open Lean (Json toJson fromJson?)
+
+namespace Lake
+
+def loadPkg (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.env.leanSearchPath
+  Package.load config.rootDir config.options config.configFile
+
+def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do
+  if let Except.ok contents ← IO.FS.readFile manifestFile  |>.toBaseIO then
+    match Json.parse contents with
+    | Except.ok json =>
+      match fromJson? json with
+      | Except.ok (manifest : Manifest) =>
+        return manifest.toMap
+      | Except.error e =>
+        logWarning s!"improperly formatted package manifest: {e}"
+        return {}
+    | Except.error e =>
+      logWarning s!"invalid JSON in package manifest: {e}"
+      return {}
+  else
+    return {}
+
+def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
+  let root ← loadPkg config
+  let ws : Workspace := {root, env := config.env}
+  let manifestMap ← loadManifestMap ws.manifestFile
+  let (packageMap, resolvedMap) ← resolveDeps ws root updateDeps |>.run manifestMap
+  unless resolvedMap.isEmpty do
+    let json := Json.pretty <| toJson <| Manifest.fromMap resolvedMap
+    IO.FS.writeFile ws.manifestFile <| json.push '\n'
+  let packageMap := packageMap.insert root.name root
+  return {ws with packageMap}