feat(frontends/lean): add option 'max_memory'

Default value is 512Mb

src/frontends/lean/parser.cpp

@@ -215,6 +215,17 @@ expr parser::mk_by(expr const & t, pos_info const & pos) {
 void parser::updt_options() {
     m_verbose     = get_verbose(m_ios.get_options());
     m_show_errors = get_parser_show_errors(m_ios.get_options());
+    try {
+        set_max_memory_megabyte(get_max_memory(m_ios.get_options()));
+    } catch (exception&) {
+        if (m_ios.get_options().contains(get_max_memory_opt_name())) {
+            static bool m_already_reported = false;
+            if (!m_already_reported) {
+                m_already_reported = true;
+                throw;
+            }
+        }
+    }
 }
 
 void parser::display_warning_pos(unsigned line, unsigned pos) {

src/shell/lean.cpp

@@ -406,7 +406,8 @@ int main(int argc, char ** argv) {
             index_name = optarg;
             gen_index  = true;
         case 'M':
-            lean::set_max_memory(atoi(optarg)*1024*1024);
+            lean::set_max_memory_megabyte(atoi(optarg));
+            opts = opts.update(lean::get_max_memory_opt_name(), atoi(optarg));
             break;
         case 't':
             trust_lvl = atoi(optarg);
@@ -418,7 +419,7 @@ int main(int argc, char ** argv) {
             tmode = keep_theorem_mode::DiscardAll;
             break;
         case 'q':
-            opts = opts.update("verbose", false);
+            opts = opts.update(lean::get_verbose_opt_name(), false);
             break;
         case 'd':
             only_deps = true;

src/util/memory.cpp

@@ -8,6 +8,15 @@ Author: Leonardo de Moura
 #include <cstdlib>
 #include <iostream>
 #include "util/exception.h"
+#include "util/memory.h"
+
+namespace lean {
+void set_max_memory_megabyte(unsigned max) {
+    size_t m = max;
+    m *= 1024 * 1024;
+    set_max_memory(m);
+}
+}
 
 #if !defined(LEAN_TRACK_MEMORY)
 namespace lean {

src/util/memory.h

@@ -8,7 +8,10 @@ Author: Leonardo de Moura
 #include <cstdlib>
 
 namespace lean {
+/** \brief Set maximum amount of memory in bytes */
 void set_max_memory(size_t max);
+/** \brief Set maximum amount of memory in megabytes */
+void set_max_memory_megabyte(unsigned max);
 void check_memory(char const * component_name);
 size_t get_allocated_memory();
 void * malloc(size_t sz);

src/util/sexpr/options.cpp

@@ -15,22 +15,43 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_VERBOSE true
 #endif
 
+#ifndef LEAN_DEFAULT_MAX_MEMORY
+#define LEAN_DEFAULT_MAX_MEMORY 512 // 512Mb
+#endif
+
+
 namespace lean {
-static name * g_verbose = nullptr;
+static name * g_verbose    = nullptr;
+static name * g_max_memory = nullptr;
 
 void initialize_options() {
-    g_verbose = new name("verbose");
+    g_verbose    = new name("verbose");
+    g_max_memory = new name("max_memory");
     register_bool_option(*g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages");
+    register_unsigned_option(*g_max_memory, LEAN_DEFAULT_MAX_MEMORY, "maximum amount of memory available for Lean in megabytes");
 }
 
 void finalize_options() {
     delete g_verbose;
+    delete g_max_memory;
+}
+
+name const & get_verbose_opt_name() {
+    return *g_verbose;
+}
+
+name const & get_max_memory_opt_name() {
+    return *g_max_memory;
 }
 
 bool get_verbose(options const & opts) {
     return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE);
 }
 
+unsigned get_max_memory(options const & opts) {
+    return opts.get_unsigned(*g_max_memory, LEAN_DEFAULT_MAX_MEMORY);
+}
+
 std::ostream & operator<<(std::ostream & out, option_kind k) {
     switch (k) {
     case BoolOption: out << "Bool"; break;

src/util/sexpr/options.h

@@ -87,6 +87,9 @@ public:
     friend bool operator==(options const & a, options const & b) { return a.m_value == b.m_value; }
 };
 bool get_verbose(options const & opts);
+unsigned get_max_memory(options const & opts);
+name const & get_verbose_opt_name();
+name const & get_max_memory_opt_name();
 
 inline options read_options(deserializer & d) { return options(read_sexpr(d)); }
 inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; }

tests/lean/run/max_memory.lean

@@ -0,0 +1 @@
+set_option max_memory 40