diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index b21e372b31..b92c6b5d3d 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -121,16 +121,16 @@ void module_mgr::build_lean(std::shared_ptr 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 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 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); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 7c8b3f84f3..0c34efb97c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -491,13 +491,21 @@ int main(int argc, char ** argv) { scope_message_log scope_log(l); auto imports = mod_mgr.get_direct_imports("", 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, "", {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, ""); - // 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, ""); + // The server will obviously do something more complicated from here + p.parse_commands(); + } for (auto const & msg : l.to_buffer()) { if (json_output) {