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

feat(library/module_mgr,shell/lean): abort on import with errors

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-20 15:46:05 -07:00
parent f21609c93d
commit 896b45239e
2 changed files with 22 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/module_mgr.cpp
View file

@ -121,16 +121,16 @@ void module_mgr::build_lean(std::shared_ptr<module_info> const & mod, name_set c
auto contents = read_file(mod->m_filename);
auto imports = get_direct_imports(mod->m_filename, contents);
for (auto & d : imports) {
std::shared_ptr<module_info> d_mod;
try {
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, 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::shared_ptr<module_info> d_mod = m_modules[d];
if (d_mod->m_log.has_errors()) {
message_builder msg(m_initial_env, m_ios, mod->m_filename, {1, 0}, ERROR);
msg << "import " << d_mod->m_name << " has errors, aborting";
msg.report();
return;
}
mod->m_trans_mtime = std::max(mod->m_trans_mtime, d_mod->m_trans_mtime);
mod->m_deps.push_back(module_info::dependency { d, d_mod });
}
std::istringstream in(contents);

18
src/shell/lean.cpp
View file

@ -491,13 +491,21 @@ int main(int argc, char ** argv) {
scope_message_log scope_log(l);
auto imports = mod_mgr.get_direct_imports("<stdin>", buf.str());
for (auto & d : imports) {
mod_mgr.get_module(d);
auto d_mod = mod_mgr.get_module(d);
if (d_mod->m_log.has_errors()) {
message_builder msg(env, ios, "<stdin>", {1, 0}, ERROR);
msg << "import " << d_mod->m_name << " has errors, aborting";
msg.report();
ok = false;
}
}
auto mod_env = import_modules(env, imports, mod_mgr.mk_loader());
parser p(mod_env, ios, buf, "<stdin>");
// The server will obviously do something more complicated from here
p.parse_commands();
if (ok) {
auto mod_env = import_modules(env, imports, mod_mgr.mk_loader());
parser p(mod_env, ios, buf, "<stdin>");
// The server will obviously do something more complicated from here
p.parse_commands();
}
for (auto const & msg : l.to_buffer()) {
if (json_output) {