diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index ea89de42f4fc..20e2c2911a60 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 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`.