From bf41d40b1d40914abde585cff921cc603f80e2d1 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Sat, 12 Jun 2021 23:28:22 -0700
Subject: [PATCH] fix: allow plugins to run IO initializers

---
 src/initialize/init.cpp |  7 +------
 src/shell/lean.cpp      | 14 +++-----------
 2 files changed, 4 insertions(+), 17 deletions(-)

diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
index 6d19e8b9ae..9bfc8af0f9 100644
--- a/src/initialize/init.cpp
+++ b/src/initialize/init.cpp
@@ -33,10 +33,6 @@ extern "C" void lean_initialize() {
     initialize_constructions_module();
 }
 
-void initialize() {
-    lean_initialize();
-}
-
 void finalize() {
     run_thread_finalizers();
     finalize_constructions_module();
@@ -50,8 +46,7 @@ void finalize() {
 }
 
 initializer::initializer() {
-    initialize();
-    lean::io_mark_end_initialization();
+    lean_initialize();
 }
 
 initializer::~initializer() {
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 3aa50ce909..6dd7ea334f 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -318,16 +318,6 @@ void load_plugin(std::string path) {
     // NOTE: we never unload plugins
 }
 
-class initializer {
-private:
-    lean::initializer m_init;
-public:
-    initializer() {
-    }
-    ~initializer() {
-    }
-};
-
 namespace lean {
 extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w);
 pair_ref<environment, object_ref> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) {
@@ -413,7 +403,7 @@ int main(int argc, char ** argv) {
     SetErrorMode(SEM_FAILCRITICALERRORS);
 #endif
     auto init_start = std::chrono::steady_clock::now();
-    ::initializer init;
+    lean::initializer init;
     second_duration init_time = std::chrono::steady_clock::now() - init_start;
     bool run = false;
     optional<std::string> olean_fn;
@@ -546,6 +536,8 @@ int main(int argc, char ** argv) {
         }
     }
 
+    lean::io_mark_end_initialization();
+
     if (print_prefix) {
         std::cout << get_io_result<string_ref>(lean_get_prefix(io_mk_world())).data() << std::endl;
         return 0;