diff --git a/Lake/Glob.lean b/Lake/Glob.lean index 5450fb4e56..61e3a86ef8 100644 --- a/Lake/Glob.lean +++ b/Lake/Glob.lean @@ -16,7 +16,7 @@ inductive Glob one : Name → Glob | /-- Selects all submodules of the specified module, - without building the module itself. + but not the module itself. -/ submodules : Name → Glob | /-- Selects the specified module and all submodules. -/ diff --git a/Lake/Package.lean b/Lake/Package.lean index 2ab2406067..7a5b2e1841 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -101,25 +101,13 @@ structure PackageConfig where -/ version : String - /- - The root module(s) of the package's library. - - Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered - part of the package. - - Defaults to a single root of the package's uppercase `name`. - -/ - libRoots : Array Name := #[name.capitalize] - /-- - An `Array` of additional module `Glob`s to include in the package. - Defaults to singular globs of the module's `libRoots`. + A `HashMap` of scripts for the package. - Submodule globs build every source file within their directory. - Local imports of said files (i.e., fellow modules of the package) are - also recursively built. + A `Script` is an arbitrary `(args : List String) → IO PUnit` function that + is indexed by a `String` key and can be be run by `lake run [-- ]`. -/ - libGlobs : Array Glob := libRoots.map Glob.one + scripts : HashMap String Script := HashMap.empty /- A `List` of the package's dependencies. @@ -141,11 +129,6 @@ structure PackageConfig where -/ extraDepTarget : OpaqueTarget := Target.nil - /-- - Additional arguments to pass to `lean` while compiling Lean source files. - -/ - leanArgs : Array String := #[] - /-- The directory containing the package's Lean source files. Defaults to the package's directory. @@ -166,13 +149,30 @@ structure PackageConfig where -/ oleanDir : FilePath := defaultOleanDir - /-- - A `HashMap` of scripts for the package. + /- + The root module(s) of the package's library. - A `Script` is an arbitrary `(args : List String) → IO PUnit` function that - is indexed by a `String` key and can be be run by `lake run [-- ]`. + Submodules of these roots (e.g., `Pkg.Foo` of `Pkg`) are considered + part of the package. + + Defaults to a single root of the package's uppercase `name`. -/ - scripts : HashMap String Script := HashMap.empty + libRoots : Array Name := #[name.capitalize] + + /-- + An `Array` of additional module `Glob`s to include in the package. + Defaults to singular globs of the module's `libRoots`. + + Submodule globs build every source file within their directory. + Local imports of said files (i.e., fellow modules of the package) are + also recursively built. + -/ + libGlobs : Array Glob := libRoots.map Glob.one + + /-- + Additional arguments to pass to `lean` while compiling Lean source files. + -/ + leanArgs : Array String := #[] /-- Additional arguments to pass to `leanc` @@ -280,6 +280,50 @@ def version (self : Package) : String := def scripts (self : Package) : HashMap String Script := self.config.scripts +/-- The package's `dependencies` configuration. -/ +def dependencies (self : Package) : List Dependency := + self.config.dependencies + +/-- The package's `extraDepTarget` configuration. -/ +def extraDepTarget (self : Package) : OpaqueTarget := + self.config.extraDepTarget + +/-- The package's `dir` joined with its `depsDir` configuration. -/ +def depsDir (self : Package) : FilePath := + self.dir / self.config.depsDir + +/-- The package's `dir` joined with its `srcDir` configuration. -/ +def srcDir (self : Package) : FilePath := + self.dir / self.config.srcDir + +/-- The package's root directory for Lean (i.e., `srcDir`). -/ +def rootDir (self : Package) : FilePath := + self.srcDir + +/-- The path to a module's `.lean` source file within the package. -/ +def modToSrc (mod : Name) (self : Package) : FilePath := + Lean.modToFilePath self.srcDir mod "lean" + +/-- The package's `dir` joined with its `buildDir` configuration. -/ +def buildDir (self : Package) : FilePath := + self.dir / self.config.buildDir + +/-- The package's `buildDir` joined with its `oleanDir` configuration. -/ +def oleanDir (self : Package) : FilePath := + self.buildDir / self.config.oleanDir + +/-- The package's `leanArgs` configuration. -/ +def leanArgs (self : Package) : Array String := + self.config.leanArgs + +/-- The path to a module's `.olean` file within the package. -/ +def modToOlean (mod : Name) (self : Package) : FilePath := + Lean.modToFilePath self.oleanDir mod "olean" + +/-- The path to module's `.hash` file within the package. -/ +def modToHashFile (mod : Name) (self : Package) : FilePath := + Lean.modToFilePath self.oleanDir mod "hash" + /-- The package's `libRoots` configuration. -/ def libRoots (self : Package) : Array Name := self.config.libRoots @@ -293,42 +337,6 @@ def isLocalModule (mod : Name) (self : Package) : Bool := self.libRoots.any (fun root => root.isPrefixOf mod) || self.libGlobs.any (fun glob => glob.matches mod) -/-- The package's `dependencies` configuration. -/ -def dependencies (self : Package) : List Dependency := - self.config.dependencies - -/-- The package's `extraDepTarget` configuration. -/ -def extraDepTarget (self : Package) : OpaqueTarget := - self.config.extraDepTarget - -/-- The package's `leanArgs` configuration. -/ -def leanArgs (self : Package) : Array String := - self.config.leanArgs - -/-- The package's `leancArgs` configuration. -/ -def leancArgs (self : Package) : Array String := - self.config.leancArgs - -/-- The package's `linkArgs` configuration. -/ -def linkArgs (self : Package) : Array String := - self.config.linkArgs - -/-- The package's `dir` joined with its configuration's `depsDir`. -/ -def depsDir (self : Package) : FilePath := - self.dir / self.config.depsDir - -/-- The package's `dir` joined with its configuration's `srcDir`. -/ -def srcDir (self : Package) : FilePath := - self.dir / self.config.srcDir - -/-- The package's root directory for Lean (i.e., `srcDir`). -/ -def rootDir (self : Package) : FilePath := - self.srcDir - -/-- The path to a module's `.lean` source file within the package. -/ -def modToSrc (mod : Name) (self : Package) : FilePath := - Lean.modToFilePath self.srcDir mod "lean" - /-- Get an `Array` of the package's module. -/ def getModuleArray (self : Package) : IO (Array Name) := do let mut mods := #[] @@ -336,23 +344,11 @@ def getModuleArray (self : Package) : IO (Array Name) := do mods ← glob.pushModules self.srcDir mods return mods -/-- The package's `dir` joined with its configuration's `buildDir`. -/ -def buildDir (self : Package) : FilePath := - self.dir / self.config.buildDir +/-- The package's `leancArgs` configuration. -/ +def leancArgs (self : Package) : Array String := + self.config.leancArgs -/-- The package's `buildDir` joined with its configuration's `oleanDir`. -/ -def oleanDir (self : Package) : FilePath := - self.buildDir / self.config.oleanDir - -/-- The path to a module's `.olean` file within the package. -/ -def modToOlean (mod : Name) (self : Package) : FilePath := - Lean.modToFilePath self.oleanDir mod "olean" - -/-- The path to module's `.hash` file within the package. -/ -def modToHashFile (mod : Name) (self : Package) : FilePath := - Lean.modToFilePath self.oleanDir mod "hash" - -/-- The package's `buildDir` joined with its configuration's `irDir`. -/ +/-- The package's `buildDir` joined with its `irDir` configuration. -/ def irDir (self : Package) : FilePath := self.buildDir / self.config.irDir @@ -372,11 +368,27 @@ def oDir (self : Package) : FilePath := def modToO (mod : Name) (self : Package) : FilePath := Lean.modToFilePath self.oDir mod "o" +/-- The package's `buildDir` joined with its `libDir` configuration. -/ +def libDir (self : Package) : FilePath := + self.buildDir / self.config.libDir + +/-- The package's `libName` configuration. -/ +def staticLibName (self : Package) : FilePath := + self.config.libName + +/-- The file name of package's static library (i.e., `lib{staticLibName}.a`) -/ +def staticLibFileName (self : Package) : FilePath := + s!"lib{self.staticLibName}.a" + +/-- The path to the package's static library. -/ +def staticLibFile (self : Package) : FilePath := + self.libDir / self.staticLibFileName + /-- The package's `binRoot` configuration. -/ def binRoot (self : Package) : Name := self.config.binRoot -/-- The package's `buildDir` joined with its configuration's `binDir`. -/ +/-- The package's `buildDir` joined with its `binDir` configuration. -/ def binDir (self : Package) : FilePath := self.buildDir / self.config.binDir @@ -395,22 +407,10 @@ def binFileName (self : Package) : FilePath := def binFile (self : Package) : FilePath := self.binDir / self.binFileName -/-- The package's `buildDir` joined with its configuration's `libDir`. -/ -def libDir (self : Package) : FilePath := - self.buildDir / self.config.libDir - -/-- The package's `libName` configuration. -/ -def staticLibName (self : Package) : FilePath := - self.config.libName - -/-- The file name of package's static library (i.e., `lib{staticLibName}.a`) -/ -def staticLibFileName (self : Package) : FilePath := - s!"lib{self.staticLibName}.a" - -/-- The path to the package's static library. -/ -def staticLibFile (self : Package) : FilePath := - self.libDir / self.staticLibFileName - /-- The package's `moreLibTargets` configuration. -/ def moreLibTargets (self : Package) : Array FileTarget := self.config.moreLibTargets + +/-- The package's `linkArgs` configuration. -/ +def linkArgs (self : Package) : Array String := + self.config.linkArgs diff --git a/README.md b/README.md index 14f3f2da65..f431878316 100644 --- a/README.md +++ b/README.md @@ -70,16 +70,16 @@ Lake provides a large assortment of configuration options for packages. * `name` **(Required)**: The name of the package. * `version` **(Required)**: The version string of the package. -* `libRoots`: The root module of the package. Imports relative to this root (e.g., `Pkg.Foo`) are considered part of the package. Defaults to the package's uppercase `name`. -* `libGlobs`: An `Array` of additional module `Glob`s to include in the package. Defaults to singular globs of the module's `libRoots`. Submodule globs build every source file within their directory. Local imports of said files (i.e., fellow modules of the package) are also recursively built. +* `scripts`: A `HashMap` of scripts for the package. A `Script` is an arbitrary `(args : List String) → IO PUnit` function that is indexed by a `String` key and can be be run by `lake run [-- ]`. * `dependencies`: A `List` of the package's dependencies. * `depsDir`: The directory to which Lake should download dependencies. Defaults to `lean_packages`. * `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. -* `leanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. * `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`. * `oleanDir`: The build subdirectory to which Lake should output the package's `.olean` files. Defaults to `lib`. -* `scripts`: A `HashMap` of scripts for the package. A `Script` is an arbitrary `(args : List String) → IO PUnit` function that is indexed by a `String` key and can be be run by `lake run [-- ]`. +* `libRoots`: The root module(s) of the package. Imports relative to this root (e.g., `Pkg.Foo`) are considered part of the package. Defaults to a single root of the package's uppercase `name`. +* `libGlobs`: An `Array` of additional module `Glob`s to include in the package. Defaults to singular globs of the module's `libRoots`. Submodule globs build every source file within their directory. Local imports of said files (i.e., fellow modules of the package) are also recursively built. +* `leanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. ### Library / Binary Compilation