From 15a6401f4ba7c5fda2ec28d7c8aa4f657b5c4f61 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 5 Aug 2022 17:31:04 -0400
Subject: [PATCH] feat: make manifest file configurable

see #111
---
 Lake/CLI/Init.lean       |  2 +-
 Lake/Config/Package.lean | 14 ++++++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean
index 2cb9f79..763f6cb 100644
--- a/Lake/CLI/Init.lean
+++ b/Lake/CLI/Init.lean
@@ -22,7 +22,7 @@ def toolchainFileName : FilePath :=
 def gitignoreContents :=
 s!"/{defaultBuildDir}
 /{defaultPackagesDir}/*
-!/{defaultPackagesDir}/{manifestFileName}
+!/{defaultPackagesDir}/{defaultManifestFileName}
 "
 
 def libFileContents :=
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 76151b8..b45dfb5 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -16,9 +16,6 @@ open Std System Lean
 
 namespace Lake
 
-/-- The file name of a workspace's package manifest (i.e., `manifest.json`). -/
-def manifestFileName := "manifest.json"
-
 /-- A string descriptor of the `System.Platform` OS (`windows`, `macOS`, or `linux`). -/
 def osDescriptor : String :=
   if Platform.isWindows then
@@ -45,6 +42,9 @@ def nameToArchive (name? : Option String) : String :=
 /-! # Defaults -/
 --------------------------------------------------------------------------------
 
+/-- The default name of the package manifest. -/
+def defaultManifestFileName := "manifest.json"
+
 /-- The default setting for a `PackageConfig`'s `buildDir` option. -/
 def defaultBuildDir : FilePath := "build"
 
@@ -70,6 +70,12 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   /-- The `Name` of the package. -/
   name : Name
 
+  /--
+  The path of a package's manifest file
+  Defaults to `packagesDir` / `defaultManifestFileName` (i.e., `manifest.json`).
+  -/
+  manifestFile := packagesDir / defaultManifestFileName
+
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
 
@@ -221,7 +227,7 @@ def packagesDir (self : Package) : FilePath :=
 
 /-- The package's JSON manifest of remote dependencies. -/
 def manifestFile (self : Package) : FilePath :=
-  self.dir / self.config.packagesDir / manifestFileName
+  self.dir / self.config.manifestFile
 
 /-- The package's `dir` joined with its `buildDir` configuration. -/
 @[inline] def buildDir (self : Package) : FilePath :=