chore: deprecate Lake.PackageConfig.manifestFile

src/lake/Lake/Config/Package.lean

@@ -78,6 +78,8 @@ 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.
 

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 ·)

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`.