From 7435fd5dd43224d87d92cb7bd2314673ea2a26fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Nov 2021 10:25:26 -0800
Subject: [PATCH] chore: add `USE_GMP` cmake option

---
 src/CMakeLists.txt | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8b7d09a5a6..415bc3f110 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -58,6 +58,7 @@ option(SMALL_ALLOCATOR     "SMALL_ALLOCATOR" ON)
 option(LAZY_RC             "LAZY_RC" OFF)
 option(RUNTIME_STATS       "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
+option(USE_GMP "USE_GMP" ON)
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" ON)
@@ -227,15 +228,18 @@ elseif (MULTI_THREAD)
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 endif ()
 
-if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  include_directories(${GMP_INSTALL_PREFIX}/include)
-  set(GMP_LIBRARIES "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
-else()
-  # GMP
-  find_package(GMP 5.0.5 REQUIRED)
-  include_directories(${GMP_INCLUDE_DIR})
-  # dlopen
-  set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
+if("${USE_GMP}" MATCHES "ON")
+  set(CMAKE_CXX_FLAGS                "-D LEAN_USE_GMP ${CMAKE_CXX_FLAGS}")
+  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+    include_directories(${GMP_INSTALL_PREFIX}/include)
+    set(GMP_LIBRARIES "${GMP_INSTALL_PREFIX}/lib/libgmp.a")
+  else()
+    # GMP
+    find_package(GMP 5.0.5 REQUIRED)
+    include_directories(${GMP_INCLUDE_DIR})
+    # dlopen
+    set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS})
+  endif()
 endif()
 
 # ccache