refactor(util): explicit initialization/finalization

src/init/init.cpp

@@ -4,17 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/stackinfo.h"
 #include "util/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
 #include "kernel/inductive/inductive.h"
 #include "library/init_module.h"
 #include "library/tactic/init_module.h"
+#include "library/print.h"
 #include "frontends/lean/init_module.h"
+#include "frontends/lua/register_modules.h"
 #include "init/init.h"
 
 namespace lean {
 void initialize() {
+    save_stack_info();
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
@@ -22,6 +26,8 @@ void initialize() {
     initialize_library_module();
     initialize_tactic_module();
     initialize_frontend_lean_module();
+    init_default_print_fn();
+    register_modules();
 }
 void finalize() {
     finalize_frontend_lean_module();

src/shell/lean.cpp

@@ -28,13 +28,11 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/definition_cache.h"
 #include "library/declaration_index.h"
-#include "library/print.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/dependencies.h"
-#include "frontends/lua/register_modules.h"
 #include "init/init.h"
 #include "version.h"
 #include "githash.h" // NOLINT
@@ -195,9 +193,6 @@ options set_config_option(options const & opts, char const * in) {
 }
 
 int main(int argc, char ** argv) {
-    lean::save_stack_info();
-    lean::init_default_print_fn();
-    lean::register_modules();
     lean::initializer init;
     bool export_objects  = false;
     unsigned trust_lvl   = 0;

src/tests/util/thread.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/shared_mutex.h"
 #include "util/interrupt.h"
 #include "util/thread_script_state.h"
+#include "util/init_module.h"
 using namespace lean;
 
 #if defined(LEAN_MULTI_THREAD) && !defined(__APPLE__)
@@ -214,6 +215,7 @@ static void tst8() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
     tst1();
     tst2();
     tst3();
@@ -222,6 +224,7 @@ int main() {
     tst6();
     tst7();
     tst8();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
 #else

src/util/init_module.cpp

@@ -8,7 +8,10 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 #include "util/trace.h"
 #include "util/serializer.h"
+#include "util/thread_script_state.h"
+#include "util/script_state.h"
 #include "util/name.h"
+#include "util/name_generator.h"
 #include "util/lean_path.h"
 #include "util/thread.h"
 
@@ -16,18 +19,24 @@ namespace lean {
 void initialize_util_module() {
     initialize_debug();
     initialize_trace();
+    initialize_serializer();
     initialize_thread();
     initialize_ascii();
-    initialize_lean_path();
-    initialize_serializer();
+    initialize_thread_script_state();
+    initialize_script_state();
     initialize_name();
+    initialize_name_generator();
+    initialize_lean_path();
 }
 void finalize_util_module() {
-    finalize_name();
-    finalize_serializer();
     finalize_lean_path();
+    finalize_name_generator();
+    finalize_name();
+    finalize_script_state();
+    finalize_thread_script_state();
     finalize_ascii();
     finalize_thread();
+    finalize_serializer();
     finalize_trace();
     finalize_debug();
 }

src/util/memory.cpp

@@ -107,6 +107,7 @@ public:
     size_t size() const { return m_size; }
 };
 
+// TODO(Leo): use explicit initialization?
 static alloc_info                          g_global_memory;
 
 size_t     get_allocated_memory() { return g_global_memory.size(); }

src/util/name.cpp

@@ -154,17 +154,17 @@ name::~name() {
         m_ptr->dec_ref();
 }
 
-static name g_anonymous;
+static name * g_anonymous = nullptr;
 
 name const & name::anonymous() {
-    lean_assert(g_anonymous.is_anonymous());
-    return g_anonymous;
+    lean_assert(g_anonymous->is_anonymous());
+    return *g_anonymous;
 }
 
-static atomic<unsigned> g_next_id(0);
+static atomic<unsigned> * g_next_id = nullptr;
 
 name name::mk_internal_unique_name() {
-    unsigned id = g_next_id++;
+    unsigned id = (*g_next_id)++;
     return name(id);
 }
 
@@ -479,14 +479,6 @@ struct name_sd {
 };
 static name_sd * g_name_sd = nullptr;
 
-void initialize_name() {
-    g_name_sd = new name_sd();
-}
-
-void finalize_name() {
-    delete g_name_sd;
-}
-
 serializer & operator<<(serializer & s, name const & n) {
     s.get_extension<name_serializer>(g_name_sd->m_serializer_extid).write(n);
     return s;
@@ -622,5 +614,17 @@ void open_name(lua_State * L) {
 
     open_list_name(L);
 }
+
+void initialize_name() {
+    g_anonymous = new name();
+    g_name_sd   = new name_sd();
+    g_next_id   = new atomic<unsigned>(0);
+}
+
+void finalize_name() {
+    delete g_next_id;
+    delete g_name_sd;
+    delete g_anonymous;
+}
 }
 void print(lean::name const & n) { std::cout << n << std::endl; }

src/util/name_generator.cpp

@@ -26,10 +26,10 @@ void swap(name_generator & a, name_generator & b) {
 }
 
 DECL_UDATA(name_generator)
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
 static int mk_name_generator(lua_State * L) {
     if (lua_gettop(L) == 0)
-        return push_name_generator(L, name_generator(g_tmp_prefix));
+        return push_name_generator(L, name_generator(*g_tmp_prefix));
     else
         return push_name_generator(L, name_generator(to_name_ext(L, 1)));
 }
@@ -53,4 +53,12 @@ void open_name_generator(lua_State * L) {
     SET_GLOBAL_FUN(mk_name_generator,   "name_generator");
     SET_GLOBAL_FUN(name_generator_pred, "is_name_generator");
 }
+
+void initialize_name_generator() {
+    g_tmp_prefix = new name(name::mk_internal_unique_name());
+}
+
+void finalize_name_generator() {
+    delete g_tmp_prefix;
+}
 }

src/util/name_generator.h

@@ -39,4 +39,6 @@ void swap(name_generator & a, name_generator & b);
 
 UDATA_DEFS(name_generator)
 void open_name_generator(lua_State * L);
+void initialize_name_generator();
+void finalize_name_generator();
 }

src/util/script_state.cpp

@@ -25,9 +25,18 @@ Author: Leonardo de Moura
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
 namespace lean {
-static std::vector<script_state::reg_fn> g_modules;
+static std::vector<script_state::reg_fn> * g_modules = nullptr;
+
 void script_state::register_module(reg_fn f) {
-    g_modules.push_back(f);
+    g_modules->push_back(f);
+}
+
+void initialize_script_state() {
+    g_modules = new std::vector<script_state::reg_fn>();
+}
+
+void finalize_script_state() {
+    delete g_modules;
 }
 
 static unsigned g_check_interrupt_freq = 1048576;
@@ -91,7 +100,7 @@ struct script_state::imp {
         open_rb_map(m_state);
         open_extra(m_state);
 
-        for (auto f : g_modules) {
+        for (auto f : *g_modules) {
             f(m_state);
         }
     }

src/util/script_state.h

@@ -60,4 +60,6 @@ public:
    \brief Return a reference to the script_state object that is wrapping \c L.
 */
 script_state to_script_state(lua_State * L);
+void initialize_script_state();
+void finalize_script_state();
 }

src/util/thread_script_state.cpp

@@ -15,25 +15,31 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct script_state_manager {
-    static bool                          g_alive;
     mutex                                m_code_mutex;
     std::vector<pair<bool, std::string>> m_code;
     mutex                                m_state_mutex;
     std::vector<script_state>            m_states;
     std::vector<script_state>            m_available_states;
-    script_state_manager() { g_alive = true; }
-    ~script_state_manager() { g_alive = false; }
-    static bool is_alive() { return g_alive; }
+    script_state_manager() {}
+    ~script_state_manager() {}
 };
 
-script_state_manager & get_script_state_manager() {
-    static script_state_manager m;
-    return m;
+static script_state_manager * g_manager = nullptr;
+
+void initialize_thread_script_state() {
+    g_manager = new script_state_manager();
 }
 
-// make sure it is initialize at startup.
-static script_state_manager & g_aux = get_script_state_manager();
-bool script_state_manager::g_alive  = true;
+void finalize_thread_script_state() {
+    delete g_manager;
+    g_manager = nullptr;
+}
+
+static script_state_manager & get_script_state_manager() {
+    return *g_manager;
+}
+
+static bool is_manager_alive() { return g_manager; }
 
 /** \brief Execute \c code in all states in the pool */
 void system_dostring(char const * code) {
@@ -101,7 +107,7 @@ static script_state get_state() {
 }
 
 static void recycle_state(script_state s) {
-    if (script_state_manager::is_alive()) {
+    if (is_manager_alive()) {
         script_state_manager & m = get_script_state_manager();
         lock_guard<mutex> lk(m.m_state_mutex);
         m.m_available_states.push_back(s);

src/util/thread_script_state.h

@@ -40,4 +40,6 @@ script_state get_thread_script_state();
 void release_thread_script_state();
 
 void enable_script_state_recycling(bool flag);
+void initialize_thread_script_state();
+void finalize_thread_script_state();
 }