Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Commit

Permalink
feat: make manifest file configurable
Browse files Browse the repository at this point in the history
see #111
  • Loading branch information
tydeu committed Aug 5, 2022
1 parent 35873c6 commit 15a6401
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 5 deletions.
2 changes: 1 addition & 1 deletion Lake/CLI/Init.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ def toolchainFileName : FilePath :=
def gitignoreContents :=
s!"/{defaultBuildDir}
/{defaultPackagesDir}/*
!/{defaultPackagesDir}/{manifestFileName}
!/{defaultPackagesDir}/{defaultManifestFileName}
"

def libFileContents :=
Expand Down
14 changes: 10 additions & 4 deletions Lake/Config/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"

Expand All @@ -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 := #[]

Expand Down Expand Up @@ -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 :=
Expand Down

0 comments on commit 15a6401

Please sign in to comment.