From ff1e63c7194ea9722d6e6d358ce5b922f953fd97 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 25 Sep 2021 23:57:31 -0400
Subject: [PATCH] refactor: default `leancArgs`  to `-03`, `-DNDEBUG` (like
 `leanpkg`)

---
 Lake/Package.lean               | 3 ++-
 README.md                       | 2 +-
 examples/bootstrap/package.lean | 1 -
 3 files changed, 3 insertions(+), 3 deletions(-)

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