refactor: default leancArgs to -03, -DNDEBUG (like leanpkg)

This commit is contained in:
tydeu 2021-09-25 23:57:31 -04:00
parent 3f534e1155
commit ff1e63c719
3 changed files with 3 additions and 3 deletions

View file

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

View file

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

View file

@ -5,7 +5,6 @@ package where
name := "lake"
srcDir := FilePath.mk ".." / ".."
oleanDir := "."
leancArgs := #["-O3", "-DNDEBUG"]
binRoot := `Lake.Main
linkArgs :=
if Platform.isWindows then