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

refactor(library/module_mgr): minor refactorings

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-11 12:58:53 -07:00 • committed by Leonardo de Moura
parent af99f153f8
commit 43e57358af
5 changed files with 62 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/module.h
View file

@ -24,12 +24,14 @@ public:
struct modification;
using modification_list = std::vector<std::shared_ptr<modification const>>;
/** \brief A finished module. The in-memory representation of a .olean file. */
struct loaded_module {
module_name m_name; // not serialized
std::vector<module_name> 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<std::shared_ptr<loaded_module const> (module_name const &)>;

114
src/library/module_mgr.cpp
View file

@ -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<std::string, std::shared_ptr<module_info>>
static std::shared_ptr<module_info>
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<module_info>(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<module_info>(mod_name, olean_fn, module_src::OLEAN, olean_mtime);
}
} catch (exception) {}
return std::make_pair(lean_fn, std::make_shared<module_info>(mod_name, read_file(lean_fn), module_src::LEAN, lean_mtime));
return std::make_shared<module_info>(mod_name, lean_fn, module_src::LEAN, lean_mtime);
}
static void compile_olean(search_path const & path, std::shared_ptr<module_info> 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<module_info> 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<loaded_module const>(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<loaded_module const>(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<module_info> const & mod, std::string const & file_name, name_set const & module_stack) {
time_t module_mgr::build_lean(std::shared_ptr<module_info> 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<module_info> 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<module_info> const & mod, std::strin
}
}
mod->m_result = module_info::parse_result {
p.get_options(), std::make_shared<loaded_module const>(export_module(p.mk_snapshot()->m_env, mod_name)) };
mod->m_loaded_module = std::make_shared<loaded_module const>(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_info const> module_mgr::get_module(module_name const & mod_name) {

24
src/library/module_mgr.h
View file

@ -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<dependency> m_deps;
struct parse_result {
options m_opts;
std::shared_ptr<loaded_module const> m_loaded_module;
};
message_log m_log;
parse_result m_result;
bool m_compiled_olean;
std::shared_ptr<loaded_module const> 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<std::shared_ptr<module_info>> 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<module_name>
get_direct_imports(std::string const & file_name, std::string const & contents);
void build_lean(std::shared_ptr<module_info> const & mod, std::string const & file_name, name_set const & module_stack);
time_t build_lean(std::shared_ptr<module_info> 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; }
};
}

26
src/util/lean_path.cpp
View file

@ -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<unsigned> const & k,
}
}
void find_imports(search_path const & paths, std::string const & base, optional<unsigned> const & k,
std::vector<pair<std::string, std::string>> & 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;
}
}

2
tests/lean/leanpkg.path
View file

@ -1,2 +1,2 @@
builtin_path
./.
path .