feat: library-level module configuration
This commit is contained in:
tydeu
parent
c0bc0344b0
commit
62815168c6
8 changed files with 119 additions and 76 deletions
|
|
@ -15,6 +15,10 @@ structure ExternLib where
|
|||
config : ExternLibConfig
|
||||
deriving Inhabited
|
||||
|
||||
/-- The external libraries of the package (as an Array). -/
|
||||
@[inline] def Package.externLibs (self : Package) : Array ExternLib :=
|
||||
self.externLibConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
|
||||
|
||||
/-- Try to find a external library in the package with the given name. -/
|
||||
@[inline] def Package.findExternLib? (name : Name) (self : Package) : Option ExternLib :=
|
||||
self.externLibConfigs.find? name |>.map (⟨self, ·⟩)
|
||||
|
|
|
|||
32
Lake/Config/LeanConfig.lean
Normal file
32
Lake/Config/LeanConfig.lean
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
/-
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
namespace Lake
|
||||
|
||||
/-- Configuration options common to targets that build modules. -/
|
||||
structure LeanConfig where
|
||||
/--
|
||||
Additional arguments to pass to `lean` when compiling
|
||||
a module's Lean source files.
|
||||
-/
|
||||
moreLeanArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc` when compiling
|
||||
a module's C source files generated by `lean`.
|
||||
|
||||
Lake already passes `-O3` and `-DNDEBUG` automatically,
|
||||
but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
|
||||
-/
|
||||
moreLeancArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc` when linking (e.g., shared
|
||||
libraries or binary executable). These will come *after* the paths of
|
||||
external libraries.
|
||||
-/
|
||||
moreLinkArgs : Array String := #[]
|
||||
|
||||
deriving Inhabited, Repr
|
||||
|
|
@ -16,6 +16,10 @@ structure LeanExe where
|
|||
config : LeanExeConfig
|
||||
deriving Inhabited
|
||||
|
||||
/-- The Lean executables of the package (as an Array). -/
|
||||
@[inline] def Package.leanExes (self : Package) : Array LeanExe :=
|
||||
self.leanExeConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
|
||||
|
||||
/-- The Lean executable built into the package. -/
|
||||
@[inline] def Package.builtinExe (self : Package) : LeanExe :=
|
||||
⟨self, self.builtinExeConfig⟩
|
||||
|
|
@ -24,11 +28,29 @@ structure LeanExe where
|
|||
@[inline] def Package.findLeanExe? (name : Name) (self : Package) : Option LeanExe :=
|
||||
self.leanExeConfigs.find? name |>.map (⟨self, ·⟩)
|
||||
|
||||
/--
|
||||
Converts the executable configuration into a library
|
||||
with a single module (the root).
|
||||
-/
|
||||
def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig) : LeanLibConfig where
|
||||
name := self.name
|
||||
roots := #[self.root]
|
||||
libName := self.exeName
|
||||
toLeanConfig := self.toLeanConfig
|
||||
|
||||
namespace LeanExe
|
||||
|
||||
/-- Converts the executable into a library with a single module (the root). -/
|
||||
@[inline] def toLeanLib (self : LeanExe) : LeanLib :=
|
||||
⟨self.pkg, self.config.toLeanLibConfig⟩
|
||||
|
||||
/-- The executable's root module. -/
|
||||
@[inline] def root (self : LeanExe) : Module :=
|
||||
⟨self.pkg, WfName.ofName self.config.root⟩
|
||||
⟨self.toLeanLib, WfName.ofName self.config.root⟩
|
||||
|
||||
/- Return the the modules root if the name matches, otherwise return none. -/
|
||||
def isRoot? (name : Name) (self : LeanExe) : Option Module :=
|
||||
if name == self.config.root then some self.root else none
|
||||
|
||||
/--
|
||||
The file name of binary executable
|
||||
|
|
@ -52,3 +74,12 @@ def linkArgs (self : LeanExe) : Array String :=
|
|||
#["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
|
||||
else
|
||||
self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
|
||||
|
||||
end LeanExe
|
||||
|
||||
/-- Locate the named module in the package (if it is buildable and local to it). -/
|
||||
def Package.findModule? (mod : Name) (self : Package) : Option Module :=
|
||||
self.leanLibs.findSome? (·.findModule? mod) <|>
|
||||
self.leanExes.findSome? (·.isRoot? mod) <|>
|
||||
self.builtinLib.findModule? mod <|>
|
||||
self.builtinExe.isRoot? mod
|
||||
|
|
|
|||
|
|
@ -3,11 +3,13 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
import Lake.Config.LeanConfig
|
||||
|
||||
namespace Lake
|
||||
open Lean System
|
||||
|
||||
/-- A Lean executable's declarative configuration. -/
|
||||
structure LeanExeConfig where
|
||||
structure LeanExeConfig extends LeanConfig where
|
||||
/-- The name of the target. -/
|
||||
name : Name
|
||||
|
||||
|
|
@ -41,10 +43,4 @@ structure LeanExeConfig where
|
|||
-/
|
||||
supportInterpreter : Bool := false
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc` when linking the binary executable.
|
||||
These will come *after* the paths of the package's external libraries.
|
||||
-/
|
||||
moreLinkArgs : Array String := #[]
|
||||
|
||||
deriving Inhabited, Repr
|
||||
|
|
|
|||
|
|
@ -16,6 +16,10 @@ structure LeanLib where
|
|||
config : LeanLibConfig
|
||||
deriving Inhabited
|
||||
|
||||
/-- The Lean libraries of the package (as an Array). -/
|
||||
@[inline] def Package.leanLibs (self : Package) : Array LeanLib :=
|
||||
self.leanLibConfigs.fold (fun a _ v => a.push (⟨self, v⟩)) #[]
|
||||
|
||||
/-- The Lean library built into the package. -/
|
||||
@[inline] def Package.builtinLib (self : Package) : LeanLib :=
|
||||
⟨self, self.builtinLibConfig⟩
|
||||
|
|
@ -55,14 +59,26 @@ def sharedLibFile (self : LeanLib) : FilePath :=
|
|||
self.pkg.libDir / self.sharedLibFileName
|
||||
|
||||
/--
|
||||
The arguments to pass to `leanc` when compiling the library's C files.
|
||||
It is `-O3`, `-DNDEBUG`, the package's `moreLeancArgs`, and then the library's
|
||||
`moreLeancArgs`.
|
||||
Whether to precompile the library's modules.
|
||||
Is true if either the package or the library have `precompileModules` set.
|
||||
-/
|
||||
def precompileModules (self : LeanLib) : Bool :=
|
||||
self.pkg.precompileModules || self.config.precompileModules
|
||||
|
||||
TODO: Use this option.
|
||||
/--
|
||||
The arguments to pass to `lean` when compiling the library's Lean files.
|
||||
That is, the package's `moreLeanArgs` plus the library's `moreLeanArgs`.
|
||||
-/
|
||||
def leanArgs (self : LeanLib) : Array String :=
|
||||
self.pkg.moreLeanArgs ++ self.config.moreLeanArgs
|
||||
|
||||
/--
|
||||
The arguments to pass to `leanc` when compiling the library's C files.
|
||||
That is, `-O3`, `-DNDEBUG`, the package's `moreLeancArgs`, and then the
|
||||
library's `moreLeancArgs`.
|
||||
-/
|
||||
def leancArgs (self : LeanLib) : Array String :=
|
||||
self.pkg.moreLeancArgs ++ self.config.moreLeancArgs
|
||||
#["-O3", "-DNDEBUG"] ++ self.pkg.moreLeancArgs ++ self.config.moreLeancArgs
|
||||
|
||||
/--
|
||||
The arguments to pass to `leanc` when linking the shared library.
|
||||
|
|
|
|||
|
|
@ -5,13 +5,14 @@ Authors: Mac Malone
|
|||
-/
|
||||
import Lake.Util.Casing
|
||||
import Lake.Config.InstallPath
|
||||
import Lake.Config.LeanConfig
|
||||
import Lake.Config.Glob
|
||||
|
||||
namespace Lake
|
||||
open Lean System
|
||||
|
||||
/-- A Lean library's declarative configuration. -/
|
||||
structure LeanLibConfig where
|
||||
structure LeanLibConfig extends LeanConfig where
|
||||
/-- The name of the target. -/
|
||||
name : Name
|
||||
|
||||
|
|
@ -51,19 +52,13 @@ structure LeanLibConfig where
|
|||
libName := toUpperCamelCase name |>.toString (escape := false)
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc`
|
||||
while compiling the library's C source files generated by `lean`.
|
||||
Whether to compile each of the library's modules into a native shared library
|
||||
that is loaded whenever the module is imported. This speeds up evaluation of
|
||||
metaprograms and enables the interpreter to run functions marked `@[extern]`.
|
||||
|
||||
Lake already passes `-O3` and `-DNDEBUG` automatically,
|
||||
but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
|
||||
Defaults to `false`.
|
||||
-/
|
||||
moreLeancArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc` while linking the shared library.
|
||||
These will come *after* the paths of package's external libraries.
|
||||
-/
|
||||
moreLinkArgs : Array String := #[]
|
||||
precompileModules : Bool := false
|
||||
|
||||
deriving Inhabited, Repr
|
||||
|
||||
|
|
|
|||
|
|
@ -9,9 +9,9 @@ import Lake.Config.LeanLib
|
|||
namespace Lake
|
||||
open Std System
|
||||
|
||||
/-- A buildable Lean module of a `Package`. -/
|
||||
/-- A buildable Lean module of a `LeanLib`. -/
|
||||
structure Module where
|
||||
pkg : Package
|
||||
lib : LeanLib
|
||||
name : WfName
|
||||
deriving Inhabited
|
||||
|
||||
|
|
@ -24,24 +24,22 @@ abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
|
|||
/-- Locate the named module in the library (if it is buildable and local to it). -/
|
||||
def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module :=
|
||||
let mod := WfName.ofName mod
|
||||
if self.isBuildableModule mod then some ⟨self.pkg, mod⟩ else none
|
||||
if self.isBuildableModule mod then some ⟨self, mod⟩ else none
|
||||
|
||||
/-- Get an `Array` of the library's modules. -/
|
||||
def LeanLib.getModuleArray (self : LeanLib) : IO (Array Module) :=
|
||||
(·.2) <$> StateT.run (s := #[]) do
|
||||
self.config.globs.forM fun glob => do
|
||||
glob.forEachModuleIn self.srcDir fun mod => do
|
||||
modify (·.push ⟨self.pkg, mod⟩)
|
||||
|
||||
/-- Locate the named module in the package (if it is buildable and local to it). -/
|
||||
def Package.findModule? (mod : Name) (self : Package) : Option Module :=
|
||||
let mod := WfName.ofName mod
|
||||
if self.isBuildableModule mod then some ⟨self, mod⟩ else none
|
||||
modify (·.push ⟨self, mod⟩)
|
||||
|
||||
namespace Module
|
||||
|
||||
abbrev pkg (self : Module) : Package :=
|
||||
self.lib.pkg
|
||||
|
||||
@[inline] def leanFile (self : Module) : FilePath :=
|
||||
Lean.modToFilePath self.pkg.srcDir self.name "lean"
|
||||
Lean.modToFilePath self.lib.srcDir self.name "lean"
|
||||
|
||||
@[inline] def oleanFile (self : Module) : FilePath :=
|
||||
Lean.modToFilePath self.pkg.oleanDir self.name "olean"
|
||||
|
|
@ -69,17 +67,16 @@ namespace Module
|
|||
self.pkg.libDir / s!"lib{self.dynlib}.{sharedLibExt}"
|
||||
|
||||
@[inline] def leanArgs (self : Module) : Array String :=
|
||||
self.pkg.moreLeanArgs
|
||||
self.lib.leanArgs
|
||||
|
||||
@[inline] def leancArgs (self : Module) : Array String :=
|
||||
self.pkg.moreLeancArgs
|
||||
self.lib.leancArgs
|
||||
|
||||
@[inline] def linkArgs (self : Module) : Array String :=
|
||||
-- TODO: derive link arguments from library, not package
|
||||
self.pkg.config.moreLinkArgs
|
||||
self.lib.linkArgs
|
||||
|
||||
@[inline] def shouldPrecompile (self : Module) : Bool :=
|
||||
self.pkg.precompileModules
|
||||
self.lib.precompileModules
|
||||
|
||||
@[inline] def isLeanOnly (self : Module) : Bool :=
|
||||
self.pkg.isLeanOnly && !self.shouldPrecompile
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩
|
|||
--------------------------------------------------------------------------------
|
||||
|
||||
/-- A `Package`'s declarative configuration. -/
|
||||
structure PackageConfig extends WorkspaceConfig where
|
||||
structure PackageConfig extends WorkspaceConfig, LeanConfig where
|
||||
|
||||
/-- The `Name` of the package. -/
|
||||
name : Name
|
||||
|
|
@ -93,9 +93,9 @@ structure PackageConfig extends WorkspaceConfig where
|
|||
defaultFacet : PackageFacet := .exe
|
||||
|
||||
/--
|
||||
Whether to compile each module into a native shared library that is loaded
|
||||
whenever the module is imported. This speeds up evaluation of metaprograms
|
||||
and enables the interpreter to run functions marked `@[extern]`.
|
||||
Whether to compile each of the package's module into a native shared library
|
||||
that is loaded whenever the module is imported. This speeds up evaluation of
|
||||
metaprograms and enables the interpreter to run functions marked `@[extern]`.
|
||||
|
||||
Defaults to `false`.
|
||||
-/
|
||||
|
|
@ -157,20 +157,6 @@ structure PackageConfig extends WorkspaceConfig where
|
|||
-/
|
||||
libGlobs : Array Glob := libRoots.map Glob.one
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `lean` while compiling Lean source files.
|
||||
-/
|
||||
moreLeanArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc`
|
||||
while compiling the C source files generated by `lean`.
|
||||
|
||||
Lake already passes `-O3` and `-DNDEBUG` automatically,
|
||||
but you can change this by, for example, adding `-O0` and `-UNDEBUG`.
|
||||
-/
|
||||
moreLeancArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
The build subdirectory to which Lake should output
|
||||
the package's intermediary results (e.g., `.c` and `.o` files).
|
||||
|
|
@ -237,21 +223,6 @@ structure PackageConfig extends WorkspaceConfig where
|
|||
-/
|
||||
supportInterpreter : Bool := false
|
||||
|
||||
/--
|
||||
Additional arguments to pass to `leanc` while compiling the package's
|
||||
binary executable. These will come *after* the paths of libraries built
|
||||
with `moreLibTargets`.
|
||||
-/
|
||||
moreLinkArgs : Array String := #[]
|
||||
|
||||
/--
|
||||
Marks the package as only containing scripts.
|
||||
|
||||
Used to turn off deprecation warnings about package facets in packages
|
||||
not intended to have any targets.
|
||||
-/
|
||||
scriptsOnly : Bool := false
|
||||
|
||||
deriving Inhabited
|
||||
|
||||
namespace PackageConfig
|
||||
|
|
@ -261,13 +232,14 @@ def toLeanLibConfig (self : PackageConfig) : LeanLibConfig where
|
|||
name := self.libName
|
||||
roots := self.libRoots
|
||||
globs := self.libGlobs
|
||||
toLeanConfig := self.toLeanConfig
|
||||
|
||||
/-- The configuration of the package's binary executable. -/
|
||||
def toLeanExeConfig (self : PackageConfig) : LeanExeConfig where
|
||||
root := self.binRoot
|
||||
name := self.binName
|
||||
supportInterpreter := self.supportInterpreter
|
||||
moreLinkArgs := self.moreLinkArgs
|
||||
toLeanConfig := self.toLeanConfig
|
||||
|
||||
end PackageConfig
|
||||
|
||||
|
|
@ -385,9 +357,9 @@ def externLibTargets (self : Package) : Array FileTarget :=
|
|||
@[inline] def moreLeanArgs (self : Package) : Array String :=
|
||||
self.config.moreLeanArgs
|
||||
|
||||
/- `-O3`, `-DNDEBUG`, and `moreLeancArgs` -/
|
||||
/- The package's `moreLeancArgs` configuration. -/
|
||||
@[inline] def moreLeancArgs (self : Package) : Array String :=
|
||||
#["-O3", "-DNDEBUG"] ++ self.config.moreLeancArgs
|
||||
self.config.moreLeancArgs
|
||||
|
||||
/-- The package's `moreLinkArgs` configuration. -/
|
||||
@[inline] def moreLinkArgs (self : Package) : Array String :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue