diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a9ac262f7e..181f5c9982 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2479,28 +2479,7 @@ void parser::process_imports() { scope_log_tree lt("importing", {begin_pos, pos()}); buffer import_errors; - std::unordered_set already_checked; - module_loader sorry_checking_import_fn = - [&] (std::string const & mod_id, module_name const & import) { - auto mod = m_import_fn(mod_id, import); - - auto pos = m_last_cmd_pos; - auto mod_name = mod->m_module_name; - auto fn = m_file_name; - if (!already_checked.count(mod_name)) { - add_library_task(map(mod->m_uses_sorry, [pos, mod_name, fn](bool uses_sorry) { - if (uses_sorry) - report_message(message(fn, pos, WARNING, - (sstream() << "imported file '" << mod_name - << "' uses sorry").str())); - return unit {}; - }), "checking import for sorry", true, log_tree::CrossModuleLintLevel); - already_checked.insert(mod_name); - } - - return mod; - }; - m_env = import_modules(m_env, m_file_name, imports, sorry_checking_import_fn, import_errors); + m_env = import_modules(m_env, m_file_name, imports, m_import_fn, import_errors); if (!import_errors.empty()) { for (auto & e : import_errors) { diff --git a/src/library/module.cpp b/src/library/module.cpp index 6215d29a8f..10e90ddb2d 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -24,7 +24,6 @@ Author: Leonardo de Moura #include "kernel/quotient/quotient.h" #include "library/module.h" #include "library/noncomputable.h" -#include "library/sorry.h" #include "library/constants.h" #include "library/kernel_serializer.h" #include "library/unfold_macros.h" @@ -252,12 +251,9 @@ void write_module(loaded_module const & mod, std::ostream & out) { std::string r = out1.str(); unsigned h = olean_hash(r); - bool uses_sorry = get(mod.m_uses_sorry); - serializer s2(out); s2 << g_olean_header << get_version_string(); s2 << h; - s2 << uses_sorry; // store imported files s2 << static_cast(mod.m_imports.size()); for (auto m : mod.m_imports) @@ -266,12 +262,6 @@ void write_module(loaded_module const & mod, std::ostream & out) { s2.write_blob(r); } -static task has_sorry(modification_list const & mods) { - std::vector> introduced_exprs; - for (auto & mod : mods) mod->get_introduced_exprs(introduced_exprs); - return any(introduced_exprs, [] (expr const & e) { return has_sorry(e); }); -} - loaded_module export_module(environment const & env, std::string const & mod_name) { loaded_module out; out.m_module_name = mod_name; @@ -284,8 +274,6 @@ loaded_module export_module(environment const & env, std::string const & mod_nam out.m_modifications.push_back(w); std::reverse(out.m_modifications.begin(), out.m_modifications.end()); - out.m_uses_sorry = has_sorry(out.m_modifications); - return out; } @@ -331,12 +319,6 @@ struct decl_modification : public modification { return std::make_shared(std::move(decl)); } - void get_introduced_exprs(std::vector> & es) const override { - es.push_back(mk_pure_task(m_decl.get_type())); - if (m_decl.is_definition()) - es.push_back(mk_pure_task(m_decl.get_value())); - } - void get_task_dependencies(buffer &) const override { } }; @@ -361,12 +343,6 @@ struct inductive_modification : public modification { auto decl = read_certified_inductive_decl(d); return std::make_shared(std::move(decl)); } - - void get_introduced_exprs(std::vector> & es) const override { - es.push_back(mk_pure_task(m_decl.get_decl().m_type)); - for (auto & i : m_decl.get_decl().m_intro_rules) - es.push_back(mk_pure_task(i)); - } }; struct quot_modification : public modification { @@ -411,8 +387,6 @@ environment update_module_defs(environment const & env, declaration const & d) { } } -struct sorry_warning_tag : public log_entry_cell {}; - environment add(environment const & env, certified_declaration const & d) { environment new_env = env.add(d); declaration _d = d.get_declaration(); @@ -465,7 +439,6 @@ bool is_candidate_olean_file(std::string const & file_name) { olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash) { std::vector imports; - bool uses_sorry; deserializer d1(in, optional(file_name)); std::string header, version; @@ -476,8 +449,6 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch d1 >> version >> claimed_hash; // version has already been checked in `is_candidate_olean_file` - d1 >> uses_sorry; - unsigned num_imports = d1.read_unsigned(); for (unsigned i = 0; i < num_imports; i++) { module_name r; @@ -497,7 +468,7 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch throw exception(sstream() << "file '" << file_name << "' has been corrupted, checksum mismatch"); } - return { imports, code, uses_sorry }; + return { imports, code }; } static void import_module(environment & env, std::string const & module_file_name, module_name const & ref, @@ -621,8 +592,7 @@ module_loader mk_olean_loader(std::vector const & path) { auto parsed = parse_olean(in, fn, check_hash); auto modifs = parse_olean_modifications(parsed.m_serialized_modifications, fn); return std::make_shared( - loaded_module { fn, parsed.m_imports, modifs, - mk_pure_task(parsed.m_uses_sorry), {} }); + loaded_module { fn, parsed.m_imports, modifs, {} }); }; } diff --git a/src/library/module.h b/src/library/module.h index 801a03f8d3..30592b2312 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -37,7 +37,6 @@ struct loaded_module { std::string m_module_name; std::vector m_imports; modification_list m_modifications; - task m_uses_sorry; task m_env; }; @@ -98,7 +97,6 @@ bool is_candidate_olean_file(std::string const & file_name); struct olean_data { std::vector m_imports; std::string m_serialized_modifications; - bool m_uses_sorry; }; olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash = true); modification_list parse_olean_modifications(std::string const & serialized_modifications, std::string const & file_name); @@ -111,9 +109,6 @@ public: virtual void perform(environment &) const = 0; virtual void serialize(serializer &) const = 0; virtual void get_task_dependencies(buffer &) const {} - - // Used to check for sorrys. - virtual void get_introduced_exprs(std::vector> &) const {} }; #define LEAN_MODIFICATION(k) \ diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 88b466fde6..04d7f773ee 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -100,8 +100,7 @@ static gtask compile_olean(std::shared_ptr const & mod, log_t gtask mod_dep = mk_deep_dependency(mod->m_result, [] (buffer & deps, module_info::parse_result const & res) { for (auto & mdf : res.m_loaded_module->m_modifications) mdf->get_task_dependencies(deps); - deps.push_back(res.m_loaded_module->m_uses_sorry); - }); + }); std::vector olean_deps; for (auto & dep : mod->m_deps) @@ -192,8 +191,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set auto deps = mod->m_deps; res.m_loaded_module = cache_preimported_env( { id, parsed_olean.m_imports, - parse_olean_modifications(parsed_olean.m_serialized_modifications, id), - mk_pure_task(parsed_olean.m_uses_sorry), {} }, + parse_olean_modifications(parsed_olean.m_serialized_modifications, id), {} }, m_initial_env, [=] { return mk_loader(id, deps); }); mod->m_result = mk_pure_task(res);