doc: info on RTLD_GLOBAL and symbol clashes

src/Lean/LoadDynlib.lean

@@ -13,7 +13,10 @@ Dynamically loads a shared library so that its symbols can be used by
 the Lean interpreter (e.g., for interpreting `@[extern]` declarations).
 Equivalent to passing `--load-dynlib=path` to `lean`.
 
-Lean never unloads libraries.
+**Lean never unloads libraries.** Attempting to load a library that defines
+symbols shared with a previously loaded library (including itself) will error.
+If multiple libraries share common symbols, those symbols should be linked
+and loaded as separate libraries.
 -/
 @[extern "lean_load_dynlib"]
 opaque loadDynlib (path : @& System.FilePath) : IO Unit
@@ -32,7 +35,10 @@ Lean environment initializers, such as definitions calling
 To enable them, use `loadPlugin` within a `withImporting` block. This will
 set  `Lean.initializing` (but not `IO.initializing`).
 
-Lean never unloads plugins.
+**Lean never unloads plugins.** Attempting to load a plugin that defines
+symbols shared with a previously loaded plugin (including itself) will error.
+If multiple plugins share common symbols (e.g., imports), those symbols
+should be linked and loaded separately.
 -/
 @[extern "lean_load_plugin"]
 opaque loadPlugin (path : @& System.FilePath) : IO Unit

src/runtime/load_dynlib.cpp

@@ -91,6 +91,10 @@ extern "C" LEAN_EXPORT obj_res lean_load_plugin(b_obj_arg path, obj_arg) {
     }
     init = reinterpret_cast<void *>(GetProcAddress(h, sym.c_str()));
 #else
+    // Like lean_load_dynlib, the library is loaded with RTLD_GLOBAL.
+    // This ensures the interpreter has access to plugin definitions that are also
+    // imported (e.g., an environment extension defined with builtin_initialize).
+    // It also means that loading multiple plugins which define the same symbol will error.
     void *handle = dlopen(rpath.c_str(), RTLD_LAZY | RTLD_GLOBAL);
     if (!handle) {
         return io_result_mk_error((sstream()