From 712d3c2292151668a57fc6be2ab06ab4df7c2d4e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 2 Nov 2023 16:34:41 -0400
Subject: [PATCH] chore: deprecate `Lake.PackageConfig.manifestFile`

---
 src/lake/Lake/Config/Package.lean | 2 ++
 src/lake/Lake/Load/Package.lean   | 4 ++++
 src/lake/README.md                | 1 -
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index ea89de42f4..20e2c2911a 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/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.
 
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index ccd0d85da8..52d75cfc23 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 f51078393f..04ec9d9814 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`.