diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index ea232146be..fad1a6ffed 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1165,17 +1165,19 @@ static void to_string_buffer(lua_State * L, int i, buffer & r) { } static int import_modules(environment const & env, lua_State * L, int s) { + int nargs = lua_gettop(L); buffer mnames; to_string_buffer(L, s, mnames); unsigned num_threads = 1; - int nargs = lua_gettop(L); + bool keep_proofs = false; if (nargs > s) num_threads = lua_tonumber(L, s+1); - - if (nargs > s + 1 && is_io_state(L, s+2)) - return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, to_io_state(L, s+2))); + if (nargs > s+1) + keep_proofs = lua_toboolean(L, s+2); + if (nargs > s+2 && is_io_state(L, s+3)) + return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, to_io_state(L, s+3))); else - return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, get_io_state(L))); + return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, get_io_state(L))); } static int import_modules(lua_State * L) { diff --git a/src/library/module.cpp b/src/library/module.cpp index 7c7c4c48bf..63a98a3a11 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -107,30 +107,6 @@ environment add(environment const & env, std::string const & k, std::function & add_asynch_update, - std::function &) { - declaration decl = read_declaration(d, midx); - environment env = senv.env(); - if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { - senv.add(decl); - } else if (LEAN_ASYNCH_IMPORT_THEOREM && decl.is_theorem()) { - // First, we add the theorem as an axiom, and create an asychronous task for - // checking the actual theorem, and replace the axiom with the actual theorem. - certified_declaration tmp_c = check(env, mk_axiom(decl.get_name(), decl.get_params(), decl.get_type())); - senv.add(tmp_c); - add_asynch_update([=](shared_environment & senv) { - certified_declaration c = check(env, decl); - senv.replace(c); - }); - } else { - certified_declaration c = check(env, decl); - senv.add(c); - } -} - -static register_module_object_reader_fn g_reg_decl_reader(g_decl, declaration_reader); - environment add(environment const & env, certified_declaration const & d) { environment new_env = env.add(d); declaration _d = d.get_declaration(); @@ -174,6 +150,7 @@ struct import_modules_fn { typedef std::tuple delayed_update; shared_environment m_senv; unsigned m_num_threads; + bool m_keep_proofs; io_state m_ios; mutex m_asynch_mutex; condition_variable m_asynch_cv; @@ -195,8 +172,8 @@ struct import_modules_fn { typedef std::shared_ptr module_info_ptr; std::unordered_map m_module_info; - import_modules_fn(environment const & env, unsigned num_threads, io_state const & ios): - m_senv(env), m_num_threads(num_threads), m_ios(ios), + import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios): + m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios), m_import_counter(0), m_all_modules_imported(false) { if (m_num_threads == 0) m_num_threads = 1; @@ -273,6 +250,41 @@ struct import_modules_fn { add_asynch_task([=](shared_environment &) { import_module(r); }); } + declaration theorem2axiom(declaration const & decl) { + lean_assert(decl.is_theorem()); + return mk_axiom(decl.get_name(), decl.get_params(), decl.get_type()); + } + + void import_decl(deserializer & d, module_idx midx) { + declaration decl = read_declaration(d, midx); + environment env = m_senv.env(); + if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { + if (!m_keep_proofs && decl.is_theorem()) + m_senv.add(theorem2axiom(decl)); + else + m_senv.add(decl); + } else if (LEAN_ASYNCH_IMPORT_THEOREM && decl.is_theorem()) { + // First, we add the theorem as an axiom, and create an asychronous task for + // checking the actual theorem, and replace the axiom with the actual theorem. + certified_declaration tmp_c = check(env, theorem2axiom(decl)); + m_senv.add(tmp_c); + add_asynch_task([=](shared_environment & m_senv) { + certified_declaration c = check(env, decl); + if (m_keep_proofs) + m_senv.replace(c); + }); + } else { + if (!m_keep_proofs && decl.is_theorem()) { + // check theorem, but add an axiom + check(env, decl); + m_senv.add(check(env, theorem2axiom(decl))); + } else { + certified_declaration c = check(env, decl); + m_senv.add(c); + } + } + } + void import_module(module_info_ptr const & r) { std::string s(r->m_obj_code.data(), r->m_obj_code.size()); std::istringstream in(s, std::ios_base::binary); @@ -291,14 +303,16 @@ struct import_modules_fn { d >> k; if (k == g_olean_end_file) { break; + } else if (k == g_decl) { + import_decl(d, r->m_module_idx); } else { object_readers & readers = get_object_readers(); auto it = readers.find(k); if (it == readers.end()) throw exception(sstream() << "file '" << r->m_fname << "' has been corrupted"); it->second(d, r->m_module_idx, m_senv, add_asynch_update, add_delayed_update); - obj_counter++; } + obj_counter++; } if (atomic_fetch_sub_explicit(&m_import_counter, 1u, memory_order_relaxed) == 1u) { m_all_modules_imported = true; @@ -404,12 +418,12 @@ struct import_modules_fn { }; environment import_modules(environment const & env, unsigned num_modules, std::string const * modules, - unsigned num_threads, io_state const & ios) { - return import_modules_fn(env, num_threads, ios)(num_modules, modules); + unsigned num_threads, bool keep_proofs, io_state const & ios) { + return import_modules_fn(env, num_threads, keep_proofs, ios)(num_modules, modules); } environment import_module(environment const & env, std::string const & module, - unsigned num_threads, io_state const & ios) { - return import_modules(env, 1, &module, num_threads, ios); + unsigned num_threads, bool keep_proofs, io_state const & ios) { + return import_modules(env, 1, &module, num_threads, keep_proofs, ios); } } diff --git a/src/library/module.h b/src/library/module.h index 80f71820c2..5cbff89597 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -17,11 +17,14 @@ namespace lean { \brief Return an environment based on \c env, where all modules in \c modules are imported. Modules included directly or indirectly by them are also imported. The environment \c env is usually an empty environment. + + If \c keep_proofs is false, then the proof of the imported theorems is discarded after being + checked. The idea is to save memory. */ environment import_modules(environment const & env, unsigned num_modules, std::string const * modules, - unsigned num_threads, io_state const & ios); + unsigned num_threads, bool keep_proofs, io_state const & ios); environment import_module(environment const & env, std::string const & module, - unsigned num_threads, io_state const & ios); + unsigned num_threads, bool keep_proofs, io_state const & ios); /** \brief Store/Export module using \c env to the output stream \c out. diff --git a/tests/lua/mod1.lua b/tests/lua/mod1.lua index f7ad7ef5bb..44df95ef3c 100644 --- a/tests/lua/mod1.lua +++ b/tests/lua/mod1.lua @@ -8,7 +8,7 @@ assert(env:get("H2"):is_theorem()) env = add_decl(env, mk_definition("B", Bool, A)) env:export("mod1_mod.olean") -local env2 = import_modules("mod1_mod.olean") +local env2 = import_modules("mod1_mod.olean", 1, true) assert(env2:get("A"):type() == Bool) assert(env2:get("A"):is_var_decl()) assert(env2:get("H1"):type() == A) @@ -19,3 +19,14 @@ assert(env2:get("H2"):value() == H1) assert(env2:get("B"):type() == Bool) assert(env2:get("B"):value() == A) assert(env2:get("B"):is_definition()) + +local env3 = import_modules("mod1_mod.olean") +assert(env3:get("A"):type() == Bool) +assert(env3:get("A"):is_var_decl()) +assert(env3:get("H1"):type() == A) +assert(env3:get("H1"):is_axiom()) +assert(env3:get("H2"):type() == A) +assert(env3:get("H2"):is_axiom()) +assert(env3:get("B"):type() == Bool) +assert(env3:get("B"):value() == A) +assert(env3:get("B"):is_definition()) diff --git a/tests/lua/slow/mod2.lua b/tests/lua/slow/mod2.lua index 2e20620713..119e1639bb 100644 --- a/tests/lua/slow/mod2.lua +++ b/tests/lua/slow/mod2.lua @@ -37,7 +37,7 @@ end print("importing...") local initt = os.clock() -local env2 = import_modules(mod_names, 4) +local env2 = import_modules(mod_names, 4, true) print(string.format("elapsed time: %.2f\n", os.clock() - initt)) for i = 1, NumMods do for j = 1, NumThs do