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

fix: allow plugins to run IO initializers

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-06-12 23:28:22 -07:00 • committed by Leonardo de Moura
parent 51d26e1172
commit bf41d40b1d
2 changed files with 4 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/initialize/init.cpp
View file

@ -33,10 +33,6 @@ extern "C" void lean_initialize() {
initialize_constructions_module();
}
void initialize() {
lean_initialize();
}
void finalize() {
run_thread_finalizers();
finalize_constructions_module();
@ -50,8 +46,7 @@ void finalize() {
}
initializer::initializer() {
initialize();
lean::io_mark_end_initialization();
lean_initialize();
}
initializer::~initializer() {

14
src/shell/lean.cpp
View file

@ -318,16 +318,6 @@ void load_plugin(std::string path) {
// NOTE: we never unload plugins
}
class initializer {
private:
lean::initializer m_init;
public:
initializer() {
}
~initializer() {
}
};
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) {
@ -413,7 +403,7 @@ int main(int argc, char ** argv) {
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
auto init_start = std::chrono::steady_clock::now();
::initializer init;
lean::initializer init;
second_duration init_time = std::chrono::steady_clock::now() - init_start;
bool run = false;
optional<std::string> olean_fn;
@ -546,6 +536,8 @@ int main(int argc, char ** argv) {
}
}
lean::io_mark_end_initialization();
if (print_prefix) {
std::cout << get_io_result<string_ref>(lean_get_prefix(io_mk_world())).data() << std::endl;
return 0;