max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: --load-dynlib

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-29 17:34:42 +02:00 • committed by Leonardo de Moura
parent 5a65189894
commit 4b51d00fcb
1 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/util/shell.cpp
View file

@ -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<environment, object_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);