max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: -O3 not -03

Browse source
This commit is contained in:
tydeu 2021-09-25 23:59:13 -04:00
parent ff1e63c719
commit 6a9997c7ad
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Package.lean
View file

@ -172,7 +172,7 @@ structure PackageConfig where
/--
Additional arguments to pass to `leanc`
while compiling the C source files generated by `lean`.
Defaults to `-03` and `-DNDEBUG`.
Defaults to `-O3` and `-DNDEBUG`.
-/
leancArgs : Array String := #["-O3", "-DNDEBUG"]

2
README.md
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`. Defaults to `-03` and `-DNDEBUG`.
* `leancArgs`: An `Array` additional arguments to pass to `leanc` while compiling the C source files generated by `lean`. Defaults to `-O3` 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`.