refactor: introduce LakefileConfig & well-formed workspaces (#13282)

This PR introduces `LakefileConfig`, which can be constructed from a
Lake configuration file without all the information required to
construct a full `Package`. Also, workspaces now have a well-formedness
property attached which ensures the workspace indices of its packages
match their index in the workspace. Finally, the facet configuration map
now has its own type: `FacetConfigMap`.

Created by splitting off the major self-contained (but overlapping)
refactors from #11662.

src/lake/Lake/Build/InitFacets.lean

@@ -19,7 +19,7 @@ import Lake.Build.InputFile
 namespace Lake
 
 /-- The initial set of Lake facets. -/
-public def initFacetConfigs : DNameMap FacetConfig :=
+public def initFacetConfigs : FacetConfigMap :=
   DNameMap.empty
   |> insert Module.initFacetConfigs
   |> insert Package.initFacetConfigs
@@ -30,4 +30,4 @@ public def initFacetConfigs : DNameMap FacetConfig :=
   |> insert InputDir.initFacetConfigs
 where
   insert {k} (group : DNameMap (KFacetConfig k)) map :=
-    group.foldl (init := map) fun m k v => m.insert k v.toFacetConfig
+    group.foldl (init := map) fun m _ v => m.insert v.toFacetConfig

src/lake/Lake/Config/FacetConfig.lean

@@ -27,6 +27,20 @@ public structure FacetConfig (name : Name) : Type where
   memoize : Bool := true
   deriving Inhabited
 
+/-- A mapping of facet names to the configuration for that name. -/
+public abbrev FacetConfigMap := DNameMap FacetConfig
+
+/--
+Tries to retrieve the facet configuration for the given {lean}`name`,
+returning {lean}`none` if no such mapping is present.
+-/
+public nonrec def FacetConfigMap.get? (name : Name) (self : FacetConfigMap) : Option (FacetConfig name) :=
+  self.get? name -- specializes `get?`
+
+/-- Inserts the facet configuration {lean}`cfg` into the map (overwriting any existing configuration). -/
+public nonrec def FacetConfigMap.insert {name} (cfg : FacetConfig name) (self : FacetConfigMap) : FacetConfigMap :=
+  self.insert name cfg -- specializes `insert`
+
 public protected abbrev FacetConfig.name (_ : FacetConfig name) := name
 
 public structure KFacetConfig (k : Name) (name : Name) extends FacetConfig name where
@@ -70,6 +84,9 @@ public structure NamedConfigDecl (β : Name → Type u) where
   name : Name
   config : β name
 
+/-- A facet declaration from a configuration file. -/
+public abbrev FacetDecl := NamedConfigDecl FacetConfig
+
 /-- A module facet's declarative configuration. -/
 public abbrev ModuleFacetConfig := KFacetConfig Module.facetKind
 

src/lake/Lake/Config/LakefileConfig.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+module
+
+prelude
+public import Lake.Config.Script
+public import Lake.Config.Dependency
+public import Lake.Config.PackageConfig
+public import Lake.Config.FacetConfig
+public import Lake.Config.TargetConfig
+
+set_option doc.verso true
+
+open Lean
+
+namespace Lake
+
+/-- The configuration defined by a Lake configuration file (e.g., {lit}`lakefile.(lean|toml)`). -/
+public structure LakefileConfig where
+  /-- The package deceleration of the configuration file. -/
+  pkgDecl : PackageDecl
+  /-- Depdency configurations in the order declared by the configuration file.  -/
+  depConfigs : Array Dependency := #[]
+  /-- Facet configurations in the order declared by the configuration file. -/
+  facetDecls : Array FacetDecl := {}
+  /-- Target configurations in the order declared by the configuration file. -/
+  targetDecls : Array (PConfigDecl pkgDecl.keyName) := #[]
+  /-- Name-declaration map of target configurations declared in the configuration file. -/
+  targetDeclMap : DNameMap (NConfigDecl pkgDecl.keyName) :=
+    targetDecls.foldl (fun m d => m.insert d.name (.mk d rfl)) {}
+  /-- The names of targets declared via {lit}`@[default_target]`. -/
+  defaultTargets : Array Name := #[]
+  /-- Scripts declared in the configuration file. -/
+  scripts : NameMap Script := {}
+  /-- The names of the scripts declared via {lit}`@[default_script]`. -/
+  defaultScripts : Array Script := #[]
+  /-- {lit}`post_update` hooks in the order declared by the configuration file.. -/
+  postUpdateHooks : Array (OpaquePostUpdateHook pkgDecl.keyName) := #[]
+  /--
+  The name of the configuration file's test driver.
+
+  It is either  declared via {lit}`@[test_driver]` or derived from {lean}`PackageConfig.testDriver`.
+  -/
+  testDriver : String := pkgDecl.config.testDriver
+  /--
+  The name of the configuration file's test driver.
+
+  It is either declared via {lit}`@[lint_driver]` or derived from {lean}`PackageConfig.lintDriver`.
+  -/
+  lintDriver : String := pkgDecl.config.lintDriver

src/lake/Lake/Config/Package.lean

@@ -45,7 +45,7 @@ public structure Package where
   /-- The path to the package's configuration file (relative to `dir`). -/
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
-  relManifestFile : FilePath := defaultManifestFile
+  relManifestFile : FilePath
   /-- The package's scope (e.g., in Reservoir). -/
   scope : String
   /-- The URL to this package's Git remote. -/

src/lake/Lake/Config/PackageConfig.lean

@@ -336,11 +336,16 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
 deriving Inhabited
 
 /-- The package's name as specified by the author. -/
+@[deprecated "Deprecated without replacement" (since := "2025-12-10")]
 public abbrev PackageConfig.origName (_ : PackageConfig p n) := n
 
 /-- A package declaration from a configuration written in Lean. -/
 public structure PackageDecl where
-  name : Name
+  baseName : Name
+  keyName : Name
   origName : Name
-  config : PackageConfig name origName
+  config : PackageConfig keyName origName
   deriving TypeName
+
+@[deprecated PackageDecl.keyName (since := "2025-12-10")]
+public abbrev PackageDecl.name := @keyName

src/lake/Lake/Config/Workspace.lean

@@ -22,15 +22,17 @@ open Lean (Name LeanOptions)
 
 namespace Lake
 
-/-- **For internal use only.** Computes the cache to use for the package based on the environment. -/
+/--
+**For internal use only.**
+Computes the cache to use for the package based on the environment.
+-/
 public def computeLakeCache (pkg : Package) (lakeEnv : Lake.Env) : Cache :=
   if pkg.bootstrap then
     lakeEnv.lakeSystemCache?.getD ⟨pkg.lakeDir / "cache"⟩
   else
     lakeEnv.lakeCache?.getD ⟨pkg.lakeDir / "cache"⟩
 
-/-- A Lake workspace -- the top-level package directory. -/
-public structure Workspace : Type where
+public structure Workspace.Raw : Type where
   /-- The root package of the workspace. -/
   root : Package
   /-- The detected {lean}`Lake.Env` of the workspace. -/
@@ -49,14 +51,25 @@ public structure Workspace : Type where
   The packages within the workspace
   (in {lit}`require` declaration order with the root coming first).
   -/
-  packages : Array Package := {}
+  packages : Array Package := #[]
   /-- Name-package map of packages within the workspace. -/
   packageMap : DNameMap NPackage := {}
   /-- Configuration map of facets defined in the workspace. -/
-  facetConfigs : DNameMap FacetConfig := {}
+  facetConfigs : FacetConfigMap := {}
+  deriving Nonempty
 
-public instance : Nonempty Workspace :=
-  ⟨by constructor <;> exact Classical.ofNonempty⟩
+public structure Workspace.Raw.WF (ws : Workspace.Raw) : Prop where
+  packages_wsIdx : ∀ (h : i < ws.packages.size), (ws.packages[i]'h).wsIdx = i
+
+/-- A Lake workspace -- the top-level package directory. -/
+public structure Workspace extends raw : Workspace.Raw, wf : raw.WF
+
+public instance : Nonempty Workspace := .intro {
+  lakeEnv := default
+  lakeConfig := Classical.ofNonempty
+  root := Classical.ofNonempty
+  packages_wsIdx h := by simp at h
+}
 
 public hydrate_opaque_type OpaqueWorkspace Workspace
 
@@ -175,9 +188,20 @@ This is configured through {lit}`cache.service` entries in the system Lake confi
 @[inline] public def packageOverridesFile (self : Workspace) : FilePath :=
   self.lakeDir / "package-overrides.json"
 
+/-- **For internal use only.** Add a well-formed package to the workspace. -/
+@[inline] public def addPackage' (pkg : Package) (self : Workspace) (h : pkg.wsIdx = self.packages.size) : Workspace :=
+  {self with
+    packages := self.packages.push pkg
+    packageMap := self.packageMap.insert pkg.keyName pkg
+    packages_wsIdx {i} i_lt := by
+      cases Nat.lt_add_one_iff_lt_or_eq.mp <| Array.size_push .. ▸ i_lt with
+      | inl i_lt => simpa [Array.getElem_push_lt i_lt] using self.packages_wsIdx i_lt
+      | inr i_eq => simpa [i_eq] using h
+  }
+
 /-- Add a package to the workspace. -/
-public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
-  {self with packages := self.packages.push pkg, packageMap := self.packageMap.insert pkg.keyName pkg}
+@[inline] public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
+  self.addPackage' {pkg with wsIdx := self.packages.size} rfl
 
 /-- Returns the unique package in the workspace (if any) that is identified by  {lean}`keyName`. -/
 @[inline] public protected def findPackageByKey? (keyName : Name) (self : Workspace) : Option (NPackage keyName) :=
@@ -251,15 +275,15 @@ public def findTargetDecl? (name : Name) (self : Workspace) : Option ((pkg : Pac
   self.packages.findSome? fun pkg => pkg.findTargetDecl? name <&> (⟨pkg, ·⟩)
 
 /-- Add a facet to the workspace. -/
-public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
-  {self with facetConfigs := self.facetConfigs.insert name cfg}
+@[inline] public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
+  {self with facetConfigs := self.facetConfigs.insert cfg}
 
 /-- Try to find a facet configuration in the workspace with the given name. -/
-public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
+@[inline] public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
   self.facetConfigs.get? name
 
 /-- Add a module facet to the workspace. -/
-public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
+@[inline] public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
@@ -267,7 +291,7 @@ public def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (Mod
   self.findFacetConfig? name |>.bind (·.toKind? Module.facetKind)
 
 /-- Add a package facet to the workspace. -/
-public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
+@[inline] public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
@@ -275,7 +299,7 @@ public def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (Pa
   self.findFacetConfig? name |>.bind (·.toKind? Package.facetKind)
 
 /-- Add a library facet to the workspace. -/
-public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
+@[inline] public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a library facet configuration in the workspace with the given name. -/

src/lake/Lake/DSL/Package.lean

@@ -26,17 +26,18 @@ def elabPackageCommand : CommandElab := fun stx => do
   let configId : Ident ← `(pkgConfig)
   let id ← mkConfigDeclIdent nameStx?
   let origName := Name.quoteFrom id id.getId
-  let ⟨idx, name⟩ := nameExt.getState (← getEnv)
-  let name := match name with
+  let ⟨wsIdx, name⟩ := nameExt.getState (← getEnv)
+  let baseName := match name with
     | .anonymous => origName
     | name => Name.quoteFrom id name
-  let name := Syntax.mkCApp ``Name.num #[name, quote idx]
-  let ty := Syntax.mkCApp ``PackageConfig #[name, origName]
+  let wsIdx := quote wsIdx
+  let keyName := Syntax.mkCApp ``Name.num #[baseName, wsIdx]
+  let ty := Syntax.mkCApp ``PackageConfig #[keyName, origName]
   elabConfig ``PackageConfig configId ty cfg
   let attr ← `(Term.attrInstance| «package»)
   let attrs := #[attr] ++ expandAttrs attrs?
   let id := mkIdentFrom id packageDeclName
-  let decl ← `({name := $name, origName := $origName, config := $configId})
+  let decl ← `({baseName := $baseName, origName := $origName, keyName := $keyName, config := $configId})
   let cmd ← `($[$doc?]? @[$attrs,*] abbrev $id : PackageDecl := $decl)
   withMacroExpansion stx cmd <| elabCommand cmd
   let nameId := mkIdentFrom id <| packageDeclName.str "name"

src/lake/Lake/Load/Config.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lake.Config.Env
+public import Lake.Config.Lang
 public import Lake.Config.LakeConfig
 public import Lake.Load.Manifest
 
@@ -41,8 +42,16 @@ public structure LoadConfig where
   pkgDir : FilePath := wsDir / relPkgDir
   /-- The package's Lake configuration file (relative to its directory). -/
   relConfigFile : FilePath := defaultConfigFile
-    /-- The full path to the loaded package's Lake configuration file. -/
+  /-- The full path to the loaded package's Lake configuration file. -/
   configFile : FilePath := pkgDir / relConfigFile
+  /-
+  The format of the package's configuration file.
+
+  If {lean}`none`, the format will be determined by the file's extension.
+  -/
+  configLang? : Option ConfigLang := none
+  /-- The package's Lake manifest file (relative to its directory). -/
+  relManifestFile : FilePath := defaultManifestFile
   /-- Additional package overrides for this workspace load. -/
   packageOverrides : Array PackageEntry := #[]
   /-- A set of key-value Lake configuration options (i.e., {lit}`-K` settings). -/
@@ -55,6 +64,7 @@ public structure LoadConfig where
   updateDeps : Bool := false
   /--
   Whether to update the workspace's {lit}`lean-toolchain` when dependencies are updated.
+
   If {lean}`true` and a toolchain update occurs, Lake will need to be restarted.
   -/
   updateToolchain : Bool := true

src/lake/Lake/Load/Lean.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lake.Config.Package
+public import Lake.Config.LakefileConfig
 public import Lake.Load.Config
 import Lake.Load.Lean.Elab
 import Lake.Load.Lean.Eval
@@ -21,22 +22,7 @@ open Lean
 
 namespace Lake
 
-/--
-Elaborate a Lean configuration file into a `Package`.
-The resulting package does not yet include any dependencies.
--/
-public def loadLeanConfig (cfg : LoadConfig) : LogIO (Package × Environment) := do
+/-- Elaborate a Lake configuration file written in Lean and extract the Lake configuration.  -/
+public def loadLeanConfig  (cfg : LoadConfig) : LogIO LakefileConfig := do
   let configEnv ← importConfigFile cfg
-  let ⟨keyName, origName, config⟩ ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
-  let baseName := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
-  let pkg : Package := {
-    wsIdx := cfg.pkgIdx
-    baseName, keyName, origName, config
-    dir := cfg.pkgDir
-    relDir := cfg.relPkgDir
-    configFile := cfg.configFile
-    relConfigFile := cfg.relConfigFile
-    scope := cfg.scope
-    remoteUrl := cfg.remoteUrl
-  }
-  return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)
+  LakefileConfig.loadFromEnv configEnv cfg.leanOpts

src/lake/Lake/Load/Lean/Eval.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lake.Config.Workspace
+public import Lake.Config.LakefileConfig
 import Lean.DocString
 import Lake.DSL.AttributesCore
 
@@ -75,39 +76,38 @@ private def mkOrdTagMap
     return map.insert declName <| ← f declName
 
 /-- Load a `PackageDecl` from a configuration environment. -/
-public def PackageDecl.loadFromEnv
+private def PackageDecl.loadFromEnv
   (env : Environment) (opts := Options.empty)
 : Except String PackageDecl := do
   let declName ←
     match packageAttr.getAllEntries env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
-    | [name] => pure name
+    | [keyName] => pure keyName
     | _ => error s!"configuration file has multiple `package` declarations"
   evalConstCheck env opts _ declName
 
-/--
-Load the optional elements of a `Package` from the Lean environment.
-This is done after loading its core configuration but before resolving
-its dependencies.
--/
-public def Package.loadFromEnv
-  (self : Package) (env : Environment) (opts : Options)
-: LogIO Package := do
+/-- Load a Lake configuration from a configuration file's environment. -/
+public def LakefileConfig.loadFromEnv
+  (env : Environment) (opts : Options)
+: LogIO LakefileConfig := do
+
+  -- load package declaration
+  let pkgDecl ← IO.ofExcept <| PackageDecl.loadFromEnv env opts
+  let prettyName := pkgDecl.baseName.toString (escape := false)
+  let keyName := pkgDecl.keyName
 
   -- load target, script, hook, and driver configurations
   let constTargetMap ← IO.ofExcept <| mkOrdTagMap env targetAttr fun name => do
     evalConstCheck env opts ConfigDecl name
   let targetDecls ← constTargetMap.toArray.mapM fun decl => do
-    if h : decl.pkg = self.keyName then
+    if h : decl.pkg = keyName then
       return .mk decl h
     else
-      error s!"\
-        target '{decl.name}' was defined in package '{decl.pkg}', \
-        but registered under '{self.keyName}'"
+      error s!"target '{decl.name}' was defined in package '{decl.pkg}', \
+        but registered under '{keyName}'"
   let targetDeclMap ← targetDecls.foldlM (init := {}) fun m decl => do
     if let some orig := m.get? decl.name then
-      error s!"\
-        {self.prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
+      error s!"{prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
         but then redefined as a '{decl.kind}'"
     else
       return m.insert decl.name (.mk decl rfl)
@@ -116,8 +116,7 @@ public def Package.loadFromEnv
     if let some exeConfig := decl.config? LeanExe.configKind then
       let root := exeConfig.root
       if let some origExe := exeRoots.get? root then
-        error s!"\
-          {self.prettyName}: executable '{decl.name}' has the same root module '{root}' \
+        error s!"{prettyName}: executable '{decl.name}' has the same root module '{root}' \
           as executable '{origExe}'"
       else
         return exeRoots.insert root decl.name
@@ -125,80 +124,78 @@ public def Package.loadFromEnv
       return exeRoots
   let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then pure decl.name else
-      error s!"{self.prettyName}: package is missing target '{name}' marked as a default"
+      error s!"{prettyName}: package is missing target '{name}' marked as a default"
   let scripts ← mkTagMap env scriptAttr fun scriptName => do
-    let name := self.prettyName ++ "/" ++ scriptName.toString (escape := false)
+    let name := prettyName ++ "/" ++ scriptName.toString (escape := false)
     let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn scriptName
     return {name, fn, doc? := ← findDocString? env scriptName : Script}
   let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name =>
     if let some script := scripts.get? name then pure script else
-      error s!"{self.prettyName}: package is missing script '{name}' marked as a default"
+      error s!"{prettyName}: package is missing script '{name}' marked as a default"
   let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name =>
     match evalConstCheck env opts PostUpdateHookDecl name with
     | .ok decl =>
-      if h : decl.pkg = self.keyName then
-        return OpaquePostUpdateHook.mk ⟨cast (by rw [h, keyName]) decl.fn⟩
+      if h : decl.pkg = keyName then
+        return OpaquePostUpdateHook.mk ⟨cast (by rw [h]) decl.fn⟩
       else
-        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{self.keyName}'"
+        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{keyName}'"
     | .error e => error e
   let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
     evalConstCheck env opts Dependency name
   let testDrivers ← testDriverAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then
-      pure decl.name
+      return decl.name
     else if scripts.contains name then
-      pure name
+      return name
     else
-      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a test driver"
-  let testDriver ←
+      error s!"{prettyName}: package is missing script or target '{name}' marked as a test driver"
+  let testDriver ← id do
     if testDrivers.size > 1 then
-      error s!"{self.prettyName}: only one script, executable, or library can be tagged @[test_driver]"
+      error s!"{prettyName}: only one script, executable, or library can be tagged @[test_driver]"
     else if h : testDrivers.size > 0 then
-      if self.config.testDriver.isEmpty then
-        pure (testDrivers[0]'h |>.toString)
+      if pkgDecl.config.testDriver.isEmpty then
+        return (testDrivers[0]'h |>.toString)
       else
-        error s!"{self.prettyName}: cannot both set testDriver and use @[test_driver]"
+        error s!"{prettyName}: cannot both set testDriver and use @[test_driver]"
     else
-      pure self.config.testDriver
+      return pkgDecl.config.testDriver
   let lintDrivers ← lintDriverAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then
-      pure decl.name
+      return decl.name
     else if scripts.contains name then
-      pure name
+      return name
     else
-      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a lint driver"
-  let lintDriver ←
+      error s!"{prettyName}: package is missing script or target '{name}' marked as a lint driver"
+  let lintDriver ← id do
     if lintDrivers.size > 1 then
-      error s!"{self.prettyName}: only one script or executable can be tagged @[lint_driver]"
+      error s!"{prettyName}: only one script or executable can be tagged @[lint_driver]"
     else if h : lintDrivers.size > 0 then
-      if self.config.lintDriver.isEmpty then
-        pure (lintDrivers[0]'h |>.toString)
+      if pkgDecl.config.lintDriver.isEmpty then
+        return (lintDrivers[0]'h |>.toString)
       else
-        error s!"{self.prettyName}: cannot both set lintDriver and use @[lint_driver]"
+        error s!"{prettyName}: cannot both set lintDriver and use @[lint_driver]"
     else
-      pure self.config.lintDriver
+      return pkgDecl.config.lintDriver
+
+  -- load facets
+  let facetDecls ← IO.ofExcept do
+    let mut decls : Array FacetDecl := #[]
+    for name in moduleFacetAttr.getAllEntries env do
+      let decl ← evalConstCheck env opts ModuleFacetDecl name
+      decls :=  decls.push {decl with config := decl.config.toFacetConfig}
+    for name in packageFacetAttr.getAllEntries env do
+      let decl ← evalConstCheck env opts PackageFacetDecl name
+      decls := decls.push  {decl with config := decl.config.toFacetConfig}
+    for name in libraryFacetAttr.getAllEntries env do
+      let decl ← evalConstCheck env opts LibraryFacetDecl name
+      decls := decls.push  {decl with config := decl.config.toFacetConfig}
+    return decls
 
   -- Fill in the Package
-  return {self with
-    depConfigs, targetDecls, targetDeclMap
-    defaultTargets, scripts, defaultScripts
-    testDriver, lintDriver,  postUpdateHooks
+  return {
+    pkgDecl, depConfigs, facetDecls,
+    targetDecls, targetDeclMap, defaultTargets,
+    scripts, defaultScripts,
+    testDriver, lintDriver,
+    postUpdateHooks,
   }
-
-/--
-Load module/package facets into a `Workspace` from a configuration environment.
--/
-public def Workspace.addFacetsFromEnv
-  (env : Environment) (opts : Options) (self : Workspace)
-: Except String Workspace := do
-  let mut ws := self
-  for name in moduleFacetAttr.getAllEntries env do
-    let decl ← evalConstCheck env opts ModuleFacetDecl name
-    ws := ws.addModuleFacetConfig decl.config
-  for name in packageFacetAttr.getAllEntries env do
-    let decl ← evalConstCheck env opts PackageFacetDecl name
-    ws := ws.addPackageFacetConfig decl.config
-  for name in libraryFacetAttr.getAllEntries env do
-    let decl ← evalConstCheck env opts LibraryFacetDecl name
-    ws := ws.addLibraryFacetConfig decl.config
-  return ws

src/lake/Lake/Load/Manifest.lean

@@ -94,6 +94,9 @@ public structure PackageEntry where
 
 namespace PackageEntry
 
+@[inline] public def prettyName (entry : PackageEntry) : String :=
+  entry.name.toString (escape := false)
+
 public protected def toJson (entry : PackageEntry) : Json :=
   let fields := [
     ("name", toJson entry.name),

src/lake/Lake/Load/Materialize.lean

@@ -10,6 +10,7 @@ public import Lake.Config.Env
 public import Lake.Load.Manifest
 public import Lake.Config.Package
 import Lake.Util.Git
+import Lake.Util.IO
 import Lake.Reservoir
 
 open System Lean
@@ -87,6 +88,8 @@ def materializeGitRepo
     cloneGitPkg name repo url rev?
 
 public structure MaterializedDep where
+  /-- Absolute path to the materialized package. -/
+  pkgDir : FilePath
   /-- Path to the materialized package relative to the workspace's root directory. -/
   relPkgDir : FilePath
   /--
@@ -105,17 +108,32 @@ namespace MaterializedDep
 @[inline] public def name (self : MaterializedDep) : Name :=
   self.manifestEntry.name
 
+@[inline] public def prettyName (self : MaterializedDep) : String :=
+  self.manifestEntry.name.toString (escape := false)
+
 @[inline] public def scope (self : MaterializedDep) : String :=
   self.manifestEntry.scope
 
-/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def manifestFile? (self : MaterializedDep) : Option FilePath :=
+/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
+@[inline] public def relManifestFile? (self : MaterializedDep) : Option FilePath :=
   self.manifestEntry.manifestFile?
 
+/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
+@[inline] public def relManifestFile (self : MaterializedDep) : FilePath :=
+  self.relManifestFile?.getD defaultManifestFile
+
+/-- Absolute path to the dependency's manfiest file. -/
+@[inline] public def manifestFile (self : MaterializedDep) : FilePath :=
+  self.pkgDir / self.relManifestFile
+
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def configFile (self : MaterializedDep) : FilePath :=
+@[inline] public def relConfigFile (self : MaterializedDep) : FilePath :=
   self.manifestEntry.configFile
 
+/-- Absolute path to the dependency's configuration file. -/
+@[inline] public def configFile (self : MaterializedDep) : FilePath :=
+  self.pkgDir / self.relConfigFile
+
 public def fixedToolchain (self : MaterializedDep) : Bool :=
   match self.manifest? with
   | .ok manifest => manifest.fixedToolchain
@@ -157,10 +175,11 @@ public def Dependency.materialize
   (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath)
 : LoggerIO MaterializedDep := do
   if let some src := dep.src? then
+    let sname := dep.name.toString (escape := false)
     match src with
     | .path dir =>
       let relPkgDir := relParentDir / dir
-      mkDep (wsDir / relPkgDir) relPkgDir "" (.path relPkgDir)
+      mkDep sname relPkgDir "" (.path relPkgDir)
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
       let repoUrl := Git.filterUrl? url |>.getD ""
@@ -208,16 +227,19 @@ public def Dependency.materialize
     | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
   materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LoggerIO MaterializedDep := do
-    let pkgDir := wsDir / relPkgDir
-    let repo := GitRepo.mk pkgDir
+    let gitDir := wsDir / relPkgDir
+    let repo := GitRepo.mk gitDir
     let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
     materializeGitRepo name repo gitUrl inputRev?
     let rev ← repo.getHeadRevision
     let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
-    mkDep pkgDir relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
-  @[inline] mkDep pkgDir relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
+    mkDep name relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep name relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
+    let pkgDir := wsDir / relPkgDir
+    let some pkgDir ← resolvePath? pkgDir
+      | error s!"{name}: package directory not found: {pkgDir}"
     return {
-      relPkgDir, remoteUrl
+      pkgDir, relPkgDir, remoteUrl,
       manifest? :=  ← Manifest.load (pkgDir / defaultManifestFile) |>.toBaseIO
       manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
     }
@@ -231,9 +253,9 @@ public def PackageEntry.materialize
 : LoggerIO MaterializedDep :=
   match manifestEntry.src with
   | .path (dir := relPkgDir) .. =>
-    mkDep (wsDir / relPkgDir) relPkgDir ""
+    mkDep relPkgDir ""
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
-    let sname := manifestEntry.name.toString (escape := false)
+    let sname := manifestEntry.prettyName
     let relGitDir := relPkgsDir / sname
     let gitDir := wsDir / relGitDir
     let repo := GitRepo.mk gitDir
@@ -254,12 +276,15 @@ public def PackageEntry.materialize
       let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
       cloneGitPkg sname repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
-    mkDep gitDir relPkgDir (Git.filterUrl? url |>.getD "")
+    mkDep relPkgDir (Git.filterUrl? url |>.getD "")
 where
-  @[inline] mkDep pkgDir relPkgDir remoteUrl : LoggerIO MaterializedDep := do
+  @[inline] mkDep relPkgDir remoteUrl : LoggerIO MaterializedDep := do
+    let pkgDir := wsDir / relPkgDir
+    let some pkgDir ← resolvePath? pkgDir
+      | error s!"{manifestEntry.prettyName}: package directory not found: {pkgDir}"
     let manifest? ← id do
       if let some manifestFile := manifestEntry.manifestFile? then
         Manifest.load (pkgDir / manifestFile) |>.toBaseIO
       else
         return .error (.noFileOrDirectory "" 0 "")
-    return {relPkgDir, remoteUrl, manifest?, manifestEntry}
+    return {pkgDir, relPkgDir, remoteUrl, manifest?, manifestEntry}

src/lake/Lake/Load/Package.lean

@@ -8,10 +8,13 @@ module
 prelude
 public import Lake.Load.Config
 public import Lake.Config.Package
+public import Lake.Config.LakefileConfig
 import Lake.Util.IO
 import Lake.Load.Lean
 import Lake.Load.Toml
 
+set_option doc.verso true
+
 /-! # Package Loader
 
 This module contains the main definitions to load a package
@@ -23,6 +26,38 @@ open System (FilePath)
 
 namespace Lake
 
+/--
+**For interal use only.**
+
+Constructs a package from the configuration defined in its Lake configuration file
+and the load configuaration.
+-/
+public def mkPackage
+  (loadCfg : LoadConfig) (fileCfg : LakefileConfig) (wsIdx := loadCfg.pkgIdx)
+: Package :=
+  let {
+    pkgDir := dir, relPkgDir := relDir,
+    configFile, relConfigFile, relManifestFile,
+    scope, remoteUrl, ..} := loadCfg
+  let {
+    depConfigs, defaultTargets, scripts, defaultScripts, testDriver, lintDriver
+    -- destructing needed for type-correctness
+    pkgDecl, targetDecls, targetDeclMap, postUpdateHooks,
+    ..} := fileCfg
+  let {baseName, keyName, origName, config} := pkgDecl
+  {
+    wsIdx, baseName, keyName, origName, config
+    dir, relDir, configFile, relConfigFile, relManifestFile
+    scope, remoteUrl
+    depConfigs
+    targetDecls, targetDeclMap, defaultTargets
+    scripts, defaultScripts
+    testDriver, lintDriver
+    postUpdateHooks
+  }
+
+public theorem wsIdx_mkPackage : (mkPackage l f i).wsIdx = i := by rfl
+
 /--
 Return whether a configuration file with the given name
 and/or a supported extension exists.
@@ -49,21 +84,25 @@ public def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
       resolvePath (cfgFile.addExtension "toml")
 
 /--
-Loads a Lake package configuration (either Lean or TOML).
-The resulting package does not yet include any dependencies.
+**For internal use only.**
+
+Resolves a relative configuration file path in {lean}`cfg` and
+detects its configuration language (if necessary).
 -/
-public def loadPackageCore
+public def resolveConfigFile
   (name : String) (cfg : LoadConfig)
-: LogIO (Package × Option Environment) := do
-  if let some ext := cfg.relConfigFile.extension then
-    let cfg ←
-      if let some configFile ← resolvePath? cfg.configFile then
-        pure {cfg with configFile}
-      else error s!"{name}: configuration file not found: {cfg.configFile}"
+: LogIO {cfg : LoadConfig // cfg.configLang?.isSome} := do
+  if h : cfg.configLang?.isSome then
+    let some configFile ← resolvePath? cfg.configFile
+      | error s!"{name}: configuration file not found: {cfg.configFile}"
+    return ⟨{cfg with configFile}, h⟩
+  else if let some ext := cfg.relConfigFile.extension then
+    let some configFile ← resolvePath? cfg.configFile
+      | error s!"{name}: configuration file not found: {cfg.configFile}"
     match ext with
-    | "lean" => (·.map id some) <$> loadLeanConfig cfg
-    | "toml" => ((·,none)) <$> loadTomlConfig cfg
-    | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}"
+    | "lean" => return ⟨{cfg with configFile, configLang? := some .lean}, rfl⟩
+    | "toml" => return ⟨{cfg with configFile, configLang? := some .toml}, rfl⟩
+    | _ => error s!"{name}: configuration has unsupported file extension: {configFile}"
   else
     let relLeanFile := cfg.relConfigFile.addExtension "lean"
     let relTomlFile := cfg.relConfigFile.addExtension "toml"
@@ -72,18 +111,28 @@ public def loadPackageCore
     if let some configFile ← resolvePath? leanFile then
       if (← tomlFile.pathExists) then
         logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
-       let cfg := {cfg with configFile, relConfigFile := relLeanFile}
-      let (pkg, env) ← loadLeanConfig cfg
-      return (pkg, some env)
+      return ⟨{cfg with configFile, relConfigFile := relLeanFile, configLang? := some .lean}, rfl⟩
+    else if let some configFile ← resolvePath? tomlFile then
+      return ⟨{cfg with configFile, relConfigFile := relTomlFile, configLang? := some .toml}, rfl⟩
     else
-      if let some configFile ← resolvePath? tomlFile then
-        let cfg := {cfg with configFile, relConfigFile := relTomlFile}
-        let pkg ← loadTomlConfig cfg
-        return (pkg, none)
-      else
-        error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
+      error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
+
+/--
+**For internal use only.**
+Reads the configuration of a Lake configuration file.
+
+The load configuration {lean}`cfg` is assumed to already have an absolute path in
+{lean}`cfg.configFile` and that the proper configuratin langauge for it is in
+{lean}`cfg.configLang?`. This can be ensured through {lean}`resolveConfigFile`.
+-/
+public def loadConfigFile (cfg : LoadConfig) (h : cfg.configLang?.isSome) : LogIO LakefileConfig := do
+  match cfg.configLang?.get h with
+  | .lean => loadLeanConfig cfg
+  | .toml => loadTomlConfig cfg
 
 /-- Loads a Lake package as a single independent object (without dependencies). -/
-public def loadPackage (config : LoadConfig) : LogIO Package := do
-  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
-  (·.1) <$> loadPackageCore "[root]" config
+public def loadPackage (cfg : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
+  let ⟨cfg, h⟩ ← resolveConfigFile "[root]" cfg
+  let fileCfg ← loadConfigFile cfg h
+  return mkPackage cfg fileCfg

src/lake/Lake/Load/Resolve.lean

@@ -25,37 +25,43 @@ This module contains definitions for resolving the dependencies of a package.
 
 namespace Lake
 
+/-- Returns the load configuration of a materialized dependency. -/
+@[inline] def mkDepLoadConfig
+  (ws : Workspace) (dep : MaterializedDep)
+  (lakeOpts : NameMap String) (leanOpts : Options) (reconfigure : Bool)
+: LoadConfig where
+  lakeEnv := ws.lakeEnv
+  wsDir := ws.dir
+  pkgIdx := ws.packages.size
+  pkgName := dep.name
+  pkgDir := dep.pkgDir
+  relPkgDir := dep.relPkgDir
+  relConfigFile := dep.relConfigFile
+  relManifestFile := dep.relManifestFile
+  lakeOpts; leanOpts; reconfigure
+  scope := dep.scope
+  remoteUrl := dep.remoteUrl
+
+def Workspace.addFacetDecls (decls : Array FacetDecl) (self : Workspace) : Workspace :=
+  decls.foldl (·.addFacetConfig ·.config) self
+
 /--
 Loads the package configuration of a materialized dependency.
-Adds the facets defined in the package to the `Workspace`.
+Adds the package and the facets defined within it to the `Workspace`.
 -/
-def loadDepPackage
-  (wsIdx : Nat)
+def addDepPackage
   (dep : MaterializedDep)
   (lakeOpts : NameMap String)
   (leanOpts : Options) (reconfigure : Bool)
 : StateT Workspace LogIO Package := fun ws => do
-  let name := dep.name.toString (escape := false)
-  let pkgDir := ws.dir / dep.relPkgDir
-  let some pkgDir ← resolvePath? pkgDir
-    | error s!"{name}: package directory not found: {pkgDir}"
-  let (pkg, env?) ← loadPackageCore name {
-    lakeEnv := ws.lakeEnv
-    wsDir := ws.dir
-    pkgIdx := wsIdx
-    pkgName := dep.name
-    pkgDir
-    relPkgDir := dep.relPkgDir
-    relConfigFile := dep.configFile
-    lakeOpts, leanOpts, reconfigure
-    scope := dep.scope
-    remoteUrl := dep.remoteUrl
-  }
-  if let some env := env? then
-    let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts
-    return (pkg, ws)
-  else
-    return (pkg, ws)
+  let wsIdx := ws.packages.size
+  let loadCfg := mkDepLoadConfig ws dep lakeOpts leanOpts reconfigure
+  let ⟨loadCfg, h⟩ ← resolveConfigFile dep.prettyName loadCfg
+  let fileCfg ← loadConfigFile loadCfg h
+  let pkg := mkPackage loadCfg fileCfg wsIdx
+  let ws := ws.addPackage' pkg wsIdx_mkPackage
+  let ws := ws.addFacetDecls fileCfg.facetDecls
+  return (pkg, ws)
 
 /--
 The resolver's call stack of dependencies.
@@ -100,7 +106,7 @@ abbrev ResolveT m := DepStackT <| StateT Workspace m
 /-
 Recursively visits each node in a package's dependency graph, starting from
 the workspace package `root`. Each dependency missing from the workspace is
-resolved using the `load` function and added into the workspace.
+added to the workspace using the `resolve` function.
 
 Recursion occurs breadth-first. Each direct dependency of a package is
 resolved in reverse order before recursing to the dependencies' dependencies.
@@ -108,9 +114,10 @@ resolved in reverse order before recursing to the dependencies' dependencies.
 See `Workspace.updateAndMaterializeCore` for more details.
 -/
 @[inline] private def Workspace.resolveDepsCore
-  [Monad m] [MonadError m] (ws : Workspace)
-  (load : Package → Dependency → Nat → StateT Workspace m Package)
+  [Monad m] [MonadError m] [MonadLiftT LogIO m] (ws : Workspace)
+  (resolve : Package → Dependency → Workspace → m MaterializedDep)
   (root : Package := ws.root) (stack : DepStack := {})
+  (leanOpts : Options := {}) (reconfigure := true)
 : m Workspace := do
   ws.runResolveT go root stack
 where
@@ -123,8 +130,8 @@ where
         return -- already handled in another branch
       if pkg.baseName = dep.name then
         error s!"{pkg.prettyName}: package requires itself (or a package with the same name)"
-      let depPkg ← load pkg dep ws.packages.size
-      modifyThe Workspace (·.addPackage depPkg)
+      let matDep ← resolve pkg dep (← getWorkspace)
+      discard <| addDepPackage matDep dep.opts leanOpts reconfigure
     -- Recursively load the dependencies' dependencies
     (← getWorkspace).packages.forM recurse start
 
@@ -171,17 +178,17 @@ private def reuseManifest
     logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
 
 /-- Add a package dependency's manifest entries to the update state. -/
-private def addDependencyEntries (pkg : Package) (matDep : MaterializedDep) : UpdateT LoggerIO PUnit := do
-  match matDep.manifest? with
+private def addDependencyEntries (dep : MaterializedDep) : UpdateT LoggerIO PUnit := do
+  match (← Manifest.load dep.manifestFile |>.toBaseIO) with
   | .ok manifest =>
     manifest.packages.forM fun entry => do
       unless (← getThe (NameMap PackageEntry)).contains entry.name do
-        let entry := entry.setInherited.inDirectory pkg.relDir
+        let entry := entry.setInherited.inDirectory dep.relPkgDir
         store entry.name entry
   | .error (.noFileOrDirectory ..) =>
-    logWarning s!"{pkg.prettyName}: ignoring missing manifest '{pkg.manifestFile}'"
+    logWarning s!"{dep.prettyName}: ignoring missing manifest:\n  {dep.manifestFile}"
   | .error e =>
-    logWarning s!"{pkg.prettyName}: ignoring manifest because it failed to load: {e}"
+    logWarning s!"{dep.prettyName}: ignoring manifest because it failed to load: {e}"
 
 /-- Materialize a single dependency, updating it if desired. -/
 private def updateAndMaterializeDep
@@ -356,7 +363,6 @@ def Workspace.updateAndMaterializeCore
   (updateToolchain := true)
 : LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do
   reuseManifest ws toUpdate
-  let ws := ws.addPackage ws.root
   if updateToolchain then
     let deps := ws.root.depConfigs.reverse
     let matDeps ← deps.mapM fun dep => do
@@ -365,21 +371,18 @@ def Workspace.updateAndMaterializeCore
     ws.updateToolchain matDeps
     let start := ws.packages.size
     let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
-      let (depPkg, ws) ← loadUpdatedDep ws.packages.size dep matDep ws
-      let ws := ws.addPackage depPkg
+      addDependencyEntries matDep
+      let (_, ws) ← addDepPackage matDep dep.opts leanOpts true ws
       return ws
     ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
-      ws.resolveDepsCore (stack := [ws.root.baseName]) updateAndLoadDep pkg
+      ws.resolveDepsCore updateAndAddDep pkg [ws.root.baseName] leanOpts true
   else
-    ws.resolveDepsCore updateAndLoadDep
+    ws.resolveDepsCore updateAndAddDep (leanOpts := leanOpts) (reconfigure := true)
 where
-  @[inline] updateAndLoadDep pkg dep wsIdx := do
-    let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep
-    loadUpdatedDep wsIdx dep matDep
-  @[inline] loadUpdatedDep wsIdx dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
-    let depPkg ← loadDepPackage wsIdx matDep dep.opts leanOpts true
-    addDependencyEntries depPkg matDep
-    return depPkg
+  @[inline] updateAndAddDep pkg dep ws := do
+    let matDep ← updateAndMaterializeDep ws pkg dep
+    addDependencyEntries matDep
+    return matDep
 
 /-- Write package entries to the workspace manifest. -/
 def Workspace.writeManifest
@@ -471,12 +474,9 @@ public def Workspace.materializeDeps
   if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
     error "missing manifest; use `lake update` to generate one"
   -- Materialize all dependencies
-  let ws := ws.addPackage ws.root
-  ws.resolveDepsCore fun pkg dep wsIdx => do
-    let ws ← getWorkspace
+  ws.resolveDepsCore (leanOpts := leanOpts) (reconfigure := reconfigure) fun pkg dep ws => do
     if let some entry := pkgEntries.find? dep.name then
-      let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir
-      loadDepPackage wsIdx result dep.opts leanOpts reconfigure
+      entry.materialize ws.lakeEnv ws.dir relPkgsDir
     else
       if pkg.isRoot then
         error <|

src/lake/Lake/Load/Toml.lean

@@ -7,10 +7,12 @@ module
 
 prelude
 public import Lake.Config.Package
+public import Lake.Config.LakefileConfig
 public import Lake.Load.Config
 public import Lake.Toml.Decode
 import Lake.Toml.Load
 import Lean.Parser.Extension
+import Lake.Build.Infos
 import Init.Omega
 meta import Lake.Config.LakeConfig
 meta import Lake.Config.InputFileConfig
@@ -431,7 +433,8 @@ private def decodeTargetDecls
   return (r.decls, r.map)
 where
   go (r : DecodeTargetState pkg) kw kind
-      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
+      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n))
+      (h : DataType kind = OpaqueConfigTarget kind := by simp) := do
     let some tableArrayVal := t.find? kw | return r
     let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
     vals.foldlM (init := r) fun r val => do
@@ -446,8 +449,10 @@ where
       else
         let config ← @decode name t
         let decl : NConfigDecl pkg name :=
-          -- Safety: By definition, config kind = facet kind for declarative configurations.
-          unsafe {pkg, name, kind, config, wf_data := lcProof}
+          -- Safety: By definition, for declarative configurations, the type of a package target
+          -- is its configuration's data kind (i.e., `CustomData pkg name = DataType kind`).
+          -- In the equivalent Lean configuration, this would hold by type family axiom.
+          unsafe {pkg, name, kind, config, wf_data := fun _ => ⟨lcProof, h⟩}
         -- Check that executables have distinct root module names
         let exeRoots ← id do
           if h : kind = LeanExe.configKind then
@@ -469,8 +474,8 @@ where
 
 /-! ## Root Loader -/
 
-/-- Load a `Package` from a Lake configuration file written in TOML. -/
-public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
+/-- Load a Lake configuration from a file written in TOML. -/
+public def loadTomlConfig (cfg : LoadConfig) : LogIO LakefileConfig := do
   let input ← IO.FS.readFile cfg.configFile
   let ictx := mkInputContext input cfg.relConfigFile.toString
   match (← loadToml ictx |>.toBaseIO) with
@@ -482,21 +487,12 @@ public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
       let keyName := baseName.num wsIdx
       let prettyName := baseName.toString (escape := false)
       let config ← @PackageConfig.decodeToml keyName origName table
+      let pkgDecl := {baseName, keyName, origName, config : PackageDecl}
       let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName prettyName table
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]
-      return {
-        wsIdx, baseName, keyName, origName
-        dir := cfg.pkgDir
-        relDir := cfg.relPkgDir
-        configFile := cfg.configFile
-        relConfigFile := cfg.relConfigFile
-        scope := cfg.scope
-        remoteUrl := cfg.remoteUrl
-        config, depConfigs, targetDecls, targetDeclMap
-        defaultTargets
-      }
+      return {pkgDecl, depConfigs, targetDecls, targetDeclMap, defaultTargets}
     if errs.isEmpty then
       return pkg
     else

src/lake/Lake/Load/Workspace.lean

@@ -31,18 +31,21 @@ Does not resolve dependencies.
 public def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.lakeEnv.leanSearchPath
   let lakeConfig ← loadLakeConfig config.lakeEnv
-  let (root, env?) ← loadPackageCore "[root]" {config with pkgIdx := 0}
+  let config := {config with pkgIdx := 0}
+  let ⟨config, h⟩ ← resolveConfigFile "[root]" config
+  let fileCfg ← loadConfigFile config h
+  let root := mkPackage config fileCfg 0
+  let facetConfigs := fileCfg.facetDecls.foldl (·.insert ·.config) initFacetConfigs
   let ws : Workspace := {
     root
     lakeEnv := config.lakeEnv
     lakeConfig
     lakeArgs? := config.lakeArgs?
-    facetConfigs := initFacetConfigs
+    facetConfigs
+    packages_wsIdx h := by simp at h
   }
-  if let some env := env? then
-    IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts
-  else
-    return ws
+  let ws := ws.addPackage' root wsIdx_mkPackage
+  return ws
 
 /--
 Load a `Workspace` for a Lake package by