diff --git a/src/util/shell.cpp b/src/util/shell.cpp index b18fc3b5eb..b15201f905 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -201,7 +201,8 @@ static void display_help(std::ostream & out) { std::cout << " --server start lean in server mode\n"; std::cout << " --worker start lean in server-worker mode\n"; #endif - std::cout << " --plugin=file load and initialize shared library for registering linters etc.\n"; + std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n"; + std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n"; std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --print-prefix print the installation prefix for Lean and exit\n"; std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n"; @@ -240,6 +241,7 @@ static struct option g_long_options[] = { {"worker", no_argument, 0, 'W'}, #endif {"plugin", required_argument, 0, 'p'}, + {"load-dynlib", required_argument, 0, 'l'}, {"print-prefix", no_argument, &print_prefix, 1}, {"print-libdir", no_argument, &print_libdir, 1}, #ifdef LEAN_DEBUG @@ -318,6 +320,21 @@ 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); + } +#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, object * w); pair_ref run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) { @@ -534,6 +551,11 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { load_plugin(optarg); forwarded_args.push_back(string_ref("--plugin=" + std::string(optarg))); break; + case 'l': + check_optarg("l"); + load_library(optarg); + forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg))); + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr);