From 7696c28fe16873a91f8072fe36dcfc826a1eb8a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 May 2019 11:10:49 -0700 Subject: [PATCH] feat(library/module): module manager in Lean is alive --- src/library/module.cpp | 250 +++++++---------------------------------- 1 file changed, 41 insertions(+), 209 deletions(-) diff --git a/src/library/module.cpp b/src/library/module.cpp index 816b7c1419..064877eb05 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -136,21 +136,28 @@ void register_module_object_reader(std::string const & k, module_modification_re static char const * g_olean_end_file = "EndFile"; extern "C" object * lean_serialize_modifications(object * mod_list, object * w) { - object_ref mod(mod_list); + object_ref mod_list_ref(mod_list); try { std::ostringstream out(std::ios_base::binary); serializer s(out); - + buffer mod_buffer; while (!is_scalar(mod_list)) { - to_modification(cnstr_get(mod_list, 0)).serialize(s); + mod_buffer.push_back(cnstr_get(mod_list, 0)); mod_list = cnstr_get(mod_list, 1); } - + size_t i = mod_buffer.size(); + while (i > 0) { + --i; + modification & mod = to_modification(mod_buffer[i]); + s << std::string(mod.get_key()); + mod.serialize(s); + } s << g_olean_end_file; std::string bytes = out.str(); object * r = alloc_sarray(1, bytes.size(), bytes.size()); memcpy(sarray_cptr(r), bytes.data(), bytes.size()); + return set_io_result(w, r); } catch (exception & ex) { return set_io_error(w, ex.what()); @@ -191,102 +198,44 @@ extern "C" object * lean_perform_serialized_modifications(object * env0, object // ======================================= -struct module_ext : public environment_extension { - std::vector m_direct_imports; -}; +/* +@[export lean.write_module_core] +def writeModule (env : Environment) (fname : String) : IO Unit := */ +object * write_module_core(object * env, object * fname, object * w); -struct module_ext_reg { - unsigned m_ext_id; - module_ext_reg() { m_ext_id = environment::register_extension(new module_ext()); } -}; - -static module_ext_reg * g_ext = nullptr; - -static module_ext const & get_extension(environment const & env) { - return static_cast(env.get_extension(g_ext->m_ext_id)); +void write_module(environment const & env, std::string const & olean_fn) { + object * r = write_module_core(env.get_obj_arg(), mk_string(olean_fn), io_mk_world()); + if (io_result_is_error(r)) { + dec_ref(r); + throw exception(sstream() << "failed to write module '" << olean_fn << "'"); + } else { + dec_ref(r); + } } -static environment update(environment const & env, module_ext const & ext) { - return env.update(g_ext->m_ext_id, new module_ext(ext)); -} +/* +@[export lean.import_modules_core] +def importModules (modNames : List Name) (trustLevel : UInt32 := 0) : IO Environment := +*/ +object * import_modules_core(object * mod_names, uint32 trust_level, object * w); -static unsigned olean_hash(std::string const & data) { - return hash(data.size(), [&] (unsigned i) { return static_cast(data[i]); }); +environment import_modules(unsigned trust_lvl, std::vector const & imports) { + names mods(imports.begin(), imports.end()); + object * r = import_modules_core(mods.steal(), trust_lvl, io_mk_world()); + if (io_result_is_error(r)) { + dec_ref(r); + io_result_show_error(r); // TODO(Leo): move to exception + throw exception("failed to import modules"); + } else { + environment env(io_result_get_value(r), true); + dec_ref(r); + return env; + } } object * environment_add_modification_core(object * env, object * mod); object * environment_get_modifications_core(object * env); -void write_module(environment const & env, std::string const & olean_fn) { - exclusive_file_lock output_lock(olean_fn); - std::ofstream out(olean_fn, std::ios_base::binary); - module_ext const & ext = get_extension(env); - - buffer mods; - object * mod_list = environment_get_modifications_core(env.get_obj_arg()); - while (!is_scalar(mod_list)) { - object * mod = cnstr_get(mod_list, 0); - mods.push_back(&to_modification(mod)); - mod_list = cnstr_get(mod_list, 1); - } - - std::ostringstream out1(std::ios_base::binary); - serializer s1(out1); - - // store objects - for (int i = mods.size() - 1; i >= 0; i--) { - s1 << std::string(mods[i]->get_key()); - mods[i]->serialize(s1); - } - - dec(mod_list); - - s1 << g_olean_end_file; - - if (!out1.good()) { - throw exception(sstream() << "error during serialization"); - } - - std::string r = out1.str(); - unsigned h = olean_hash(r); - - serializer s2(out); - s2 << g_olean_header << get_version_string(); - s2 << h; - // store imported files - s2 << static_cast(ext.m_direct_imports.size()); - for (auto m : ext.m_direct_imports) - s2 << m; - // store object code - s2.write_blob(r); - - out.close(); - if (!out) throw exception("failed to write olean file"); -} - - -struct decl_modification : public modification { - LEAN_MODIFICATION("decl") - declaration m_decl; - - decl_modification() {} - decl_modification(declaration const & decl): - m_decl(decl) {} - - void perform(environment & env) const override { - env = env.add(m_decl, false); - } - - void serialize(serializer & s) const override { - s << m_decl; - } - - static modification* deserialize(deserializer & d) { - auto decl = read_declaration(d); - return new decl_modification(std::move(decl)); - } -}; - namespace module { environment add(environment const & env, modification* modf) { return environment(environment_add_modification_core(env.get_obj_arg(), to_object(modf))); @@ -299,135 +248,18 @@ environment add_and_perform(environment const & env, modification * modf) { } environment add(environment const & env, declaration const & d, bool check) { - environment new_env = env.add(d, check); - return add(new_env, new decl_modification(d)); + return env.add(d, check); } } // end of namespace module -struct olean_data { - std::vector m_imports; - std::string m_serialized_modifications; -}; -static olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash) { - std::vector imports; - time_task t(".olean deserialization", - message_builder(environment(), get_global_ios(), file_name, pos_info(), message_severity::INFORMATION)); - - deserializer d1(in, optional(file_name)); - std::string header, version; - unsigned claimed_hash; - d1 >> header; - if (header != g_olean_header) - throw exception(sstream() << "file '" << file_name << "' does not seem to be a valid object Lean file, invalid header"); - d1 >> version >> claimed_hash; -#ifndef LEAN_IGNORE_OLEAN_VERSION - if (version != get_version_string()) { - throw exception(sstream() << "error importing file '" << file_name << "', it is from a different Lean version"); - } -#endif - - unsigned num_imports = d1.read_unsigned(); - for (unsigned i = 0; i < num_imports; i++) { - module_name r; - d1 >> r; - imports.push_back(r); - } - - auto code = d1.read_blob(); - - if (!in.good()) { - throw exception(sstream() << "file '" << file_name << "' has been corrupted"); - } - - if (check_hash) { - unsigned computed_hash = olean_hash(code); - if (claimed_hash != computed_hash) - throw exception(sstream() << "file '" << file_name << "' has been corrupted, checksum mismatch"); - } - - return { imports, code }; -} - -using modification_list = std::vector; - -static void import_module(modification_list const & modifications, environment & env) { - for (auto & m : modifications) { - m->perform(env); - } -} - -modification_list parse_olean_modifications(std::string const & olean_code, std::string const & file_name) { - modification_list ms; - std::istringstream in(olean_code, std::ios_base::binary); - deserializer d(in, optional(file_name)); - object_readers & readers = get_object_readers(); - unsigned obj_counter = 0; - while (true) { - std::string k; - unsigned offset = in.tellg(); - d >> k; - if (k == g_olean_end_file) { - break; - } - - auto it = readers.find(k); - if (it == readers.end()) - throw exception(sstream() << "file '" << file_name << "' has been corrupted at offset " << offset - << ", unknown object: " << k); - ms.emplace_back(it->second(d)); - - obj_counter++; - } - if (!in.good()) { - throw exception(sstream() << "file '" << file_name << "' has been corrupted"); - } - return ms; -} - -static void import_module_rec(environment & env, module_name const & mod, name_set & already_imported) { - if (already_imported.contains(mod)) - return; - auto olean_fn = find_file(*g_search_path, mod, {".olean"}); - olean_data parsed_olean; - { - shared_file_lock olean_lock(olean_fn); - std::ifstream in2(olean_fn, std::ios_base::binary); - bool check_hash = false; - parsed_olean = parse_olean(in2, olean_fn, check_hash); - } - - for (auto & dep : parsed_olean.m_imports) { - import_module_rec(env, dep, already_imported); - } - import_module(parse_olean_modifications(parsed_olean.m_serialized_modifications, olean_fn), env); - - already_imported.insert(mod); -} - -environment import_modules(unsigned trust_lvl, std::vector const & imports) { - name_set already_imported; - environment env(trust_lvl); - - for (auto & import : imports) - import_module_rec(env, import, already_imported); - - module_ext ext = get_extension(env); - ext.m_direct_imports = imports; - return update(env, ext); -} - void initialize_module() { g_modification_class = register_external_object_class(modification_finalizer, modification_foreach); - g_ext = new module_ext_reg(); g_object_readers = new object_readers(); g_search_path = new search_path(); - decl_modification::init(); } void finalize_module() { - decl_modification::finalize(); delete g_object_readers; - delete g_ext; delete g_search_path; } }