From 0002d8bd04f6b23e934c052db1468c844d342dfb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 29 Nov 2021 11:35:13 -0800
Subject: [PATCH] chore: missing `#ifdef LEAN_USE_GMP`

---
 src/include/lean/lean_gmp.h | 2 ++
 src/runtime/compact.cpp     | 8 ++++++++
 src/runtime/mpz.cpp         | 9 ++++++++-
 src/runtime/object.cpp      | 2 ++
 4 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/include/lean/lean_gmp.h b/src/include/lean/lean_gmp.h
index 9bf971e818..d109646ecf 100644
--- a/src/include/lean/lean_gmp.h
+++ b/src/include/lean/lean_gmp.h
@@ -12,12 +12,14 @@ Author: Leonardo de Moura
 extern "C" {
 #endif
 
+#ifdef LEAN_USE_GMP
 LEAN_SHARED lean_object * lean_alloc_mpz(mpz_t);
 /* Set `v` with the value stored in `o`.
    - pre: `lean_is_mpz(o)`
    - pre: `v` has already been initialized using `mpz_init` (or equivalent).
 */
 LEAN_SHARED void lean_extract_mpz_value(lean_object * o, mpz_t v);
+#endif
 
 #ifdef __cplusplus
 }
diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp
index 5c32be133f..7076ea6aa1 100644
--- a/src/runtime/compact.cpp
+++ b/src/runtime/compact.cpp
@@ -256,6 +256,7 @@ bool object_compactor::insert_task(object * o) {
 }
 
 void object_compactor::insert_mpz(object * o) {
+#ifdef LEAN_USE_GMP
     size_t nlimbs = mpz_size(to_mpz(o)->m_value.m_val);
     size_t data_sz = sizeof(mp_limb_t) * nlimbs;
     size_t sz = sizeof(mpz_object) + data_sz;
@@ -269,6 +270,9 @@ void object_compactor::insert_mpz(object * o) {
     m._mp_d = reinterpret_cast<mp_limb_t *>(reinterpret_cast<char *>(data) - reinterpret_cast<char *>(m_begin) + reinterpret_cast<ptrdiff_t>(m_base_addr));
     m._mp_alloc = nlimbs;
     save(o, (lean_object*)new_o);
+#else
+    // TODO
+#endif
 }
 
 #ifdef LEAN_TAG_COUNTERS
@@ -418,9 +422,13 @@ inline void compacted_region::fix_task(object * o) {
 }
 
 void compacted_region::fix_mpz(object * o) {
+#ifdef LEAN_USE_GMP
     __mpz_struct & m = to_mpz(o)->m_value.m_val[0];
     m._mp_d = reinterpret_cast<mp_limb_t *>(static_cast<char *>(m_begin) + reinterpret_cast<size_t>(m._mp_d) - reinterpret_cast<size_t>(m_base_addr));
     move(sizeof(mpz_object) + sizeof(mp_limb_t) * mpz_size(to_mpz(o)->m_value.m_val));
+#else
+    // TODO
+#endif
 }
 
 object * compacted_region::read() {
diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp
index 8ec2fa9337..41049b1565 100644
--- a/src/runtime/mpz.cpp
+++ b/src/runtime/mpz.cpp
@@ -11,7 +11,8 @@ Author: Leonardo de Moura
 #include "runtime/mpz.h"
 
 namespace lean {
-
+/***** GMP VERSION ******/
+#ifdef LEAN_USE_GMP
 mpz::mpz() {
     mpz_init(m_val);
 }
@@ -245,6 +246,12 @@ std::ostream & operator<<(std::ostream & out, mpz const & v) {
     return out;
 }
 
+#else
+/***** NON GMP VERSION ******/
+
+#endif
+
+
 std::string mpz::to_string() const {
     std::ostringstream out;
     out << *this;
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index aadbc732ea..3861635a40 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1060,6 +1060,7 @@ object * alloc_mpz(mpz const & m) {
     return (lean_object*)o;
 }
 
+#ifdef LEAN_USE_GMP
 extern "C" LEAN_EXPORT lean_object * lean_alloc_mpz(mpz_t v) {
     return alloc_mpz(mpz(v));
 }
@@ -1067,6 +1068,7 @@ extern "C" LEAN_EXPORT lean_object * lean_alloc_mpz(mpz_t v) {
 extern "C" LEAN_EXPORT void lean_extract_mpz_value(lean_object * o, mpz_t v) {
     return to_mpz(o)->m_value.set(v);
 }
+#endif
 
 object * mpz_to_nat_core(mpz const & m) {
     lean_assert(!m.is_size_t() || m.get_size_t() > LEAN_MAX_SMALL_NAT);