chore: build Lean with Elab.async

leanprover · Feb 7, 2025 · 1543a1a · 1543a1a
1 parent 1248a55
commit 1543a1a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -80,7 +80,7 @@ option(USE_GMP "USE_GMP" ON)
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" OFF)
 
-set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
+set(LEAN_EXTRA_MAKE_OPTS  "-DElab.async=true"          CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
 
 if ("${LAZY_RC}" MATCHES "ON")