chore: document io_mark_end_initialization setup

src/initialize/init.cpp

@@ -20,6 +20,9 @@ namespace lean {
 extern "C" object* initialize_Init(object* w);
 extern "C" object* initialize_Lean(object* w);
 
+/* Initializes the Lean runtime. Before executing any code which uses the Lean package,
+you must first call this function, and then `lean::io_mark_end_initialization`. Inbetween
+these two calls, you may also have to run additional initializers for your own modules. */
 extern "C" void lean_initialize() {
     save_stack_info();
     initialize_util_module();
@@ -47,6 +50,9 @@ void finalize() {
 
 initializer::initializer() {
     lean_initialize();
+    /* Remark: We used to call `lean::io_mark_end_initialization` here, however this prevented
+    plugins from setting up global state such as environment extensions in their initializers.
+    See also `lean_initialize`. */
 }
 
 initializer::~initializer() {

src/shell/lean.cpp

@@ -423,6 +423,7 @@ int main(int argc, char ** argv) {
 #endif
 
     try {
+        // Remark: This currently runs under `IO.initializing = true`.
         init_search_path();
     } catch (lean::throwable & ex) {
         std::cerr << "error: " << ex.what() << std::endl;