chore: avoid stack overflow in debug tests (leanprover#6103)

kmill · Nov 17, 2024 · 405593e · 405593e
1 parent 24f305c
commit 405593e
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -37,7 +37,15 @@ extern "C" {
 #if defined(__GNUC__) || defined(__clang__)
 #define LEAN_UNLIKELY(x) (__builtin_expect((x), 0))
 #define LEAN_LIKELY(x) (__builtin_expect((x), 1))
+
+#ifdef NDEBUG
 #define LEAN_ALWAYS_INLINE __attribute__((always_inline))
+#else
+// We have observed stack frame increases from forced inlining overflowing the stack in debug builds,
+// let's leave the decision to the compiler in that case
+#define LEAN_ALWAYS_INLINE
+#endif
+
 #else
 #define LEAN_UNLIKELY(x) (x)
 #define LEAN_LIKELY(x) (x)