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

refactor(library): remove sorry checking

Browse source 
We have to revise how we do this.
This commit is contained in:
Leonardo de Moura 2018-05-31 15:20:39 -07:00
parent 8a918a2a14
commit cab6b39c76
4 changed files with 5 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/frontends/lean/parser.cpp
View file

@ -2479,28 +2479,7 @@ void parser::process_imports() {
scope_log_tree lt("importing", {begin_pos, pos()});
buffer<import_error> import_errors;
std::unordered_set<std::string> 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<unit>(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) {

34
src/library/module.cpp
View file

@ -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<unsigned>(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<bool> has_sorry(modification_list const & mods) {
std::vector<task<expr>> 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<decl_modification>(std::move(decl));
}
void get_introduced_exprs(std::vector<task<expr>> & 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<gtask> &) const override {
}
};
@ -361,12 +343,6 @@ struct inductive_modification : public modification {
auto decl = read_certified_inductive_decl(d);
return std::make_shared<inductive_modification>(std::move(decl));
}
void get_introduced_exprs(std::vector<task<expr>> & 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<module_name> imports;
bool uses_sorry;
deserializer d1(in, optional<std::string>(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<std::string> 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>(
loaded_module { fn, parsed.m_imports, modifs,
mk_pure_task<bool>(parsed.m_uses_sorry), {} });
loaded_module { fn, parsed.m_imports, modifs, {} });
};
}

5
src/library/module.h
View file

@ -37,7 +37,6 @@ struct loaded_module {
std::string m_module_name;
std::vector<module_name> m_imports;
modification_list m_modifications;
task<bool> m_uses_sorry;
task<environment> m_env;
};
@ -98,7 +97,6 @@ bool is_candidate_olean_file(std::string const & file_name);
struct olean_data {
std::vector<module_name> 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<gtask> &) const {}
// Used to check for sorrys.
virtual void get_introduced_exprs(std::vector<task<expr>> &) const {}
};
#define LEAN_MODIFICATION(k) \

6
src/library/module_mgr.cpp
View file

@ -100,8 +100,7 @@ static gtask compile_olean(std::shared_ptr<module_info const> const & mod, log_t
gtask mod_dep = mk_deep_dependency(mod->m_result, [] (buffer<gtask> & 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<gtask> 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<bool>(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<module_info::parse_result>(res);