feat: resolve depss while loading a pkg

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
   )
 

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)

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,21 +106,21 @@ 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
       (kvPair.toName, "")
     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

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 -/
 

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

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)

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

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

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

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}