diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 1322ec6..dc85536 100644
--- a/Lake/Build/Index.lean
+++ b/Lake/Build/Index.lean
@@ -114,23 +114,21 @@ the initial set of Lake package facets (e.g., `extraDep`).
   |>.insert `deps (mkPackageFacetBuild <| fun pkg => do
     let mut deps := #[]
     let mut depSet := PackageSet.empty
-    for dep in pkg.dependencies do
-      if let some depPkg ← findPackage? dep.name then
-        for depDepPkg in (← recBuild <| depPkg.facet `deps) do
-          unless depSet.contains depDepPkg do
-            deps := deps.push depDepPkg
-            depSet := depSet.insert depDepPkg
-        unless depSet.contains depPkg do
-          deps := deps.push depPkg
-          depSet := depSet.insert depPkg
+    for dep in pkg.deps do
+      for depDep in (← recBuild <| dep.facet `deps) do
+        unless depSet.contains depDep do
+          deps := deps.push depDep
+          depSet := depSet.insert depDep
+      unless depSet.contains dep do
+        deps := deps.push dep
+        depSet := depSet.insert dep
     return deps
   )
   -- Build the `extraDepTarget` for the package and its transitive dependencies
   |>.insert `extraDep (mkPackageFacetBuild <| fun pkg => do
     let mut target := ActiveTarget.nil
-    for dep in pkg.dependencies do
-      if let some depPkg ← findPackage? dep.name then
-        target ← target.mixOpaqueAsync (← depPkg.extraDep.recBuild)
+    for dep in pkg.deps do
+      target ← target.mixOpaqueAsync (← dep.extraDep.recBuild)
     target.mixOpaqueAsync <| ← pkg.extraDepTarget.activate
   )
 
diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean
index a9e767a..d31b119 100644
--- a/Lake/Build/Monad.lean
+++ b/Lake/Build/Monad.lean
@@ -13,7 +13,7 @@ namespace Lake
 deriving instance Inhabited for BuildContext
 
 def mkBuildContext (ws : Workspace) : IO BuildContext := do
-  let lean := ws.env.lean
+  let lean := ws.lakeEnv.lean
   let leanTrace :=
     if lean.githash.isEmpty then
       mixTrace (← computeTrace lean.lean) (← computeTrace lean.sharedLib)
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index b3405c8..c317e72 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -26,7 +26,7 @@ structure LakeOptions where
   configFile : FilePath := defaultConfigFile
   leanInstall? : Option LeanInstall := none
   lakeInstall? : Option LakeInstall := none
-  configOptions : NameMap String := {}
+  configOpts : NameMap String := {}
   subArgs : List String := []
   wantsHelp : Bool := false
 
@@ -51,12 +51,15 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
   Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall)
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
-def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
+def LakeOptions.mkLoadConfig
+(opts : LakeOptions) (updateDeps := false) : EIO CliError LoadConfig :=
   return {
-    rootDir := opts.rootDir,
-    configFile := opts.rootDir / opts.configFile,
     env := ← opts.computeEnv
-    options := opts.configOptions
+    rootDir := opts.rootDir
+    configFile := opts.rootDir / opts.configFile
+    configOpts := opts.configOpts
+    leanOpts := Lean.Options.empty
+    updateDeps
   }
 
 export LakeOptions (mkLoadConfig)
@@ -103,7 +106,7 @@ def setLean (lean : String) : CliStateM PUnit := do
   let leanInstall? ← findLeanCmdInstall? lean
   modify ({·  with leanInstall?})
 
-def setConfigOption (kvPair : String) : CliM PUnit :=
+def setConfigOpt (kvPair : String) : CliM PUnit :=
   let pos := kvPair.posOf '='
   let (key, val) :=
     if pos = kvPair.endPos then
@@ -111,13 +114,13 @@ def setConfigOption (kvPair : String) : CliM PUnit :=
     else
       (kvPair.extract 0 pos |>.toName, kvPair.extract (kvPair.next pos) kvPair.endPos)
   modifyThe LakeOptions fun opts =>
-    {opts with configOptions := opts.configOptions.insert key val}
+    {opts with configOpts := opts.configOpts.insert key val}
 
 def lakeShortOption : (opt : Char) → CliM PUnit
 | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
 | 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
 | 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
-| 'K' => do setConfigOption <| ← takeOptArg "-K" "key-value pair"
+| 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
 | opt => throw <| CliError.unknownShortOption opt
 
 def lakeLongOption : (opt : String) → CliM PUnit
@@ -308,8 +311,8 @@ protected def build : CliM PUnit := do
 
 protected def update : CliM PUnit := do
   processOptions lakeOption
-  let config ← mkLoadConfig (← getThe LakeOptions)
-  noArgsRem <| discard <| loadWorkspace config (updateDeps := true)
+  let config ← mkLoadConfig (← getThe LakeOptions) (updateDeps := true)
+  noArgsRem <| discard <| loadWorkspace config
 
 protected def printPaths : CliM PUnit := do
   processOptions lakeOption
diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean
index 57759d4..f91544c 100644
--- a/Lake/Config/Monad.lean
+++ b/Lake/Config/Monad.lean
@@ -36,7 +36,7 @@ section
 variable [MonadWorkspace m] [Functor m]
 
 instance : MonadLakeEnv m where
-  read := (·.env) <$> read
+  read := (·.lakeEnv) <$> read
 
 /- ## Workspace Helpers -/
 
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index ac196db..b4d8250 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -12,7 +12,7 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 import Lake.Util.DRBMap
 
-open Std System
+open Std System Lean
 
 namespace Lake
 
@@ -246,12 +246,12 @@ structure Package where
   dir : FilePath
   /-- The package's user-defined configuration. -/
   config : PackageConfig
-  /-- The package's well-formed name. -/
-  name : Name := config.name
-  /-- Scripts for the package. -/
-  scripts : NameMap Script := {}
-  /- An `Array` of the package's dependencies. -/
-  dependencies : Array Dependency := #[]
+  /-- The elaboration environment of the package's configuration file. -/
+  configEnv : Environment
+  /-- The Lean `Options` the package configuration was elaborated with. -/
+  leanOpts : Options
+  /- (Opaque references to) the package's direct dependencies. -/
+  opaqueDeps : Array OpaquePackage := #[]
   /-- Lean library configurations for the package. -/
   leanLibConfigs : NameMap LeanLibConfig := {}
   /-- Lean binary executable configurations for the package. -/
@@ -269,15 +269,25 @@ structure Package where
   (i.e., on a bare `lake build` of the package).
   -/
   defaultTargets : Array Name := #[]
+  /-- Scripts for the package. -/
+  scripts : NameMap Script := {}
   deriving Inhabited
 
 hydrate_opaque_type OpaquePackage Package
 
-abbrev PackageSet := RBTree Package (·.name.quickCmp ·.name)
+abbrev PackageSet := RBTree Package (·.config.name.quickCmp ·.config.name)
 @[inline] def PackageSet.empty : PackageSet := RBTree.empty
 
 namespace Package
 
+/-- The package's name. -/
+@[inline] def name (self : Package) : Name :=
+  self.config.name
+
+  /- An `Array` of the package's direct dependencies. -/
+@[inline] def deps (self : Package) : Array Package  :=
+  self.opaqueDeps.map (·.get)
+
 /-- The package's `extraDepTarget` configuration. -/
 @[inline] def extraDepTarget (self : Package) : OpaqueTarget :=
   self.config.extraDepTarget.getD Target.nil
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index d57215e..33af807 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -21,7 +21,7 @@ structure Workspace where
   /-- The root package of the workspace. -/
   root : Package
   /-- The detect `Lake.Env` of the workspace. -/
-  env : Lake.Env
+  lakeEnv : Lake.Env
   /-- Name-package map of packages within the workspace. -/
   packageMap : NameMap Package := {}
   deriving Inhabited
@@ -127,7 +127,7 @@ used to build is available to the environment (and thus, e.g., the Lean server).
 Otherwise, it may fall back on whatever the default Lake instance is.
 -/
 def augmentedLeanPath (self : Workspace) : SearchPath :=
-  self.env.leanPath ++ self.leanPath ++ [self.env.lake.libDir]
+  self.lakeEnv.leanPath ++ self.leanPath ++ [self.lakeEnv.lake.libDir]
 
 /--
 The detected `LEAN_SRC_PATH` of the environment
@@ -138,21 +138,21 @@ used to build is available to the environment (and thus, e.g., the Lean server).
 Otherwise, it may fall back on whatever the default Lake instance is.
 -/
 def augmentedLeanSrcPath (self : Workspace) : SearchPath :=
-  self.env.leanSrcPath ++ self.leanSrcPath ++ [self.env.lake.srcDir]
+  self.lakeEnv.leanSrcPath ++ self.leanSrcPath ++ [self.lakeEnv.lake.srcDir]
 
 /-
 The detected `sharedLibPathEnv` value of the environment
 augmented with the workspace's `libPath`.
 -/
 def augmentedSharedLibPath (self : Workspace) : SearchPath :=
-  self.env.sharedLibPath ++ self.libPath
+  self.lakeEnv.sharedLibPath ++ self.libPath
 
 /--
 The detected environment augmented with the Workspace's paths.
 These are the settings use by `lake env` / `Lake.env` to run executables.
 -/
 def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
-  self.env.installVars ++ #[
+  self.lakeEnv.installVars ++ #[
     ("LEAN_PATH", some self.augmentedLeanPath.toString),
     ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
     (sharedLibPathEnvVar, some self.augmentedSharedLibPath.toString)
diff --git a/Lake/Load.lean b/Lake/Load.lean
index 9b71d35..11a8de7 100644
--- a/Lake/Load.lean
+++ b/Lake/Load.lean
@@ -3,4 +3,4 @@ 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
+import Lake.Load.Main
diff --git a/Lake/Load/Config.lean b/Lake/Load/Config.lean
index bfba655..ec59d26 100644
--- a/Lake/Load/Config.lean
+++ b/Lake/Load/Config.lean
@@ -4,17 +4,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lean.Data.Name
+import Lean.Data.Options
 import Lake.Config.Env
 
 namespace Lake
 open System Lean
 
+/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
+def defaultConfigFile : FilePath := "lakefile.lean"
+
 /-- Context for loading a Lake configuration. -/
 structure LoadConfig where
+  /-- The Lake environment of the load process. -/
   env : Lake.Env
+  /-- The root directory of the loaded package (and its workspace). -/
   rootDir : FilePath
-  configFile : FilePath
-  options : NameMap String
-
-/-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
-def defaultConfigFile : FilePath := "lakefile.lean"
+  /-- The Lean file with the package's Lake configuration (e.g., `lakefile.lean`) -/
+  configFile : FilePath := rootDir / defaultConfigFile
+  /-- A set of key-value Lake configuration options (i.e., `-K` settings). -/
+  configOpts : NameMap String := {}
+  /-- The Lean options with which to elaborate the configuration file. -/
+  leanOpts : Options := {}
+  /--
+  Whether to update dependencies during resolution
+  or fallback to the ones listed in the manifest.
+  -/
+  updateDeps : Bool := false
diff --git a/Lake/Load/Elab.lean b/Lake/Load/Elab.lean
index 5bc440a..615a049 100644
--- a/Lake/Load/Elab.lean
+++ b/Lake/Load/Elab.lean
@@ -36,7 +36,7 @@ def configModuleName : Name := `lakefile
 
 /-- Elaborate `configFile` with the given package directory and options. -/
 def elabConfigFile (pkgDir : FilePath) (configOpts : NameMap String)
-(configFile := pkgDir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Environment := do
+(leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) : LogIO Environment := do
 
   -- Read file and initialize environment
   let input ← IO.FS.readFile configFile
diff --git a/Lake/Load/Main.lean b/Lake/Load/Main.lean
new file mode 100644
index 0000000..3604936
--- /dev/null
+++ b/Lake/Load/Main.lean
@@ -0,0 +1,75 @@
+/-
+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.Util.EStateT
+import Lake.Util.StoreInsts
+import Lake.Load.Package
+import Lake.Load.Materialize
+import Lake.Config.Workspace
+import Lake.Build.Topological
+
+open System Lean
+
+namespace Lake
+
+/--
+Elaborate a package configuration file and
+construct a bare `Package` from its `PackageConfig` file.
+-/
+def loadPkg (dir : FilePath) (configOpts : NameMap String)
+(leanOpts := Options.empty) (configFile := dir / defaultConfigFile) : LogIO Package := do
+  let configEnv ← elabConfigFile dir configOpts leanOpts configFile
+  let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
+  return {dir, config, configEnv, leanOpts}
+
+/-- Load the tagged `Dependency` definitions from a package configuration environment. -/
+def loadDeps (env : Environment) (opts : Options) : Except String (Array Dependency) := do
+  packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
+    return arr.push <| ← evalConstCheck env opts Dependency ``Dependency name
+
+/--
+Resolves the package's dependencies,
+downloading and/or updating them as necessary.
+-/
+def resolveDeps (ws : Workspace) (pkg : Package) (leanOpts : Options)
+(deps : Array Dependency) (shouldUpdate := true) : ManifestM (Array Package × NameMap Package) := do
+  let (res, map) ← EStateT.run (Std.mkRBMap _ _ Name.quickCmp) <| deps.mapM fun dep =>
+    buildTop (·.2.name) recResolveDep (pkg, dep)
+  match res with
+  | Except.ok deps => return (deps, map)
+  | Except.error cycle => do
+    let cycle := cycle.map (s!"  {·}")
+    error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
+where
+  recResolveDep info resolve := do
+    let ⟨pkg, dep⟩ := info
+    let dir ← materializeDep ws.packagesDir pkg.dir dep shouldUpdate
+    let depPkg ← loadPkg dir dep.options leanOpts
+    unless depPkg.name = dep.name do
+      error <|
+        s!"{pkg.name} (in {pkg.dir}) depends on {dep.name}, " ++
+        s!"but resolved dependency has name {depPkg.name} (in {dir})"
+    let depDeps ← IO.ofExcept <| loadDeps depPkg.configEnv leanOpts
+    let depDepPkgs ← depDeps.mapM fun dep => resolve (depPkg, dep)
+    let depPkg ← depPkg.finalize depDepPkgs
+    return depPkg
+
+/--
+Load a `Workspace` for a Lake package by
+elaborating its configuration file and resolve its dependencies.
+-/
+def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
+  Lean.searchPathRef.set config.env.leanSearchPath
+  let root ← loadPkg config.rootDir config.configOpts config.leanOpts config.configFile
+  let ws : Workspace := {root, lakeEnv := config.env}
+  let deps ← IO.ofExcept <| loadDeps root.configEnv config.leanOpts
+  let manifest ← Manifest.loadFromFile ws.manifestFile |>.catchExceptions fun _ => pure {}
+  let ((deps, packageMap), manifest) ← resolveDeps ws root
+    config.leanOpts deps config.updateDeps |>.run manifest
+  unless manifest.isEmpty do
+    manifest.saveToFile ws.manifestFile
+  let root ← root.finalize deps
+  let packageMap := packageMap.insert root.name root
+  return {ws with root, packageMap}
diff --git a/Lake/Load/Package.lean b/Lake/Load/Package.lean
index 1900807..33d06a1 100644
--- a/Lake/Load/Package.lean
+++ b/Lake/Load/Package.lean
@@ -11,8 +11,8 @@ import Lake.Load.Elab
 namespace Lake
 open Lean System
 
-/-- Like `Lean.Environment.evalConstCheck` but with plain universe-polymorphic `Except`. -/
-unsafe def evalConstCheck (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α :=
+/-- Unsafe implementation of `evalConstCheck`. -/
+unsafe def unsafeEvalConstCheck (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α :=
   match env.find? const with
   | none => throw s!"unknown constant '{const}'"
   | some info =>
@@ -27,6 +27,10 @@ where
   throwUnexpectedType : Except String α :=
     throw s!"unexpected type at '{const}', `{type}` expected"
 
+/-- Like `Lean.Environment.evalConstCheck`, but with plain universe-polymorphic `Except`. -/
+@[implementedBy unsafeEvalConstCheck] opaque evalConstCheck
+(env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α
+
 /-- Construct a `NameMap` from the declarations tagged with `attr`. -/
 def mkTagMap
 (env : Environment) (attr : TagAttribute)
@@ -41,82 +45,67 @@ def mkDTagMap
   attr.ext.getState env |>.foldM (init := {}) fun map declName =>
     return map.insert declName <| ← f declName
 
-/-- Unsafe implementation of `loadFromEnv`. -/
-unsafe def Package.unsafeLoadFromEnv
-(env : Environment) (leanOpts := Options.empty) : LogIO Package := do
-
-  -- Load Configuration
-  let pkgDeclName ←
+/-- Load a `PackageConfig` from a configuration environment. -/
+def PackageConfig.loadFromEnv
+(env : Environment) (opts := Options.empty) : Except String PackageConfig := do
+  let declName ←
     match packageAttr.ext.getState env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
     | [name] => pure name
     | _ => error s!"configuration file has multiple `package` declarations"
-  let config ← IO.ofExcept <|
-    evalConstCheck env leanOpts PackageConfig  ``PackageConfig pkgDeclName
+  evalConstCheck env opts _  ``PackageConfig declName
 
-  -- Load Dependencies
-  let dependencies ← IO.ofExcept <|
-    packageDepAttr.ext.getState env |>.foldM (init := #[]) fun arr name => do
-      return arr.push <| ← evalConstCheck env leanOpts Dependency ``Dependency name
+/--
+Load the remainder of a `Package`
+from its configuration environment after resolving its dependencies.
+-/
+def Package.finalize (self : Package) (deps : Array Package) : LogIO Package := do
+  let env := self.configEnv; let opts := self.leanOpts
 
   -- Load Script, Facet, & Target Configurations
   let scripts ← mkTagMap env scriptAttr fun name => do
-    let fn ← IO.ofExcept <| evalConstCheck env leanOpts ScriptFn ``ScriptFn name
+    let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn name
     return {fn, doc? := (← findDocString? env name)}
   let leanLibConfigs ← IO.ofExcept <| mkTagMap env leanLibAttr fun name =>
-    evalConstCheck env leanOpts LeanLibConfig ``LeanLibConfig name
+    evalConstCheck env opts LeanLibConfig ``LeanLibConfig name
   let leanExeConfigs ← IO.ofExcept <| mkTagMap env leanExeAttr fun name =>
-    evalConstCheck env leanOpts LeanExeConfig ``LeanExeConfig name
+    evalConstCheck env opts LeanExeConfig ``LeanExeConfig name
   let externLibConfigs ← IO.ofExcept <| mkTagMap env externLibAttr fun name =>
-    evalConstCheck env leanOpts ExternLibConfig ``ExternLibConfig name
+    evalConstCheck env opts ExternLibConfig ``ExternLibConfig name
   let opaqueModuleFacetConfigs ← mkDTagMap env moduleFacetAttr fun name => do
-    match evalConstCheck env leanOpts  ModuleFacetDecl ``ModuleFacetDecl name with
+    match evalConstCheck env opts  ModuleFacetDecl ``ModuleFacetDecl name with
     | .ok decl =>
       if h : name = decl.name then
         return OpaqueModuleFacetConfig.mk (h ▸ decl.config)
       else
         error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
-    | .error e => throw <| IO.userError e
+    | .error e => error e
   let opaquePackageFacetConfigs ← mkDTagMap env packageFacetAttr fun name => do
-    match evalConstCheck env leanOpts  PackageFacetDecl ``PackageFacetDecl name with
+    match evalConstCheck env opts  PackageFacetDecl ``PackageFacetDecl name with
     | .ok decl =>
       if h : name = decl.name then
         return OpaquePackageFacetConfig.mk (h ▸ decl.config)
       else
         error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
-    | .error e => throw <| IO.userError e
+    | .error e => error e
   let opaqueTargetConfigs ← mkTagMap env targetAttr fun declName =>
-    match evalConstCheck env leanOpts TargetConfig ``TargetConfig declName with
+    match evalConstCheck env opts TargetConfig ``TargetConfig declName with
     | .ok a => pure <| OpaqueTargetConfig.mk a
-    | .error e => throw <| IO.userError e
+    | .error e => error e
   let defaultTargets := defaultTargetAttr.ext.getState env |>.fold (·.push ·) #[]
 
   -- Issue Warnings
-  if config.extraDepTarget.isSome then
+  if self.config.extraDepTarget.isSome then
     logWarning <| "`extraDepTarget` has been deprecated. " ++
       "Try to use a custom target or raise an issue about your use case."
-  if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then
+  if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && self.defaultFacet ≠ .none then
     logWarning <| "Package targets are deprecated. " ++
       "Add a `lean_exe` and/or `lean_lib` default target to the package instead."
 
-  -- Construct the Package
-  let some dir := dirExt.getState env
-    | error "configuration environment has no package directory set"
-  return {
-    dir, config, scripts, dependencies,
-    leanLibConfigs, leanExeConfigs, externLibConfigs,
-    opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs,
-    defaultTargets
+  -- Fill in the Package
+  return {self with
+    opaqueDeps := deps.map (.mk ·)
+    leanLibConfigs, leanExeConfigs, externLibConfigs
+    opaqueModuleFacetConfigs, opaquePackageFacetConfigs, opaqueTargetConfigs
+    defaultTargets, scripts
   }
-
-/-- Load a `Package` from a configuration environment. -/
-@[implementedBy unsafeLoadFromEnv] opaque Package.loadFromEnv
-(env : Environment) (leanOpts := Options.empty) : LogIO Package
-
-/--
-Load the `Package` located in
-the given directory with the given configuration file.
--/
-def Package.load (dir : FilePath) (configOpts : NameMap String)
-(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package := do
-  Package.loadFromEnv (← elabConfigFile dir configOpts configFile leanOpts)
diff --git a/Lake/Load/Resolve.lean b/Lake/Load/Resolve.lean
deleted file mode 100644
index f3bc2e5..0000000
--- a/Lake/Load/Resolve.lean
+++ /dev/null
@@ -1,47 +0,0 @@
-/-
-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) : ManifestM 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) : ManifestM (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}"
diff --git a/Lake/Load/Workspace.lean b/Lake/Load/Workspace.lean
deleted file mode 100644
index 7802444..0000000
--- a/Lake/Load/Workspace.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-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
-
-namespace Lake
-
-def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
-  Lean.searchPathRef.set config.env.leanSearchPath
-  let root ← Package.load config.rootDir config.options config.configFile
-  let ws : Workspace := {root, env := config.env}
-  let manifest ← Manifest.loadFromFile ws.manifestFile |>.catchExceptions fun _ => pure {}
-  let (packageMap, manifest) ← resolveDeps ws root updateDeps |>.run manifest
-  unless manifest.isEmpty do
-    manifest.saveToFile ws.manifestFile
-  let packageMap := packageMap.insert root.name root
-  return {ws with packageMap}
diff --git a/Lake/Util/Error.lean b/Lake/Util/Error.lean
index ddb06af..4ea73ca 100644
--- a/Lake/Util/Error.lean
+++ b/Lake/Util/Error.lean
@@ -19,6 +19,9 @@ instance : MonadError IO where
 instance : MonadError (EIO String) where
   error msg := throw msg
 
+instance : MonadError (Except String) where
+  error msg := throw msg
+
 /--
 Perform an EIO action.
 If it throws an error, invoke `error` with its string representation.