From 62815168c66393aba603c5f883cef7beebd8e53b Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 26 Jun 2022 20:35:23 -0400 Subject: [PATCH] feat: library-level module configuration --- Lake/Config/ExternLib.lean | 4 ++++ Lake/Config/LeanConfig.lean | 32 +++++++++++++++++++++++++ Lake/Config/LeanExe.lean | 33 ++++++++++++++++++++++++- Lake/Config/LeanExeConfig.lean | 10 +++----- Lake/Config/LeanLib.lean | 26 ++++++++++++++++---- Lake/Config/LeanLibConfig.lean | 19 ++++++--------- Lake/Config/Module.lean | 27 ++++++++++----------- Lake/Config/Package.lean | 44 +++++++--------------------------- 8 files changed, 119 insertions(+), 76 deletions(-) create mode 100644 Lake/Config/LeanConfig.lean diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean index 371fc3b6a9..5378b3feaa 100644 --- a/Lake/Config/ExternLib.lean +++ b/Lake/Config/ExternLib.lean @@ -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, ·⟩) diff --git a/Lake/Config/LeanConfig.lean b/Lake/Config/LeanConfig.lean new file mode 100644 index 0000000000..51899ee719 --- /dev/null +++ b/Lake/Config/LeanConfig.lean @@ -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 diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean index 6a0502e071..23dc88cffd 100644 --- a/Lake/Config/LeanExe.lean +++ b/Lake/Config/LeanExe.lean @@ -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 diff --git a/Lake/Config/LeanExeConfig.lean b/Lake/Config/LeanExeConfig.lean index f60bd6a545..4566109cd3 100644 --- a/Lake/Config/LeanExeConfig.lean +++ b/Lake/Config/LeanExeConfig.lean @@ -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 diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index be61f919cb..97db0f29a5 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -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. diff --git a/Lake/Config/LeanLibConfig.lean b/Lake/Config/LeanLibConfig.lean index 88dd1678e1..6110eb7375 100644 --- a/Lake/Config/LeanLibConfig.lean +++ b/Lake/Config/LeanLibConfig.lean @@ -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 diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index a2bcddfe47..f8ff58d244 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -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 diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 85228fe372..2411f52f56 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -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 :=