feat: expose --load-dynlib functionality to Lean code

src/Lean.lean

@@ -30,4 +30,5 @@ import Lean.ScopedEnvExtension
 import Lean.DocString
 import Lean.DeclarationRange
 import Lean.LazyInitExtension
+import Lean.LoadDynlib
 import Lean.Widget

src/Lean/LoadDynlib.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lean
+
+/--
+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=lib` to `lean`.
+
+Note that Lean never unloads libraries.
+-/
+@[extern "lean_load_dynlib"]
+constant loadDynlib (path : @& System.FilePath) : IO Unit

src/runtime/CMakeLists.txt

@@ -1,6 +1,6 @@
 set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
-stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
+stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
 process.cpp object_ref.cpp mpn.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})

src/runtime/load_dynlib.cpp

@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura, Mac Malone
+*/
+#include "runtime/io.h"
+#include "runtime/object.h"
+#include "runtime/sstream.h"
+#include "runtime/exception.h"
+#include "runtime/load_dynlib.h"
+
+#ifdef LEAN_WINDOWS
+#include <windows.h>
+#undef ERROR // thanks, wingdi.h
+#else
+#include <dlfcn.h>
+#endif
+
+namespace lean {
+void load_dynlib(std::string path) {
+#ifdef LEAN_WINDOWS
+    HMODULE h = LoadLibrary(path.c_str());
+    if (!h) {
+        throw exception(sstream() << "error loading library " << path << ": " << GetLastError());
+    }
+#else
+    void *handle = dlopen(path.c_str(), RTLD_LAZY | RTLD_GLOBAL);
+    if (!handle) {
+        throw exception(sstream() << "error loading library, " << dlerror());
+    }
+#endif
+    // NOTE: we never unload libraries
+}
+
+/* loadDynlib : System.FilePath -> IO Unit */
+extern "C" LEAN_EXPORT obj_res lean_load_dynlib(b_obj_arg path, obj_arg) {
+    try {
+        load_dynlib(string_cstr(path));
+        return io_result_mk_ok(box(0));
+    } catch (exception & ex) {
+        return io_result_mk_error(ex.what());
+    }
+}
+}

src/runtime/load_dynlib.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Mac Malone
+*/
+#pragma once
+#include <string>
+
+namespace lean {
+void load_dynlib(std::string path);
+}

src/util/shell.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "runtime/thread.h"
 #include "runtime/debug.h"
 #include "runtime/sstream.h"
+#include "runtime/load_dynlib.h"
 #include "util/timer.h"
 #include "util/macros.h"
 #include "util/io.h"
@@ -320,21 +321,6 @@ void load_plugin(std::string path) {
     // NOTE: we never unload plugins
 }
 
-void load_library(std::string path) {
-#ifdef LEAN_WINDOWS
-    HMODULE h = LoadLibrary(path.c_str());
-    if (!h) {
-        throw exception(sstream() << "error loading library " << path << ": " << GetLastError());
-    }
-#else
-    void *handle = dlopen(path.c_str(), RTLD_LAZY | RTLD_GLOBAL);
-    if (!handle) {
-        throw exception(sstream() << "error loading library, " << dlerror());
-    }
-#endif
-    // NOTE: we never unload libraries
-}
-
 namespace lean {
 extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, uint32_t trust_level, 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, uint32_t trust_level) {
@@ -553,7 +539,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
                 break;
             case 'l':
                 check_optarg("l");
-                load_library(optarg);
+                lean::load_dynlib(optarg);
                 forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg)));
                 break;
             default: