Skip to content

Commit e2a47a9

Browse files
committed
fix: lake: use -O0 for debug builds
1 parent 643b962 commit e2a47a9

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/lake/Lake/Config/LeanConfig.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ public inductive BuildType
7979
Debug optimization, asserts enabled, custom debug code enabled, and
8080
debug info included in executable (so you can step through the code with a
8181
debugger and have address to source-file:line-number translation).
82-
For example, passes `-Og -g` when compiling C code.
82+
For example, passes `-O0 -g` when compiling C code.
8383
-/
8484
| debug
8585
/--
@@ -112,7 +112,7 @@ public instance : Max BuildType := maxOfLe
112112

113113
/-- The arguments to pass to `leanc` based on the build type. -/
114114
public def leancArgs : BuildType → Array String
115-
| debug => #["-Og", "-g"]
115+
| debug => #["-O0", "-g"]
116116
| relWithDebInfo => #["-O3", "-g", "-DNDEBUG"]
117117
| minSizeRel => #["-Os", "-DNDEBUG"]
118118
| release => #["-O3", "-DNDEBUG"]

0 commit comments

Comments
 (0)