fix(runtime): add init_module

src/init/init.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "runtime/stackinfo.h"
 #include "runtime/thread.h"
+#include "runtime/init_module.h"
 #include "util/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
@@ -25,6 +26,7 @@ Author: Leonardo de Moura
 namespace lean {
 void initialize() {
     save_stack_info();
+    initialize_runtime_module();
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
@@ -66,6 +68,7 @@ void finalize() {
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();
+    finalize_runtime_module();
     run_post_thread_finalizers();
 #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS
     std::cerr << "memory deallocated by memory_pool (after finalization): " << get_memory_deallocated() << "\n";

src/runtime/CMakeLists.txt

@@ -1,6 +1,6 @@
 set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp mpq.cpp utf8.cpp
 lean_obj.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
-serializer.cpp stackinfo.cpp)
+serializer.cpp stackinfo.cpp init_module.cpp)
 add_library(runtime OBJECT ${RUNTIME_OBJS})
 add_library(leanruntime ${RUNTIME_OBJS})
 

src/runtime/init_module.cpp

@@ -0,0 +1,21 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "runtime/debug.h"
+#include "runtime/serializer.h"
+#include "runtime/thread.h"
+namespace lean {
+void initialize_runtime_module() {
+    initialize_debug();
+    initialize_serializer();
+    initialize_thread();
+}
+void finalize_runtime_module() {
+    finalize_thread();
+    finalize_serializer();
+    finalize_debug();
+}
+}

src/runtime/init_module.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_runtime_module();
+void finalize_runtime_module();
+}

src/util/init_module.cpp

@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "runtime/debug.h"
-#include "runtime/serializer.h"
-#include "runtime/thread.h"
 #include "util/ascii.h"
 #include "util/name.h"
 #include "util/fresh_name.h"