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

chore(library/module): remove import errors

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-14 07:13:50 -07:00
parent 53ec9ee181
commit 9596fae665
2 changed files with 17 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/library/module.cpp
View file

@ -355,51 +355,38 @@ modification_list parse_olean_modifications(std::string const & olean_code, std:
}
static void import_module_rec(environment & env, module_name const & mod,
search_path const & path, buffer<import_error> & import_errors,
name_set & already_imported) {
search_path const & path, name_set & already_imported) {
if (already_imported.contains(mod))
return;
try {
auto olean_fn = find_file(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, path, import_errors, already_imported);
}
import_module(parse_olean_modifications(parsed_olean.m_serialized_modifications, olean_fn), env);
already_imported.insert(mod);
} catch (throwable) {
import_errors.push_back({mod, std::current_exception()});
auto olean_fn = find_file(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, path, already_imported);
}
import_module(parse_olean_modifications(parsed_olean.m_serialized_modifications, olean_fn), env);
already_imported.insert(mod);
}
environment import_modules(environment const & env0, std::vector<module_name> const & imports, search_path const & path,
buffer<import_error> & import_errors) {
environment import_modules(environment const & env0, std::vector<module_name> const & imports, search_path const & path) {
name_set already_imported;
environment env = env0;
for (auto & import : imports)
import_module_rec(env, import, path, import_errors, already_imported);
import_module_rec(env, import, path, already_imported);
module_ext ext = get_extension(env);
ext.m_direct_imports = imports;
return update(env, ext);
}
environment import_modules(environment const & env0, std::vector<module_name> const & imports, search_path const & path) {
buffer<import_error> import_errors;
auto env = import_modules(env0, imports, path, import_errors);
if (!import_errors.empty()) std::rethrow_exception(import_errors.back().m_ex);
return env;
}
void initialize_module() {
g_modification_class = register_external_object_class(modification_finalizer, modification_foreach);
g_ext = new module_ext_reg();

8
src/library/module.h
View file

@ -34,14 +34,6 @@ struct loaded_module {
environment
import_modules(environment const & env, std::vector<module_name> const & imports, search_path const & path);
struct import_error {
module_name m_import;
std::exception_ptr m_ex;
};
environment
import_modules(environment const & env, std::vector<module_name> const & imports, search_path const & path,
buffer<import_error> & errors);
/** \brief Store module using \c env. */
void write_module(environment const & env, module_name const & mod, std::string const & olean_fn);