michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/module): race condition on m_imported

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-14 15:19:50 -07:00
parent 343a9a690e
commit a30232b99a
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/module.cpp
View file

@ -252,8 +252,8 @@ struct import_modules_fn {
}; };
typedef std::shared_ptr<module_info> module_info_ptr; typedef std::shared_ptr<module_info> module_info_ptr;
name_map<module_info_ptr> m_module_info; name_map<module_info_ptr> m_module_info;
name_set m_visited; name_set m_visited; // contains visited files in the current call
name_set m_imported; // all imported files name_set m_imported; // contains all imported files, even ones from previous calls
import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios): import_modules_fn(environment const & env, unsigned num_threads, bool keep_proofs, io_state const & ios):
m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios), m_senv(env), m_num_threads(num_threads), m_keep_proofs(keep_proofs), m_ios(ios),
@ -282,6 +282,7 @@ struct import_modules_fn {
if (m_visited.contains(fname)) if (m_visited.contains(fname))
throw exception(sstream() << "circular dependency detected at '" << fname << "'"); throw exception(sstream() << "circular dependency detected at '" << fname << "'");
m_visited.insert(fname); m_visited.insert(fname);
m_imported.insert(fname);
std::ifstream in(fname, std::ifstream::binary); std::ifstream in(fname, std::ifstream::binary);
if (!in.good()) if (!in.good())
throw exception(sstream() << "failed to open file '" << fname << "'"); throw exception(sstream() << "failed to open file '" << fname << "'");
@ -430,7 +431,6 @@ struct import_modules_fn {
add_import_module_task(d); add_import_module_task(d);
} }
} }
m_imported.insert(r->m_fname);
} }
optional<asynch_update_fn> next_task() { optional<asynch_update_fn> next_task() {