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

@@ -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

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
 

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

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
 

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