diff --git a/Lake/Package.lean b/Lake/Package.lean index d2aa3e621c..6d6c2e8388 100644 --- a/Lake/Package.lean +++ b/Lake/Package.lean @@ -172,8 +172,9 @@ structure PackageConfig where /-- Additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. + Defaults to `-03` and `-DNDEBUG`. -/ - leancArgs : Array String := #[] + leancArgs : Array String := #["-O3", "-DNDEBUG"] /-- The build subdirectory to which Lake should output diff --git a/README.md b/README.md index b335dcac26..646b47c6b7 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,7 @@ Lake provides a large assortment of configuration options for packages. ### Library / Binary Compilation -* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. +* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Defaults to `-03` and `-DNDEBUG`. * `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`. diff --git a/examples/bootstrap/package.lean b/examples/bootstrap/package.lean index 7bfaa91371..0a7e3f44af 100644 --- a/examples/bootstrap/package.lean +++ b/examples/bootstrap/package.lean @@ -5,7 +5,6 @@ package where name := "lake" srcDir := FilePath.mk ".." / ".." oleanDir := "." - leancArgs := #["-O3", "-DNDEBUG"] binRoot := `Lake.Main linkArgs := if Platform.isWindows then