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

fix(init/init.cpp): initialization bug

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-11 17:21:42 -07:00
parent 06390337c6
commit 2cd2bec831
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/init/init.cpp
View file

@ -38,7 +38,6 @@ void initialize() {
initialize_frontend_lean_module();
object * w = initialize_init_default(io_mk_world());
w = initialize_init_lean_default(w);
lean::io_mark_end_initialization();
if (io_result_is_error(w)) {
io_result_show_error(w);
dec(w);
@ -84,6 +83,7 @@ void finalize() {
initializer::initializer() {
initialize();
lean::io_mark_end_initialization();
}
initializer::~initializer() {

4
src/runtime/io.cpp
View file

@ -56,7 +56,9 @@ static obj_res option_of_io_result(obj_arg r) {
}
static bool g_initializing = true;
void io_mark_end_initialization() { g_initializing = false; }
void io_mark_end_initialization() {
g_initializing = false;
}
extern "C" obj_res lean_io_initializing(obj_arg r) {
return set_io_result(r, box(g_initializing));