From 1fa1312c57cbf996b6159c8a4e2a413df9f3d37f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Feb 2017 12:09:19 -0800
Subject: [PATCH] chore(CMakeLists,frontends/lean): add SAVE_SNAPSHOT=OFF
 SAVE_INFO=OFF compilation options

---
 src/CMakeLists.txt                  | 12 +++++++++++-
 src/frontends/lean/info_manager.cpp | 15 +++++++++++++++
 src/frontends/lean/parser.cpp       |  3 +++
 3 files changed, 29 insertions(+), 1 deletion(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 520824584c..2418f3e1d4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -35,7 +35,7 @@ option(USE_GITHASH        "GIT_HASH"           ON)
 # This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell).
 option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON)
 
-# FLAGS for disabling optimizations
+# FLAGS for disabling optimizations and debugging
 option(FREE_VAR_RANGE_OPT  "FREE_VAR_RANGE_OPT"   ON)
 option(HAS_LOCAL_OPT       "HAS_LOCAL_OPT"        ON)
 option(ABSTRACTION_CACHE   "ABSTRACTION_CACHE"    ON)
@@ -45,6 +45,8 @@ option(ALPHA               "ALPHA FEATURES"       OFF)
 option(TRACK_CUSTOM_ALLOCATORS "TRACK_CUSTOM_ALLOCATORS" OFF)
 option(TRACK_LIVE_EXPRS    "TRACK_LIVE_EXPRS" OFF)
 option(CUSTOM_ALLOCATORS   "CUSTOM_ALLOCATORS" ON)
+option(SAVE_SNAPSHOT       "SAVE_SNAPSHOT" ON)
+option(SAVE_INFO           "SAVE_INFO" ON)
 
 # emacs site-lisp dir
 set(EMACS_LISP_DIR        "share/emacs/site-lisp/lean" CACHE STRING "emacs site-lisp dir")
@@ -89,6 +91,14 @@ if (NOT("${CUSTOM_ALLOCATORS}" MATCHES "ON"))
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_CUSTOM_ALLOCATORS")
 endif()
 
+if (NOT("${SAVE_SNAPSHOT}" MATCHES "ON"))
+  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_SNAPSHOT")
+endif()
+
+if (NOT("${SAVE_INFO}" MATCHES "ON"))
+  set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_INFO")
+endif()
+
 message(STATUS "Lean emacs-mode will be installed at "
   "${CMAKE_INSTALL_PREFIX}/${EMACS_LISP_DIR}")
 message(STATUS "Lean library will be installed at "
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index af0ef15e5c..11f2f1a15e 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -78,6 +78,9 @@ info_data mk_identifier_info(name const & full_id) { return info_data(new identi
 info_data mk_vm_obj_format_info(environment const & env, vm_obj const & thunk) { return info_data(new vm_obj_format_info(env, thunk)); }
 
 void info_manager::add_info(unsigned l, unsigned c, info_data data) {
+#ifdef LEAN_NO_INFO
+    return;
+#endif
     line_info_data_set line_set = m_line_data[l];
     line_set.insert(c, cons<info_data>(data, line_set[c]));
     m_line_data.insert(l, line_set);
@@ -99,6 +102,9 @@ void info_manager::instantiate_mvars(metavar_context const & mctx) {
 }
 
 void info_manager::merge(info_manager const & info) {
+#ifdef LEAN_NO_INFO
+    return;
+#endif
     info.m_line_data.for_each([&](unsigned line, line_info_data_set const & set) {
             set.for_each([&](unsigned col, list<info_data> const & data) {
                     buffer<info_data> b;
@@ -113,14 +119,23 @@ void info_manager::merge(info_manager const & info) {
 }
 
 void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) {
+#ifdef LEAN_NO_INFO
+    return;
+#endif
     add_info(l, c, mk_type_info(e));
 }
 
 void info_manager::add_identifier_info(unsigned l, unsigned c, name const & full_id) {
+#ifdef LEAN_NO_INFO
+    return;
+#endif
     add_info(l, c, mk_identifier_info(full_id));
 }
 
 void info_manager::add_vm_obj_format_info(unsigned l, unsigned c, environment const & env, vm_obj const & thunk) {
+#ifdef LEAN_NO_INFO
+    return;
+#endif
     add_info(l, c, mk_vm_obj_format_info(env, thunk));
 }
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index fa5680f8a2..0077463b02 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2489,6 +2489,9 @@ bool parser::curr_is_command_like() const {
 }
 
 void parser::save_snapshot(scope_message_context & smc, pos_info p) {
+#ifdef LEAN_NO_SNAPSHOT
+    return;
+#endif
     if (!m_snapshot_vector)
         return;
     if (m_snapshot_vector->empty() || m_snapshot_vector->back()->m_pos != p) {