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

fix: calling convention for module initializers

Browse source
This commit is contained in:
Mario Carneiro 2023-07-07 23:38:16 -04:00 • committed by Leonardo de Moura
parent 76023a7c6f
commit 51694cd6de
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/initialize/init.cpp
View file

@ -17,8 +17,8 @@ Author: Leonardo de Moura
#include "initialize/init.h"
namespace lean {
extern "C" object* initialize_Init(object* w);
extern "C" object* initialize_Lean(object* w);
extern "C" object* initialize_Init(uint8_t, object* w);
extern "C" object* initialize_Lean(uint8_t, 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
@ -26,8 +26,9 @@ these two calls, you may also have to run additional initializers for your own m
extern "C" LEAN_EXPORT void lean_initialize() {
save_stack_info();
initialize_util_module();
consume_io_result(initialize_Init(io_mk_world()));
consume_io_result(initialize_Lean(io_mk_world()));
uint8_t builtin = 1;
consume_io_result(initialize_Init(builtin, io_mk_world()));
consume_io_result(initialize_Lean(builtin, io_mk_world()));
initialize_kernel_module();
init_default_print_fn();
initialize_library_core_module();

4
src/util/shell.cpp
View file

@ -334,8 +334,8 @@ void load_plugin(std::string path) {
if (!init) {
throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module '" << pkg << "'");
}
auto init_fn = reinterpret_cast<object *(*)(object *)>(init);
object *r = init_fn(io_mk_world());
auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(init);
object *r = init_fn(1 /* builtin */, io_mk_world());
consume_io_result(r);
// NOTE: we never unload plugins
}