refactor; cleanup (primarly resolve code)

Lake/CLI/Main.lean

@@ -16,7 +16,7 @@ import Lake.CLI.Error
 -- # CLI
 
 open System
-open Lean (Json toJson fromJson?)
+open Lean (Json toJson fromJson? LeanPaths)
 
 namespace Lake
 
@@ -190,7 +190,12 @@ def printPaths (config : LoadConfig) (imports : List String := []) : MainM PUnit
     let ws ← MainM.runLogIO (loadWorkspace config) config.verbosity
     let ctx ← mkBuildContext ws
     let dynlibs ← ws.root.buildImportsAndDeps imports |>.run (MonadLog.eio config.verbosity) ctx
-    IO.println <| Json.compress <| toJson {ws.leanPaths with loadDynlibPaths := dynlibs}
+    IO.println <| Json.compress <| toJson {
+      oleanPath := ws.leanPath
+      srcPath := ws.leanSrcPath
+      loadDynlibPaths := dynlibs
+      : LeanPaths
+    }
   else
     exit noConfigFileCode
 

Lake/Config/Package.lean

@@ -222,6 +222,10 @@ abbrev name (self : Package) : Name :=
 @[inline] def deps (self : Package) : Array Package  :=
   self.opaqueDeps.map (·.get)
 
+/-- The package's `packagesDir` configuration. -/
+def packagesDir (self : Package) : FilePath :=
+  self.dir / self.config.packagesDir
+
 /-- The package's JSON manifest of remote dependencies. -/
 def manifestFile (self : Package) : FilePath :=
   self.dir / self.config.packagesDir / manifestFileName

Lake/Config/Workspace.lean

@@ -10,7 +10,6 @@ import Lake.Config.Env
 import Lake.Util.Log
 
 open System
-open Lean (LeanPaths)
 
 namespace Lake
 
@@ -35,21 +34,17 @@ hydrate_opaque_type OpaqueWorkspace Workspace
 namespace Workspace
 
 /-- The path to the workspace's directory (i.e., the directory of the root package). -/
-def dir (self : Workspace) : FilePath :=
+@[inline] def dir (self : Workspace) : FilePath :=
   self.root.dir
 
 /-- The workspace's configuration. -/
-def config (self : Workspace) : WorkspaceConfig :=
+@[inline] def config (self : Workspace) : WorkspaceConfig :=
   self.root.config.toWorkspaceConfig
 
 /-- The workspace's `dir` joined with its `packagesDir` configuration. -/
-def packagesDir (self : Workspace) : FilePath :=
+@[inline] def packagesDir (self : Workspace) : FilePath :=
   self.dir / self.config.packagesDir
 
-/-- The workspace's JSON manifest of packages. -/
-def manifestFile (self : Workspace) : FilePath :=
-  self.packagesDir / manifestFileName
-
 /-- The `List` of packages to the workspace. -/
 def packageList (self : Workspace) : List Package :=
   self.packageMap.revFold (fun pkgs _ pkg => pkg :: pkgs) []
@@ -63,7 +58,7 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace :=
   {self with packageMap := self.packageMap.insert pkg.name pkg}
 
 /-- Get a package within the workspace by name. -/
-def findPackage? (pkg : Name) (self : Workspace) : Option Package :=
+@[inline] def findPackage? (pkg : Name) (self : Workspace) : Option Package :=
   self.packageMap.find? pkg
 
 /-- Check if the module is local to any package in the workspace. -/
@@ -99,7 +94,7 @@ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Wor
   {self with moduleFacetConfigs := self.moduleFacetConfigs.insert name cfg}
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
-def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
+@[inline] def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
   self.moduleFacetConfigs.find? name
 
 /-- Add a package facet to the workspace. -/
@@ -107,7 +102,7 @@ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : W
   {self with packageFacetConfigs := self.packageFacetConfigs.insert name cfg}
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
-def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
+@[inline] def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
   self.packageFacetConfigs.find? name
 
 /-- Add a library facet to the workspace. -/
@@ -115,7 +110,7 @@ def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : W
   {self with libraryFacetConfigs := self.libraryFacetConfigs.insert cfg.name cfg}
 
 /-- Try to find a library facet configuration in the workspace with the given name. -/
-def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
+@[inline] def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) :=
   self.libraryFacetConfigs.find? name
 
 /-- The `LEAN_PATH` of the workspace. -/
@@ -133,11 +128,6 @@ This is added to the `sharedLibPathEnvVar` by `lake env`.
 def libPath (self : Workspace) : SearchPath :=
   self.packageList.map (·.libDir)
 
-/-- The `LeanPaths` of the workspace. -/
-def leanPaths (self : Workspace) : LeanPaths where
-  oleanPath := self.packageList.map (·.oleanDir)
-  srcPath := self.packageList.map (·.srcDir)
-
 /--
 Rhe detected `LEAN_PATH` of the environment
 augmented with the workspace's `leanPath` and Lake's `libDir`.

Lake/Load/Main.lean

@@ -19,39 +19,20 @@ open System Lean
 namespace Lake
 
 /-- Load the tagged `Dependency` definitions from a package configuration environment. -/
-def loadDeps (env : Environment) (opts : Options) : Except String (Array Dependency) := do
+def loadDepsFromEnv (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
 
-/-- Add entries from `pkg`'s manifest to this one. -/
-def Manifest.appendPackageManifest (self : Manifest) (pkg : Package) : LogIO Manifest := do
-  let mut result := self
-  let pkgManifest ← Manifest.loadOrEmpty pkg.manifestFile
-  for pkgEntry in pkgManifest do
-    if let some entry := self.find? pkgEntry.name then
-      let shouldUpdate :=
-        match entry.inputRev?, pkgEntry.inputRev? with
-        | none,     none     => entry.rev != pkgEntry.rev
-        | none,     some _   => false
-        | some _,   none     => false
-        | some rev, some dep => rev = dep ∧ entry.rev ≠ pkgEntry.rev
-      let contributors := entry.contributors.insert pkg.name pkgEntry.toPersistentPackageEntry
-      result := result.insert {entry with contributors, shouldUpdate}
-    else
-      let contributors := NameMap.empty.insert pkg.name pkgEntry.toPersistentPackageEntry
-      result := result.insert {pkgEntry with contributors}
-  return result
-
 /--
 Resolve a single dependency and load the resulting package.
 Resolution is based on the `Dependency` configuration and the package manifest.
 -/
-def resolveDep (ws : Workspace) (pkg : Package) (dep : Dependency)
+def resolveDep (packagesDir : FilePath) (pkg : Package) (dep : Dependency)
 (topLevel : Bool) (shouldUpdate : Bool) : StateT Manifest LogIO Package := do
   let entry? := (← get).find? dep.name
   let entry? := entry?.map fun entry =>
     {entry with shouldUpdate := if topLevel then shouldUpdate else entry.shouldUpdate}
-  let ⟨dir, url?, tag?, entry?⟩ ← materializeDep ws.packagesDir pkg.dir dep entry?
+  let ⟨dir, url?, tag?, entry?⟩ ← materializeDep packagesDir pkg.dir dep entry?
   let configEnv ← elabConfigFile dir dep.options pkg.leanOpts (dir / defaultConfigFile)
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv pkg.leanOpts
   let depPkg : Package := {
@@ -85,20 +66,20 @@ def resolveDep (ws : Workspace) (pkg : Package) (dep : Dependency)
 Resolves the package's dependencies,
 downloading and/or updating them as necessary.
 -/
-def resolveDeps (ws : Workspace) (pkg : Package) (shouldUpdate := true) : LogIO Package := do
-  let manifest ← Manifest.loadOrEmpty pkg.manifestFile
-  let (pkg, manifest) ← StateT.run (s := manifest) do
+def Package.resolveDeps (root : Package) (shouldUpdate := true) : LogIO Package := do
+  let manifest ← Manifest.loadOrEmpty root.manifestFile
+  let (root, manifest) ← StateT.run (s := manifest) do
     let res ← EStateT.run' (mkNameMap Package) do
-      buildAcyclic (·.name) pkg fun pkg resolve => do
-        let topLevel := pkg.name = ws.root.name
-        let deps ← IO.ofExcept <| loadDeps pkg.configEnv pkg.leanOpts
+      buildAcyclic (·.name) root fun pkg resolve => do
+        let topLevel := pkg.name = root.name
+        let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
         let depPkgs ← deps.mapM fun dep => do
           fetchOrCreate dep.name do
-            liftM <| resolveDep ws pkg dep topLevel shouldUpdate
+            liftM <| resolveDep root.packagesDir pkg dep topLevel shouldUpdate
         return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
     match res with
-    | Except.ok pkg =>
-      return pkg
+    | Except.ok root =>
+      return root
     | Except.error cycle =>
       let cycle := cycle.map (s!"  {·}")
       error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
@@ -112,8 +93,8 @@ def resolveDeps (ws : Workspace) (pkg : Package) (shouldUpdate := true) : LogIO
         let inputRev := entry.inputRev?.getD Git.upstreamBranch
         log := log ++  s!"Using `{inputRev}` at `{entry.rev}`"
         logInfo log
-    manifest.saveToFile ws.manifestFile
-  return pkg
+    manifest.saveToFile root.manifestFile
+  return root
 
 /--
 Finalize the workspace's root and its transitive dependencies
@@ -160,5 +141,5 @@ def loadWorkspace (config : LoadConfig) : LogIO Workspace := do
     packageFacetConfigs := initPackageFacetConfigs
     libraryFacetConfigs := initLibraryFacetConfigs
   }
-  let root ← resolveDeps ws root config.updateDeps
+  let root ← root.resolveDeps config.updateDeps
   {ws with root}.finalize