From b1d8a17f1b38e4e4b308a9cbfb06e53884591809 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 May 2018 20:38:06 -0700
Subject: [PATCH] fix(runtime): add init_module

---
 src/init/init.cpp           |  3 +++
 src/runtime/CMakeLists.txt  |  2 +-
 src/runtime/init_module.cpp | 21 +++++++++++++++++++++
 src/runtime/init_module.h   | 12 ++++++++++++
 src/util/init_module.cpp    |  3 ---
 5 files changed, 37 insertions(+), 4 deletions(-)
 create mode 100644 src/runtime/init_module.cpp
 create mode 100644 src/runtime/init_module.h

diff --git a/src/init/init.cpp b/src/init/init.cpp
index 0b16872ec4..7319bc0880 100644
--- a/src/init/init.cpp
+++ b/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";
diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt
index f7e71ad17f..454eb918c0 100644
--- a/src/runtime/CMakeLists.txt
+++ b/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})
 
diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp
new file mode 100644
index 0000000000..a1d609e138
--- /dev/null
+++ b/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();
+}
+}
diff --git a/src/runtime/init_module.h b/src/runtime/init_module.h
new file mode 100644
index 0000000000..b28dfb4cd2
--- /dev/null
+++ b/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();
+}
diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp
index de537dbdb5..a8ed8d1aeb 100644
--- a/src/util/init_module.cpp
+++ b/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"