From 43e57358af85d90ab9b735714e4962785f0ee10f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 11 Sep 2018 12:58:53 -0700 Subject: [PATCH] refactor(library/module_mgr): minor refactorings --- src/library/module.h | 2 + src/library/module_mgr.cpp | 114 +++++++++++++++++-------------------- src/library/module_mgr.h | 24 +++----- src/util/lean_path.cpp | 26 +-------- tests/lean/leanpkg.path | 2 +- 5 files changed, 62 insertions(+), 106 deletions(-) diff --git a/src/library/module.h b/src/library/module.h index ac25801ab1..b228510aa2 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -24,12 +24,14 @@ public: struct modification; using modification_list = std::vector>; + /** \brief A finished module. The in-memory representation of a .olean file. */ struct loaded_module { module_name m_name; // not serialized std::vector m_imports; modification_list m_modifications; }; + /** \brief Mapping from module name to module. Used to separate this file from the module_mgr. */ using module_loader = std::function (module_name const &)>; diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index dfe0a7140d..022f6ea7cd 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -18,10 +18,10 @@ Authors: Gabriel Ebner, Sebastian Ullrich namespace lean { module_loader module_mgr::mk_loader() { - return [this](module_name const & n) { return get_module(n)->m_result.m_loaded_module; }; // NOLINT + return [this](module_name const & n) { return get_module(n)->m_loaded_module; }; // NOLINT } -static std::pair> +static std::shared_ptr load_module(search_path const & path, module_name const & mod_name, bool can_use_olean) { auto lean_fn = find_file(path, mod_name, {".lean"}); auto lean_mtime = get_mtime(lean_fn); @@ -33,38 +33,29 @@ load_module(search_path const & path, module_name const & mod_name, bool can_use if (olean_mtime != -1 && olean_mtime >= lean_mtime && can_use_olean && is_candidate_olean_file(olean_fn)) { - auto mod = std::make_shared(mod_name, - read_file(olean_fn, std::ios_base::binary), module_src::OLEAN, olean_mtime); - return std::make_pair(olean_fn, mod); + return std::make_shared(mod_name, olean_fn, module_src::OLEAN, olean_mtime); } } catch (exception) {} - return std::make_pair(lean_fn, std::make_shared(mod_name, read_file(lean_fn), module_src::LEAN, lean_mtime)); + return std::make_shared(mod_name, lean_fn, module_src::LEAN, lean_mtime); } static void compile_olean(search_path const & path, std::shared_ptr const & mod) { - if (mod->m_compiled_olean) + lean_assert(mod->m_source == module_src::LEAN); + if (mod->m_log.has_errors()) return; - mod->m_compiled_olean = true; - for (auto & dep : mod->m_deps) - if (dep.m_mod_info) - compile_olean(path, dep.m_mod_info); - - if (mod->m_source != module_src::LEAN || mod->m_log.has_errors()) - return; - auto res = mod->m_result; auto olean_fn = olean_of_lean(find_file(path, mod->m_name, {".lean"})); exclusive_file_lock output_lock(olean_fn); std::ofstream out(olean_fn, std::ios_base::binary); - write_module(*res.m_loaded_module, out); + write_module(*mod->m_loaded_module, out); out.close(); if (!out) throw exception("failed to write olean file"); } -void module_mgr::build_module(module_name const & mod_name, bool can_use_olean, name_set module_stack) { +time_t module_mgr::build_module(module_name const & mod_name, bool can_use_olean, name_set module_stack) { if (auto const & existing_mod = m_modules.find(mod_name)) - return; + return (*existing_mod)->m_mtime; auto orig_module_stack = module_stack; if (module_stack.contains(mod_name)) { @@ -75,68 +66,64 @@ void module_mgr::build_module(module_name const & mod_name, bool can_use_olean, scope_global_ios scope_ios(m_ios); scope_traces_as_messages scope_trace_msgs(mod_name.to_string(), {1, 0}); - std::string file_name; std::shared_ptr mod; - std::tie(file_name, mod) = load_module(m_path, mod_name, can_use_olean); + auto mod = load_module(m_path, mod_name, can_use_olean); scope_message_log scope_log(mod->m_log); - if (mod->m_source == module_src::OLEAN) { - std::istringstream in2(mod->m_contents, std::ios_base::binary); - bool check_hash = false; - auto parsed_olean = parse_olean(in2, file_name, check_hash); - // we never need to re-parse .olean files, so discard content - mod->m_contents.clear(); - mod->m_trans_mtime = mod->m_mtime; + if (mod->m_source == module_src::OLEAN) { + std::ifstream in2(mod->m_filename, std::ios_base::binary); + bool check_hash = false; + auto parsed_olean = parse_olean(in2, mod->m_filename, check_hash); + auto max_mtime = mod->m_mtime; - for (auto & d : parsed_olean.m_imports) { - build_module(d, true, module_stack); + for (auto & d : parsed_olean.m_imports) { + max_mtime = std::max(max_mtime, build_module(d, true, module_stack)); - auto const & d_mod = *m_modules.find(d); - mod->m_deps.push_back({ d, d_mod }); - mod->m_trans_mtime = std::max(mod->m_trans_mtime, d_mod->m_trans_mtime); - } - - if (mod->m_trans_mtime > mod->m_mtime) - return build_module(mod_name, false, orig_module_stack); - - mod->m_compiled_olean = true; - module_info::parse_result res; - - auto deps = mod->m_deps; - loaded_module lm { - mod_name, parsed_olean.m_imports, - parse_olean_modifications(parsed_olean.m_serialized_modifications, file_name) }; - res.m_loaded_module = std::make_shared(lm); - - mod->m_result = res; - m_modules[mod_name] = mod; - } else if (mod->m_source == module_src::LEAN) { - build_lean(mod, file_name, module_stack); - m_modules[mod_name] = mod; - } else { - throw exception("unknown module source"); + auto const & d_mod = *m_modules.find(d); + mod->m_deps.push_back({ d, d_mod }); } + + if (max_mtime > mod->m_mtime) { + // .olean file out of date, try again with .lean file + return build_module(mod_name, false, orig_module_stack); + } + + auto deps = mod->m_deps; + loaded_module lm { + mod_name, parsed_olean.m_imports, + parse_olean_modifications(parsed_olean.m_serialized_modifications, mod->m_filename) }; + + mod->m_loaded_module = std::make_shared(lm); + m_modules[mod_name] = mod; + return max_mtime; + } else if (mod->m_source == module_src::LEAN) { + auto max_mtime = build_lean(mod, module_stack); + m_modules[mod_name] = mod; + return max_mtime; + } else { + throw exception("unknown module source"); + } } -void module_mgr::build_lean(std::shared_ptr const & mod, std::string const & file_name, name_set const & module_stack) { +time_t module_mgr::build_lean(std::shared_ptr const & mod, name_set const & module_stack) { auto mod_name = mod->m_name; - auto imports = get_direct_imports(file_name, mod->m_contents); - mod->m_trans_mtime = mod->m_mtime; + auto contents = read_file(mod->m_filename); + auto imports = get_direct_imports(mod->m_filename, contents); + auto max_mtime = mod->m_mtime; for (auto & d : imports) { std::shared_ptr d_mod; try { - build_module(d, true, module_stack); + max_mtime = std::max(max_mtime, build_module(d, true, module_stack)); d_mod = m_modules[d]; - mod->m_trans_mtime = std::max(mod->m_trans_mtime, d_mod->m_trans_mtime); } catch (throwable & ex) { - message_builder(m_initial_env, m_ios, file_name, {1, 0}, ERROR).set_exception(ex).report(); + message_builder(m_initial_env, m_ios, mod->m_filename, {1, 0}, ERROR).set_exception(ex).report(); } mod->m_deps.push_back(module_info::dependency { d, d_mod }); build_module(d, true, module_stack); } - std::istringstream in(mod->m_contents); + std::istringstream in(contents); auto env = import_modules(m_initial_env, imports, mk_loader()); - parser p(env, m_ios, in, file_name); + parser p(env, m_ios, in, mod->m_filename); bool done = false; while (!done) { @@ -155,12 +142,13 @@ void module_mgr::build_lean(std::shared_ptr const & mod, std::strin } } - mod->m_result = module_info::parse_result { - p.get_options(), std::make_shared(export_module(p.mk_snapshot()->m_env, mod_name)) }; + mod->m_loaded_module = std::make_shared(export_module(p.mk_snapshot()->m_env, mod_name)); if (m_save_olean) { compile_olean(m_path, mod); } + + return max_mtime; } std::shared_ptr module_mgr::get_module(module_name const & mod_name) { diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index 482c115f84..3184714e68 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -27,10 +27,9 @@ enum class module_src { struct module_info { module_name m_name; - std::string m_file_name; - std::string m_contents; + std::string m_filename; module_src m_source = module_src::LEAN; - time_t m_mtime = -1, m_trans_mtime = -1; + time_t m_mtime = -1; struct dependency { module_name m_name; @@ -38,18 +37,11 @@ struct module_info { }; std::vector m_deps; - struct parse_result { - options m_opts; - std::shared_ptr m_loaded_module; - }; message_log m_log; - parse_result m_result; - bool m_compiled_olean; + std::shared_ptr m_loaded_module; - module_info() {} - - module_info(module_name const & name, std::string const & contents, module_src src, time_t mtime) - : m_name(name), m_contents(contents), m_source(src), m_mtime(mtime) {} + module_info(module_name const & name, std::string const & filename, module_src src, time_t mtime) + : m_name(name), m_filename(filename), m_source(src), m_mtime(mtime) {} }; class module_mgr { @@ -61,11 +53,11 @@ class module_mgr { name_map> m_modules; - void build_module(module_name const & mod, bool can_use_olean, name_set module_stack); + time_t build_module(module_name const & mod, bool can_use_olean, name_set module_stack); std::vector get_direct_imports(std::string const & file_name, std::string const & contents); - void build_lean(std::shared_ptr const & mod, std::string const & file_name, name_set const & module_stack); + time_t build_lean(std::shared_ptr const & mod, name_set const & module_stack); public: module_mgr(search_path const & path, environment const & initial_env, io_state const & ios) : @@ -75,10 +67,8 @@ public: module_loader mk_loader(); void set_save_olean(bool save_olean) { m_save_olean = save_olean; } - bool get_save_olean() const { return m_save_olean; } environment get_initial_env() const { return m_initial_env; } options get_options() const { return m_ios.get_options(); } - io_state get_io_state() const { return m_ios; } }; } diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 6a569aad21..13c1c3e038 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -251,7 +251,7 @@ name module_name_of_file(search_path const & paths, std::string const & fname0) return n; } } - throw exception(sstream() << "file '" << fname0 << "' not part of any known Lean packages"); + throw exception(sstream() << "file '" << fname0 << "' is not part of any known Lean packages"); } module_name absolutize_module_name(search_path const & path, std::string const & base, rel_module_name const & rel) { @@ -277,22 +277,6 @@ void find_imports_core(std::string const & base, optional const & k, } } -void find_imports(search_path const & paths, std::string const & base, optional const & k, - std::vector> & imports) { - if (!k) { - for (auto & base : paths) - if (is_dir(base)) - find_imports_core(base, k, imports); - } else { - auto path = base; - for (unsigned i = 0; i < *k; i++) { - path += get_dir_sep(); - path += ".."; - } - find_imports_core(path, k, imports); - } -} - std::string olean_of_lean(std::string const & lean_fn) { if (lean_fn.size() > 5 && lean_fn.substr(lean_fn.size() - 5) == ".lean") { return lean_fn.substr(0, lean_fn.size() - 5) + ".olean"; @@ -300,12 +284,4 @@ std::string olean_of_lean(std::string const & lean_fn) { throw exception(sstream() << "not a .lean file: " << lean_fn); } } - -std::string olean_file_to_lean_file(std::string const &olean) { - lean_assert(is_olean_file(olean)); - std::string lean = olean; - lean.erase(lean.size() - std::string("olean").size(), 1); - return lean; -} - } diff --git a/tests/lean/leanpkg.path b/tests/lean/leanpkg.path index 05e3345a56..2cbfd2b51b 100644 --- a/tests/lean/leanpkg.path +++ b/tests/lean/leanpkg.path @@ -1,2 +1,2 @@ builtin_path -./. \ No newline at end of file +path .