From 6cfbd904262c786189a9594aaadbce146350ab60 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 6 Oct 2021 21:07:56 -0400 Subject: [PATCH] refactor: always pass `-O3` and `-DNDEBUG` when building Lean o files also add `more` prefix to `leanArgs`/`leancArgs`/`linkArgs` closes leanprover/lake#19 --- Lake/BuildBin.lean | 5 ++--- Lake/BuildModule.lean | 4 ++-- Lake/Package.lean | 30 ++++++++++++++++-------------- README.md | 10 +++++----- examples/bootstrap/lakefile.lean | 2 +- 5 files changed, 26 insertions(+), 25 deletions(-) diff --git a/Lake/BuildBin.lean b/Lake/BuildBin.lean index c41c21234c..90f3a37681 100644 --- a/Lake/BuildBin.lean +++ b/Lake/BuildBin.lean @@ -13,11 +13,10 @@ namespace Lake def ActivePackageTarget.oFileTargets (self : ActivePackageTarget) : Array FileTarget := - let leancArgs := self.package.leancArgs self.moduleTargets.map fun (mod, target) => let oFile := self.package.modToO mod let cTarget := Target.active target.cTarget - leanOFileTarget oFile cTarget leancArgs + leanOFileTarget oFile cTarget self.package.moreLeancArgs -- # Build Package Lib @@ -43,7 +42,7 @@ def ActivePackageTarget.linkTargets protected def ActivePackageTarget.binTarget (depTargets : Array ActivePackageTarget) (self : ActivePackageTarget) : FileTarget := let linkTargets := self.linkTargets depTargets - leanBinTarget self.package.binFile linkTargets self.package.linkArgs + leanBinTarget self.package.binFile linkTargets self.package.moreLinkArgs def Package.binTarget (self : Package) : FileTarget := Target.mk self.binFile do diff --git a/Lake/BuildModule.lean b/Lake/BuildModule.lean index 196201b658..013d9060ac 100644 --- a/Lake/BuildModule.lean +++ b/Lake/BuildModule.lean @@ -104,7 +104,7 @@ protected def Package.moduleOleanAndCTarget let traceFile := self.modToTraceFile mod let oleanDirs := self.oleanDir :: moreOleanDirs moduleOleanAndCTarget leanFile cFile oleanFile traceFile oleanDirs contents - depTarget self.rootDir self.leanArgs + depTarget self.rootDir self.moreLeanArgs protected def Package.moduleOleanTarget (self : Package) (moreOleanDirs : List FilePath) (mod : Name) @@ -113,7 +113,7 @@ protected def Package.moduleOleanTarget let traceFile := self.modToTraceFile mod let oleanDirs := self.oleanDir :: moreOleanDirs moduleOleanTarget leanFile oleanFile traceFile oleanDirs contents depTarget - self.rootDir self.leanArgs + self.rootDir self.moreLeanArgs -- # Recursive Building diff --git a/Lake/Package.lean b/Lake/Package.lean index c5c7e61473..bb6248803a 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -127,7 +127,7 @@ structure PackageConfig where An extra `OpaqueTarget` that should be built before the package. `OpaqueTarget.collectList/collectArray` can be used combine multiple - targets into a single `extraDepTarget`. + extra targets into a single `extraDepTarget`. -/ extraDepTarget : OpaqueTarget := Target.nil @@ -174,14 +174,16 @@ structure PackageConfig where /-- Additional arguments to pass to `lean` while compiling Lean source files. -/ - leanArgs : Array String := #[] + moreLeanArgs : Array String := #[] /-- Additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. - Defaults to `-O3` and `-DNDEBUG`. + + Lake already passes `-O3` and `-DNDEBUG` automatically, + but you can change this by, for example, adding `-O0` and `-UNDEBUG`. -/ - leancArgs : Array String := #["-O3", "-DNDEBUG"] + moreLeancArgs : Array String := #[] /-- The build subdirectory to which Lake should output @@ -241,7 +243,7 @@ structure PackageConfig where while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`. -/ - linkArgs : Array String := #[] + moreLinkArgs : Array String := #[] deriving Inhabited @@ -314,9 +316,9 @@ def buildDir (self : Package) : FilePath := 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 package's `moreLeanArgs` configuration. -/ +def moreLeanArgs (self : Package) : Array String := + self.config.moreLeanArgs /-- The path to a module's `.olean` file within the package. -/ def modToOlean (mod : Name) (self : Package) : FilePath := @@ -345,9 +347,9 @@ def getModuleArray (self : Package) : IO (Array Name) := do mods ← glob.pushModules self.srcDir mods return mods -/-- The package's `leancArgs` configuration. -/ -def leancArgs (self : Package) : Array String := - self.config.leancArgs +/- `-O3`, `-DNDEBUG`, and `moreLeancArgs` -/ +def moreLeancArgs (self : Package) : Array String := + #["-O3", "-DNDEBUG"] ++ self.config.moreLeancArgs /-- The package's `buildDir` joined with its `irDir` configuration. -/ def irDir (self : Package) : FilePath := @@ -412,6 +414,6 @@ def binFile (self : Package) : FilePath := def moreLibTargets (self : Package) : Array FileTarget := self.config.moreLibTargets -/-- The package's `linkArgs` configuration. -/ -def linkArgs (self : Package) : Array String := - self.config.linkArgs +/-- The package's `moreLinkArgs` configuration. -/ +def moreLinkArgs (self : Package) : Array String := + self.config.moreLinkArgs diff --git a/README.md b/README.md index 53c05ac73e..7775119dd9 100644 --- a/README.md +++ b/README.md @@ -89,25 +89,25 @@ Lake provides a large assortment of configuration options for packages. * `name` **(Required)**: The `Name` of the package. * `dependencies`: An `Array` 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. +* `extraDepTarget`: An extra `OpaqueTarget` that should be built before the package. `OpaqueTarget.collectList/collectArray` can be used combine multiple extra targets into a single `extraDepTarget`. * `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`. * `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 module `Glob`s to build for the package's library. Defaults to a `Glob.one` of each of the module's `libRoots`. Submodule globs build every source file within their directory. Local imports of glob'ed 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. +* `moreLeanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files. ### Library / Binary Compilation -* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Defaults to `-O3` and `-DNDEBUG`. +* `moreLeancArgs`: An `Array` of 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`. * `irDir`: The build subdirectory to which Lake should output the package's intermediary results (e.g., `.c` and `.o` files). Defaults to `ir`. * `libName`: The name of the package's static library. Defaults to the string representation of the package's `moduleRoot`. * `libDir`: The build subdirectory to which Lake should output the package's static library. Defaults to `lib`. * `binName`: The name of the package's binary executable. Defaults to the package's `name` with any `.` replaced with a `-`. * `binDir`: The build subdirectory to which Lake should output the package's binary executable. Defaults to `bin`. * `binRoot`: The root module of the package's binary executable. Defaults to `Main`. The root is built by recursively building its local imports (i.e., fellow modules of the package). This setting is most useful for packages that are distributing both a library and a binary (like Lake itself). In such cases, it is common for there to be code (e.g., `main`) that is needed for the binary but should not be included in the library proper. -* `moreLibTargets`: Additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables). -* `linkArgs`: Additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`. +* `moreLibTargets`: An `Array` of additional library `FileTarget`s (beyond the package's and its dependencies' libraries) to build and link to the package's binary executable (and/or to dependent package's executables). +* `moreLinkArgs`: An `Array` of additional arguments to pass to `leanc` while compiling the package's binary executable. These will come *after* the paths of libraries built with `moreLibTargets`. ## Scripts diff --git a/examples/bootstrap/lakefile.lean b/examples/bootstrap/lakefile.lean index 464b9abea6..2f7e6c330c 100644 --- a/examples/bootstrap/lakefile.lean +++ b/examples/bootstrap/lakefile.lean @@ -5,7 +5,7 @@ package lake where srcDir := FilePath.mk ".." / ".." oleanDir := "." binRoot := `Lake.Main - linkArgs := + moreLinkArgs := if Platform.isWindows then #["-Wl,--export-all"] else