feat: introduce Workspace which is shared across a pkg and its deps

Lake/LeanConfig.lean

@@ -56,7 +56,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
       let config ← evalPackageDecl env pkgDeclName dir args leanOpts
       let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
         fun m d => do m.insert d <| ← evalScriptDecl env d leanOpts
-      return Package.mk dir config scripts
+      return {dir, config, scripts}
     | _ =>
       throw <| IO.userError
         s!"configuration file has multiple `package` declarations"

Lake/Package.lean

@@ -41,7 +41,7 @@ def defaultDepsDir : FilePath := "lean_packages"
 def defaultBinRoot : Name := `Main
 
 --------------------------------------------------------------------------------
--- # PackageConfig Helpers
+-- # Auxiliary Definitions and Helpers
 --------------------------------------------------------------------------------
 
 /--
@@ -99,12 +99,45 @@ def toUpperCamelCase (name : Name) : Name :=
   else
     name
 
+--------------------------------------------------------------------------------
+-- # WorkspaceConfig
+--------------------------------------------------------------------------------
+
+/-- A workspace's declarative configuration. -/
+structure WorkspaceConfig where
+  /--
+    The directory to which Lake should download dependencies.
+    Defaults to `defaultDepsDir` (i.e., `lean_packages`).
+  -/
+  depsDir : FilePath := defaultDepsDir
+  deriving Inhabited, Repr
+
+
+--------------------------------------------------------------------------------
+-- # Workspace
+--------------------------------------------------------------------------------
+
+structure Workspace where
+  /-- The path to the workspace's directory. -/
+  dir : FilePath
+  /-- The workspace's configuration. -/
+  config : WorkspaceConfig
+  deriving Inhabited, Repr
+
+namespace Workspace
+
+/-- The workspace's `dir` joined with its `depsDir` configuration. -/
+def depsDir (self : Workspace) : FilePath :=
+  self.dir / self.config.depsDir
+
+end Workspace
+
 --------------------------------------------------------------------------------
 -- # PackageConfig
 --------------------------------------------------------------------------------
 
 /-- A package's declarative configuration. -/
-structure PackageConfig where
+structure PackageConfig extends WorkspaceConfig where
 
   /--
     The `Name` of the package.
@@ -117,12 +150,6 @@ structure PackageConfig where
   -/
   dependencies : Array Dependency := #[]
 
-  /--
-    The directory to which Lake should download dependencies.
-    Defaults to `defaultDepsDir` (i.e., `lean_packages`).
-  -/
-  depsDir : FilePath := defaultDepsDir
-
   /--
     An extra `OpaqueTarget` that should be built before the package.
 
@@ -257,6 +284,8 @@ structure Package where
   dir : FilePath
   /-- The package's configuration. -/
   config : PackageConfig
+  /-- The workspace the package is contained in. -/
+  workspace : Workspace := {dir, config := config.toWorkspaceConfig}
   /--
     A `NameMap` of scripts for the package.
 
@@ -280,6 +309,14 @@ def IOPackager := (pkgDir : FilePath) → (args : List String) → IO PackageCon
 
 namespace Package
 
+/-- Replace the package's workspace. -/
+def withWorkspace (ws : Workspace) (self : Package) : Package :=
+  {self with workspace := ws}
+
+/-- The workspace's `depsDir`. -/
+def depsDir (self : Package) : FilePath :=
+  self.workspace.depsDir
+
 /-- The package's `name` configuration. -/
 def name (self : Package) : Name :=
   self.config.name
@@ -292,10 +329,6 @@ def dependencies (self : Package) : Array Dependency :=
 def extraDepTarget (self : Package) : OpaqueTarget :=
   self.config.extraDepTarget
 
-/-- The package's `dir` joined with its `depsDir` configuration. -/
-def depsDir (self : Package) : FilePath :=
-  self.dir / self.config.depsDir
-
 /-- The package's `dir` joined with its `srcDir` configuration. -/
 def srcDir (self : Package) : FilePath :=
   self.dir / self.config.srcDir

Lake/Resolve.lean

@@ -31,7 +31,7 @@ def materializeGit
     checkoutDetach hash dir
 
 /--
-  Materializes a dependency relative to the given package,
+  Materializes a `Dependency` relative to the given `Package`,
   downloading and/or updating it as necessary.
 -/
 def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath :=
@@ -44,8 +44,8 @@ def materializeDep (pkg : Package) (dep : Dependency) : IO FilePath :=
     depDir
 
 /--
-  Resolves a dependency relative to the given package,
-  downloading and/or updating it as necessary.
+  Resolves a `Dependency` relative to the given `Package`
+  in the same `Workspace`, downloading and/or updating it as necessary.
 -/
 def resolveDep (pkg : Package) (dep : Dependency) : IO Package := do
   let dir ← materializeDep pkg dep
@@ -54,7 +54,7 @@ def resolveDep (pkg : Package) (dep : Dependency) : IO Package := 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
+  return depPkg.withWorkspace pkg.workspace
 
 /--
   Resolves the package's direct dependencies,

README.md

@@ -84,11 +84,16 @@ Hello, world!
 
 Lake provides a large assortment of configuration options for packages.
 
+### Workspace
+
+Workspace options are shared across a package and its dependencies.
+
+* `depsDir`: The directory to which Lake should download dependencies. Defaults to `lean_packages`.
+
 ### General
 
 * `name` **(Required)**: The `Name` of the package.
 * `dependencies`: An `Array` of the package's dependencies.
-* `depsDir`: The directory to which Lake should download dependencies. Defaults to `lean_packages`.
 * `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `OpaqueTarget.collectList/collectArray` can be used combine multiple extra targets into a single `extraDepTarget`.
 * `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.)
 * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.
@@ -101,7 +106,7 @@ Lake provides a large assortment of configuration options for packages.
 
 * `moreLeancArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Lake already passes `-O3` and `-DNDEBUG` automatically, but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
 * `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`.
-* `libName`: The name of the package's static library. Defaults to the string representation of the package's `moduleRoot`.
+* `libName`: The name of the package's static library. Defaults to the package's upper camel case `name`.
 * `libDir`: The build subdirectory to which Lake should output the package's static library. Defaults to `lib`.
 * `binName`: The name of the package's binary executable. Defaults to the package's `name` with any `.` replaced with a `-`.
 * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`.