diff --git a/RELEASES.md b/RELEASES.md
index ee24504c39f8..4b87eb193918 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -13,6 +13,8 @@ v4.4.0 (development in progress)
 
 * By default, `simp` will no longer try to use Decidable instances to rewrite terms. In particular, not all decidable goals will be closed by `simp`, and the `decide` tactic may be useful in such cases. The `decide` simp configuration option can be used to locally restore the old `simp` behavior, as in `simp (config := {decide := true})`; this includes using Decidable instances to verify side goals such as numeric inequalities.
 * **Lake:** Moved the default build directory (e.g., `build`), default packages directory (e.g., `lake-packages`), and the compiled configuration (e.g., `lakefile.olean`) into a new dedicated directory for Lake outputs, `.lake`. The cloud release build archives are also stored here, fixing [#2713](https://github.com/leanprover/lean4/issues/2713).
+* **Lake:** Update manifest format to version 7 (see [lean4#2801](https://github.com/leanprover/lean4/pull/2801) for details on the changes).
+* **Lake:** Deprecate the `manifestFile` field of a package configuration.
 
 v4.3.0
 ---------
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 2855ee2484ee..20e2c2911a60 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -12,6 +12,7 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 import Lake.Util.DRBMap
 import Lake.Util.OrdHashSet
+import Lake.Load.Config
 
 open System Lean
 
@@ -51,9 +52,6 @@ def stringToLegalOrSimpleName (s : String) : Name :=
 /-! # Defaults -/
 --------------------------------------------------------------------------------
 
-/-- The default setting for a `PackageConfig`'s `manifestFile` option. -/
-def defaultManifestFile := "lake-manifest.json"
-
 /-- The default setting for a `PackageConfig`'s `buildDir` option. -/
 def defaultBuildDir : FilePath := "build"
 
@@ -80,12 +78,14 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   name : Name
 
   /--
+  **This field is deprecated.**
+
   The path of a package's manifest file, which stores the exact versions
   of its resolved dependencies.
 
   Defaults to `defaultManifestFile` (i.e., `lake-manifest.json`).
   -/
-  manifestFile := defaultManifestFile
+  manifestFile : Option FilePath := none
 
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
@@ -178,12 +178,18 @@ declare_opaque_type OpaquePostUpdateHook (pkg : Name)
 structure Package where
   /-- The path to the package's directory. -/
   dir : FilePath
+  /-- The path to the package's directory relative to the workspace. -/
+  relDir : FilePath
   /-- The package's user-defined configuration. -/
   config : PackageConfig
   /-- The elaboration environment of the package's configuration file. -/
   configEnv : Environment
   /-- The Lean `Options` the package configuration was elaborated with. -/
   leanOpts : Options
+  /-- The path to the package's configuration file. -/
+  configFile : FilePath
+  /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
+  relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile
   /-- The URL to this package's Git remote. -/
   remoteUrl? : Option String := none
   /-- (Opaque references to) the package's direct dependencies. -/
@@ -280,9 +286,9 @@ namespace Package
 @[inline] def pkgsDir (self : Package) : FilePath :=
   self.dir / self.relPkgsDir
 
-/-- The package's JSON manifest of remote dependencies. -/
+/-- The path to the package's JSON manifest of remote dependencies. -/
 @[inline] def manifestFile (self : Package) : FilePath :=
-  self.dir / self.config.manifestFile
+  self.dir / self.relManifestFile
 
 /-- The package's `dir` joined with its `buildDir` configuration. -/
 @[inline] def buildDir (self : Package) : FilePath :=
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index c049e8cda8b8..27dd34bd2eee 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -17,6 +17,9 @@ def toolchainFileName : FilePath := "lean-toolchain"
 /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
 def defaultConfigFile : FilePath := "lakefile.lean"
 
+/-- The default name of the Lake manifest file (i.e., `lake-manifest.json`). -/
+def defaultManifestFile := "lake-manifest.json"
+
 /-- Context for loading a Lake configuration. -/
 structure LoadConfig where
   /-- The Lake environment of the load process. -/
diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index 2665eaed7932..a92c61cba072 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -30,14 +30,17 @@ def loadDepsFromEnv (env : Environment) (opts : Options) : Except String (Array
 Elaborate a dependency's configuration file into a `Package`.
 The resulting package does not yet include any dependencies.
 -/
-def MaterializedDep.loadPackage (dep : MaterializedDep) (wsDir : FilePath)
-(leanOpts : Options) (lakeOpts : NameMap String) (reconfigure : Bool) : LogIO Package := do
+def MaterializedDep.loadPackage (dep : MaterializedDep)
+(wsDir : FilePath) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
   let lakeDir := dir / defaultLakeDir
-  let configEnv ← importConfigFile wsDir dir lakeDir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
+  let configEnv ← importConfigFile wsDir dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
-    dir, config, configEnv, leanOpts
+    dir
+    relDir := dep.relPkgDir
+    config, configEnv, leanOpts
+    configFile := dep.configFile
     remoteUrl? := dep.remoteUrl?
   }
 
@@ -52,8 +55,12 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let root := {
-    configEnv, leanOpts := config.leanOpts
-    dir := config.rootDir, config := pkgConfig
+    dir := config.rootDir
+    relDir := "."
+    config := pkgConfig
+    configEnv
+    leanOpts := config.leanOpts
+    configFile := config.configFile
   }
   return {
     root, lakeEnv := config.env
@@ -98,49 +105,59 @@ If `reconfigure`, elaborate configuration files while updating, do not use OLean
 -/
 def Workspace.updateAndMaterialize (ws : Workspace)
 (toUpdate : NameSet := {}) (reconfigure := true) : LogIO Workspace := do
-  let res ← StateT.run (s := mkNameMap MaterializedDep) <| EStateT.run' (mkNameMap Package) do
+  let res ← StateT.run (s := mkNameMap MaterializedDep) <|
+    StateT.run' (s := mkNameMap PackageEntry) <| EStateT.run' (mkNameMap Package) do
     -- Use manifest versions of root packages that should not be updated
-    unless toUpdate.isEmpty do
-      for entry in (← Manifest.loadOrEmpty ws.manifestFile) do
-        unless entry.inherited || toUpdate.contains entry.name do
-          let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
-          modifyThe (NameMap MaterializedDep) (·.insert entry.name dep)
-    buildAcyclic (·.1.name) (ws.root, FilePath.mk ".") fun (pkg, relPkgDir) resolve => do
+    if let some manifest ← liftM <| Manifest.load? ws.manifestFile then
+      unless toUpdate.isEmpty do
+        manifest.packages.forM fun entry => do
+          unless entry.inherited || toUpdate.contains entry.name do
+            modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
+      if let some oldRelPkgsDir := manifest.packagesDir? then
+        let oldPkgsDir := ws.dir / oldRelPkgsDir
+        if oldPkgsDir != ws.pkgsDir && (← oldPkgsDir.pathExists) then
+          liftM <| createParentDirs ws.pkgsDir
+          liftM <| IO.FS.rename oldPkgsDir ws.pkgsDir
+    buildAcyclic (·.name) ws.root fun pkg resolve => do
       let inherited := pkg.name != ws.root.name
-      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       -- Materialize this package's dependencies first
+      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
-        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir ws.lakeEnv.pkgUrlMap
+        if let some entry := (← getThe (NameMap PackageEntry)).find? dep.name then
+          entry.materialize dep ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
+        else
+          dep.materialize inherited ws.dir ws.relPkgsDir pkg.relDir ws.lakeEnv.pkgUrlMap
       -- Load dependency packages and materialize their locked dependencies
       let deps ← deps.mapM fun dep => do
-        if let .some pkg := (← getThe (NameMap Package)).find? dep.name then
-          return (pkg, dep.relPkgDir)
+        if let some pkg := (← getThe (NameMap Package)).find? dep.name then
+          return pkg
         else
           -- Load the package
-          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts dep.opts reconfigure
+          let depPkg ← dep.loadPackage ws.dir pkg.leanOpts reconfigure
           if depPkg.name ≠ dep.name then
             logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
           -- Materialize locked dependencies
-          for entry in (← Manifest.loadOrEmpty depPkg.manifestFile) do
-            unless (← getThe (NameMap MaterializedDep)).contains entry.name do
-              let entry := entry.setInherited.inDirectory dep.relPkgDir
-              let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
-              modifyThe (NameMap MaterializedDep) (·.insert entry.name dep)
+          if let some manifest ← liftM <| Manifest.load? depPkg.manifestFile then
+            manifest.packages.forM fun entry => do
+              unless (← getThe (NameMap PackageEntry)).contains entry.name do
+                let entry := entry.setInherited.inDirectory dep.relPkgDir
+                modifyThe (NameMap PackageEntry) (·.insert entry.name entry)
           modifyThe (NameMap Package) (·.insert dep.name depPkg)
-          return (depPkg, dep.relPkgDir)
+          return depPkg
       -- Resolve dependencies's dependencies recursively
       return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
   match res with
   | (.ok root, deps) =>
     let ws : Workspace ← {ws with root}.finalize
     let manifest : Manifest := {
-      name? := ws.root.name
-      lakeDir? := ws.relLakeDir
+      name := ws.root.name
+      lakeDir := ws.relLakeDir
       packagesDir? := ws.relPkgsDir
     }
     let manifest := ws.packages.foldl (init := manifest) fun manifest pkg =>
       match deps.find? pkg.name with
-      | some dep => manifest.addPackage dep.manifestEntry
+      | some dep => manifest.addPackage <|
+        dep.manifestEntry.setManifestFile pkg.relManifestFile
       | none => manifest -- should only be the case for the root
     manifest.saveToFile ws.manifestFile
     LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
@@ -157,7 +174,7 @@ Resolving a workspace's dependencies using a manifest,
 downloading and/or updating them as necessary.
 -/
 def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigure := false) : LogIO Workspace := do
-  if !manifest.isEmpty && manifest.packagesDir? != some ws.relPkgsDir then
+  if !manifest.packages.isEmpty && manifest.packagesDir? != some (normalizePath ws.relPkgsDir) then
     logWarning <|
       "manifest out of date: packages directory changed; " ++
       "use `lake update` to rebuild the manifest (warning: this will update ALL workspace dependencies)"
@@ -169,7 +186,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
       let topLevel := pkg.name = ws.root.name
       let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       if topLevel then
-        if manifest.isEmpty && !deps.isEmpty then
+        if manifest.packages.isEmpty && !deps.isEmpty then
           error "missing manifest; use `lake update` to generate one"
         for dep in deps do
           let warnOutOfDate (what : String) :=
@@ -185,10 +202,8 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
           | _, _ => warnOutOfDate "source kind (git/path)"
       let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
         if let some entry := pkgEntries.find? dep.name then
-          let result ← entry.materialize ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
-          -- Union manifest and configuration options (preferring manifest)
-          let opts := entry.opts.mergeBy (fun _ e _ => e) dep.opts
-          result.loadPackage ws.dir pkg.leanOpts opts reconfigure
+          let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
+          result.loadPackage ws.dir pkg.leanOpts reconfigure
         else if topLevel then
           error <|
             s!"dependency '{dep.name}' not in manifest; " ++
@@ -196,8 +211,8 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
         else
           error <|
             s!"dependency '{dep.name}' of '{pkg.name}' not in manifest; " ++
-            s!"this suggests that the manifest is corrupt;" ++
-            s!"use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)"
+            "this suggests that the manifest is corrupt;" ++
+            "use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)"
       return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}
   match res with
   | Except.ok root =>
diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean
index 8d9b6f1d3e51..4335b48605a1 100644
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@@ -5,6 +5,8 @@ Authors: Mac Malone, Gabriel Ebner
 -/
 import Lake.Util.Log
 import Lake.Util.Name
+import Lake.Load.Config
+import Lake.Config.Workspace
 
 open System Lean
 
@@ -16,67 +18,167 @@ to create, modify, serialize, and deserialize it.
 namespace Lake
 
 /-- Current version of the manifest format. -/
-def Manifest.version : Nat := 6
+def Manifest.version : Nat := 7
+
+/-- An entry for a package stored in the manifest. -/
+inductive PackageEntryV6
+| path (name : Name) (opts : NameMap String) (inherited : Bool) (dir : FilePath)
+| git (name : Name) (opts : NameMap String) (inherited : Bool) (url : String) (rev : String)
+    (inputRev? : Option String) (subDir? : Option FilePath)
+deriving FromJson, ToJson, Inhabited
+
+/-- Set `/` as the path separator, even on Windows. -/
+def normalizePath (path : FilePath) : FilePath :=
+  if System.Platform.isWindows then
+    path.toString.map fun c => if c = '\\' then '/' else c
+  else
+    path.toString
+
+/--
+Use `/` and instead of `\\` in file paths
+when serializing the manifest on Windows.
+-/
+local instance : ToJson FilePath where
+  toJson path := toJson <| normalizePath path
 
 /-- An entry for a package stored in the manifest. -/
 inductive PackageEntry
-| /--
+  /--
   A local filesystem package. `dir` is relative to the package directory
   of the package containing the manifest.
   -/
-  path (name : Name) (opts : NameMap String) (inherited : Bool) (dir : FilePath)
-| /-- A remote Git package. -/
-  git (name : Name) (opts : NameMap String) (inherited : Bool) (url : String) (rev : String)
-    (inputRev? : Option String) (subDir? : Option FilePath)
-deriving FromJson, ToJson, Inhabited
+  | path
+    (name : Name)
+    (inherited : Bool)
+    (configFile : FilePath)
+    (manifestFile? : Option FilePath)
+    (dir : FilePath)
+  /-- A remote Git package. -/
+  | git
+    (name : Name)
+    (inherited : Bool)
+    (configFile : FilePath)
+    (manifestFile? : Option FilePath)
+    (url : String)
+    (rev : String)
+    (inputRev? : Option String)
+    (subDir? : Option FilePath)
+  deriving Inhabited
 
 namespace PackageEntry
 
-@[inline] protected def name : PackageEntry → Name
-| .path name .. | .git name .. => name
+protected def toJson : PackageEntry → Json
+| .path name inherited configFile manifestFile? dir => Json.mkObj [
+  ("type", "path"),
+  ("inherited", toJson inherited),
+  ("name", toJson name),
+  ("configFile" , toJson configFile),
+  ("manifestFile", toJson manifestFile?),
+  ("inherited", toJson inherited),
+  ("dir", toJson dir)
+]
+| .git name inherited configFile manifestFile? url rev inputRev? subDir? => Json.mkObj [
+  ("type", "git"),
+  ("inherited", toJson inherited),
+  ("name", toJson name),
+  ("configFile" , toJson configFile),
+  ("manifestFile", toJson manifestFile?),
+  ("url", toJson url),
+  ("rev", toJson rev),
+  ("inputRev", toJson inputRev?),
+  ("subDir", toJson subDir?)
+]
+
+instance : ToJson PackageEntry := ⟨PackageEntry.toJson⟩
+
+protected def fromJson? (json : Json) : Except String PackageEntry := do
+  let obj ← json.getObj?
+  let type ← get obj "type"
+  let name ← get obj "name"
+  let inherited ← get obj "inherited"
+  let configFile ← getD obj "configFile" defaultConfigFile
+  let manifestFile ← getD obj "manifestFile" defaultManifestFile
+  match type with
+  | "path"=>
+    let dir ← get obj "dir"
+    return .path name inherited configFile manifestFile dir
+  | "git" =>
+    let url ← get obj "url"
+    let rev ← get obj "rev"
+    let inputRev? ← get? obj "inputRev"
+    let subDir? ← get? obj "subDir"
+    return .git name inherited configFile manifestFile url rev inputRev? subDir?
+  | _ =>
+    throw s!"unknown package entry type '{type}'"
+where
+  get {α} [FromJson α] obj prop : Except String α :=
+    match obj.find compare prop with
+    | none => throw s!"package entry missing required property '{prop}'"
+    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
+  get? {α} [FromJson α] obj prop : Except String (Option α) :=
+    match obj.find compare prop with
+    | none => pure none
+    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
+  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
+    (Option.getD · default) <$> get? obj prop
+
+instance : FromJson PackageEntry := ⟨PackageEntry.fromJson?⟩
 
-@[inline] protected def opts : PackageEntry → NameMap String
-| .path _ opts .. | .git _ opts .. => opts
+@[inline] protected def name : PackageEntry → Name
+| .path (name := name) .. | .git (name := name) .. => name
 
 @[inline] protected def inherited : PackageEntry → Bool
-| .path _ _ inherited .. | .git _ _ inherited .. => inherited
+| .path (inherited := inherited) .. | .git (inherited := inherited) .. => inherited
 
 def setInherited : PackageEntry → PackageEntry
-| .path name opts _ dir => .path name opts true dir
-| .git name opts _ url rev inputRev? subDir? => .git name opts true url rev inputRev? subDir?
+| .path name _ configFile manifestFile? dir =>
+  .path name true configFile manifestFile? dir
+| .git name _ configFile manifestFile? url rev inputRev? subDir? =>
+  .git name true configFile manifestFile? url rev inputRev? subDir?
+
+@[inline] protected def configFile : PackageEntry → FilePath
+| .path (configFile := configFile) .. | .git (configFile := configFile) .. => configFile
+
+@[inline] protected def manifestFile? : PackageEntry →  Option FilePath
+| .path (manifestFile? := manifestFile?) .. | .git (manifestFile? := manifestFile?) .. => manifestFile?
+
+def setManifestFile (path? : Option FilePath) : PackageEntry → PackageEntry
+| .path name inherited configFile _ dir =>
+  .path name inherited configFile path? dir
+| .git name inherited configFile _ url rev inputRev? subDir? =>
+  .git name inherited configFile path? url rev inputRev? subDir?
 
 def inDirectory (pkgDir : FilePath) : PackageEntry → PackageEntry
-| .path name opts inherited dir => .path name opts inherited (pkgDir / dir)
+| .path name inherited configFile manifestFile? dir =>
+  .path name inherited configFile manifestFile? (pkgDir / dir)
 | entry => entry
 
+def ofV6 : PackageEntryV6 → PackageEntry
+| .path name _opts inherited dir =>
+  .path name inherited defaultConfigFile none dir
+| .git name _opts inherited url rev inputRev? subDir? =>
+  .git name inherited defaultConfigFile none url rev inputRev? subDir?
+
 end PackageEntry
 
 /-- Manifest data structure that is serialized to the file. -/
 structure Manifest where
-  name? : Option Name := none
-  lakeDir? : Option FilePath := none
+  name : Name
+  lakeDir : FilePath
   packagesDir? : Option FilePath := none
   packages : Array PackageEntry := #[]
 
 namespace Manifest
 
-def empty : Manifest := {}
-
-@[inline] def isEmpty (self : Manifest) : Bool :=
-  self.packages.isEmpty
-
 /-- Add a package entry to the end of a manifest. -/
 def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
   {self with packages := self.packages.push entry}
 
-instance : ForIn m Manifest PackageEntry where
-  forIn self init f := self.packages.forIn init f
-
 protected def toJson (self : Manifest) : Json :=
   Json.mkObj [
     ("version", version),
-    ("name", toJson self.name?),
-    ("lakeDir", toJson self.lakeDir?),
+    ("name", toJson self.name),
+    ("lakeDir", toJson self.lakeDir),
     ("packagesDir", toJson self.packagesDir?),
     ("packages", toJson self.packages)
   ]
@@ -84,22 +186,40 @@ protected def toJson (self : Manifest) : Json :=
 instance : ToJson Manifest := ⟨Manifest.toJson⟩
 
 protected def fromJson? (json : Json) : Except String Manifest := do
-  let ver ← json.getObjVal? "version"
-  let .ok ver := ver.getNat? | throw s!"unknown manifest version `{ver}`"
+  let .ok obj := json.getObj?
+    | throw "manifest not a JSON object"
+  let ver : Json ← get obj "version"
+  let .ok ver := ver.getNat?
+    | throw s!"unknown manifest version `{ver}`"
   if ver < 5 then
     throw s!"incompatible manifest version `{ver}`"
   else if ver ≤ 6 then
-    let name? ← json.getObjValAs? _ "name"
-    let packagesDir? ← do
-      match json.getObjVal? "packagesDir" with
-      | .ok path => fromJson? path
-      | .error _ => pure none
-    let packages : Array PackageEntry ← fromJson? (← json.getObjVal? "packages")
-    return {name?, packagesDir?, packages}
+    let name ← getD obj "name" Name.anonymous
+    let lakeDir ← getD obj "lakeDir" defaultLakeDir
+    let packagesDir? ← get? obj "packagesDir"
+    let pkgs : Array PackageEntryV6 ← getD obj "packages" #[]
+    return {name, lakeDir, packagesDir?, packages := pkgs.map PackageEntry.ofV6}
+  else if ver = 7 then
+    let name ← getD obj "name" Name.anonymous
+    let lakeDir ← get obj "lakeDir"
+    let packagesDir ← get obj "packagesDir"
+    let packages : Array PackageEntry ← getD obj "packages" #[]
+    return {name, lakeDir, packagesDir? := packagesDir, packages}
   else
     throw <|
       s!"manifest version `{ver}` is higher than this Lake's '{Manifest.version}'; " ++
       "you may need to update your `lean-toolchain`"
+where
+  get {α} [FromJson α] obj prop : Except String α :=
+    match obj.find compare prop with
+    | none => throw s!"manifest missing required property '{prop}'"
+    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
+  get? {α} [FromJson α] obj prop : Except String (Option α) :=
+    match obj.find compare prop with
+    | none => pure none
+    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
+  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
+    (Option.getD · default) <$> get? obj prop
 
 instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 
@@ -125,19 +245,6 @@ def load? (file : FilePath) : IO (Option Manifest) := do
   | .error (.noFileOrDirectory ..) => pure none
   | .error e => throw e
 
-/--
- Parse the manifest file or return an empty one.
- Warn on any IO/parse errors if the file exists.
--/
-def loadOrEmpty (file : FilePath) : LogIO Manifest := do
-  match (← IO.FS.readFile file |>.toBaseIO) with
-  | .ok contents =>
-    match inline <| Manifest.parse contents with
-    | .ok a => return a
-    | .error e => logWarning s!"{file}: {e}"; pure {}
-  | .error (.noFileOrDirectory ..) => pure {}
-  | .error e => logWarning (toString e); pure {}
-
 /-- Save the manifest as JSON to a file. -/
 def saveToFile (self : Manifest) (manifestFile : FilePath) : IO PUnit := do
   let jsonString := Json.pretty self.toJson
diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean
index 53683168b51b..9ad1406a908f 100644
--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@@ -74,15 +74,31 @@ def materializeGitRepo (name : String) (repo : GitRepo)
 structure MaterializedDep where
   /-- Path to the materialized package relative to the workspace's root directory. -/
   relPkgDir : FilePath
+  /--
+  URL for the materialized package.
+  Used as the endpoint from which to fetch cloud releases for the package.
+  -/
   remoteUrl? : Option String
+  /-- The manifest entry for the dependency. -/
   manifestEntry : PackageEntry
+  /-- The configuration-specified dependency. -/
+  configDep : Dependency
   deriving Inhabited
 
 @[inline] def MaterializedDep.name (self : MaterializedDep) :=
   self.manifestEntry.name
 
-@[inline] def MaterializedDep.opts (self : MaterializedDep) :=
-  self.manifestEntry.opts
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] def MaterializedDep.manifestFile? (self : MaterializedDep) :=
+  self.manifestEntry.manifestFile?
+
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] def MaterializedDep.configFile (self : MaterializedDep) :=
+  self.manifestEntry.configFile
+
+ /-- Lake configuration options for the dependency. -/
+@[inline] def MaterializedDep.configOpts (self : MaterializedDep) :=
+  self.configDep.opts
 
 /--
 Materializes a configuration dependency.
@@ -97,7 +113,8 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := none
-      manifestEntry := .path dep.name dep.opts inherited relPkgDir
+      manifestEntry := .path dep.name inherited defaultConfigFile none relPkgDir
+      configDep := dep
     }
   | .git url inputRev? subDir? => do
     let sname := dep.name.toString (escape := false)
@@ -110,22 +127,25 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := Git.filterUrl? url
-      manifestEntry := .git dep.name dep.opts inherited url rev inputRev? subDir?
+      manifestEntry := .git dep.name inherited defaultConfigFile none url rev inputRev? subDir?
+      configDep := dep
     }
 
 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.
 -/
 def PackageEntry.materialize (manifestEntry : PackageEntry)
-(wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String) : LogIO MaterializedDep :=
+(configDep : Dependency) (wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String)
+: LogIO MaterializedDep :=
   match manifestEntry with
-  | .path _name _opts _inherited relPkgDir =>
+  | .path (dir := relPkgDir) .. =>
     return {
       relPkgDir
       remoteUrl? := none
       manifestEntry
+      configDep
     }
-  | .git name _opts _inherited url rev _inputRev? subDir? => do
+  | .git name (url := url) (rev := rev) (subDir? := subDir?) .. => do
     let sname := name.toString (escape := false)
     let relGitDir := relPkgsDir / sname
     let gitDir := wsDir / relGitDir
@@ -151,4 +171,5 @@ def PackageEntry.materialize (manifestEntry : PackageEntry)
       relPkgDir
       remoteUrl? := Git.filterUrl? url
       manifestEntry
+      configDep
     }
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index ccd0d85da8c0..52d75cfc235d 100644
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -107,6 +107,10 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
         error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`"
     | .error e => error e
 
+  -- Deprecation warnings
+  unless self.config.manifestFile.isNone do
+    logWarning s!"{self.name}: package configuration option `manifestFile` is deprecated"
+
   -- Fill in the Package
   return {self with
     opaqueDeps := deps.map (.mk ·)
diff --git a/src/lake/README.md b/src/lake/README.md
index f51078393f4f..04ec9d9814f3 100644
--- a/src/lake/README.md
+++ b/src/lake/README.md
@@ -154,7 +154,6 @@ Lake provides a large assortment of configuration options for packages.
 ### Layout
 
 * `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `.lake/packages`.
-* `manifestFile`: The path of a package's manifest file, which stores the exact versions of its resolved dependencies. Defaults to `lake-manifest.json`.
 * `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`.
 * `leanLibDir`: The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., `.olean`, `.ilean` files). Defaults to `lib`.
diff --git a/src/lake/tests/manifest/bar/lakefile.lean b/src/lake/tests/manifest/bar/lakefile.lean
new file mode 100644
index 000000000000..2b2488da9557
--- /dev/null
+++ b/src/lake/tests/manifest/bar/lakefile.lean
@@ -0,0 +1,3 @@
+import Lake
+open Lake DSL
+package bar
diff --git a/src/lake/tests/manifest/clean.sh b/src/lake/tests/manifest/clean.sh
new file mode 100755
index 000000000000..e22e74298b1b
--- /dev/null
+++ b/src/lake/tests/manifest/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake foo/.lake bar/.git lake-packages lake-manifest.json
diff --git a/src/lake/tests/manifest/foo/lakefile.lean b/src/lake/tests/manifest/foo/lakefile.lean
new file mode 100644
index 000000000000..d868010b142f
--- /dev/null
+++ b/src/lake/tests/manifest/foo/lakefile.lean
@@ -0,0 +1,3 @@
+import Lake
+open Lake DSL
+package foo
diff --git a/src/lake/tests/manifest/lake-manifest-v5.json b/src/lake/tests/manifest/lake-manifest-v5.json
new file mode 100644
index 000000000000..bb70411f54c0
--- /dev/null
+++ b/src/lake/tests/manifest/lake-manifest-v5.json
@@ -0,0 +1,12 @@
+{"version": 5,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "bar",
+    "subDir?": null,
+    "rev": "253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f",
+    "opts": {},
+    "name": "bar",
+    "inputRev?": null,
+    "inherited": false}},
+  {"path": {"opts": {}, "name": "foo", "inherited": false, "dir": "./foo"}}]}
diff --git a/src/lake/tests/manifest/lake-manifest-v6.json b/src/lake/tests/manifest/lake-manifest-v6.json
new file mode 100644
index 000000000000..93ad2cb1ab44
--- /dev/null
+++ b/src/lake/tests/manifest/lake-manifest-v6.json
@@ -0,0 +1,13 @@
+{"version": 6,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"path": {"opts": {}, "name": "foo", "inherited": false, "dir": "./foo"}},
+  {"git":
+   {"url": "bar",
+    "subDir?": null,
+    "rev": "dab525a78710d185f3d23622b143bdd837e44ab0",
+    "opts": {},
+    "name": "bar",
+    "inputRev?": null,
+    "inherited": false}}],
+ "name": "test"}
diff --git a/src/lake/tests/manifest/lake-manifest-v7.json b/src/lake/tests/manifest/lake-manifest-v7.json
new file mode 100644
index 000000000000..18649a77bb73
--- /dev/null
+++ b/src/lake/tests/manifest/lake-manifest-v7.json
@@ -0,0 +1,20 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./foo",
+   "configFile": "lakefile.lean"},
+  {"url": "bar",
+   "type": "git",
+   "subDir": null,
+   "rev": "0538596b94a0510f55dc820cabd3bde41ad93c3e",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "test",
+ "lakeDir": ".lake"}
diff --git a/src/lake/tests/manifest/lakefile.lean b/src/lake/tests/manifest/lakefile.lean
new file mode 100644
index 000000000000..345340cf305d
--- /dev/null
+++ b/src/lake/tests/manifest/lakefile.lean
@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+require foo from "foo"
+require bar from git "bar"
diff --git a/src/lake/tests/manifest/test.sh b/src/lake/tests/manifest/test.sh
new file mode 100755
index 000000000000..02282fe28ed8
--- /dev/null
+++ b/src/lake/tests/manifest/test.sh
@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+set -exo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+if [ "`uname`" = Darwin ]; then
+  sed_i() { sed -i '' "$@"; }
+else
+  sed_i() { sed -i "$@"; }
+fi
+
+./clean.sh
+
+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the bar repository on each test. This requires updating the
+# locked manifest to the new hash to ensure things work properly.
+pushd bar
+git init
+git checkout -b master
+git config user.name test
+git config user.email test@example.com
+git add --all
+git commit -m "initial commit"
+REV=`git rev-parse HEAD`
+popd
+
+# ---
+# Test manifest properly upgrades from supported versions
+# ---
+
+# Test successful loading of a V5 manifest
+cp lake-manifest-v5.json lake-manifest.json
+sed_i "s/253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f/$REV/g" lake-manifest.json
+$LAKE resolve-deps
+
+# Test update produces the expected V7 manifest
+$LAKE update
+sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
+diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+
+# Test successful loading of a V6 manifest
+cp lake-manifest-v6.json lake-manifest.json
+sed_i "s/dab525a78710d185f3d23622b143bdd837e44ab0/$REV/g" lake-manifest.json
+$LAKE resolve-deps
+
+# Test update produces the expected V7 manifest
+$LAKE update
+sed_i "s/$REV/0538596b94a0510f55dc820cabd3bde41ad93c3e/g" lake-manifest.json
+diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json