feat(library/module): module manager in Lean is alive
This commit is contained in:
Leonardo de Moura
parent
d5fd5d86ee
commit
7696c28fe1
1 changed files with 41 additions and 209 deletions
|
|
@ -136,21 +136,28 @@ void register_module_object_reader(std::string const & k, module_modification_re
|
|||
static char const * g_olean_end_file = "EndFile";
|
||||
|
||||
extern "C" object * lean_serialize_modifications(object * mod_list, object * w) {
|
||||
object_ref mod(mod_list);
|
||||
object_ref mod_list_ref(mod_list);
|
||||
try {
|
||||
std::ostringstream out(std::ios_base::binary);
|
||||
serializer s(out);
|
||||
|
||||
buffer<object *> mod_buffer;
|
||||
while (!is_scalar(mod_list)) {
|
||||
to_modification(cnstr_get(mod_list, 0)).serialize(s);
|
||||
mod_buffer.push_back(cnstr_get(mod_list, 0));
|
||||
mod_list = cnstr_get(mod_list, 1);
|
||||
}
|
||||
|
||||
size_t i = mod_buffer.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
modification & mod = to_modification(mod_buffer[i]);
|
||||
s << std::string(mod.get_key());
|
||||
mod.serialize(s);
|
||||
}
|
||||
s << g_olean_end_file;
|
||||
std::string bytes = out.str();
|
||||
|
||||
object * r = alloc_sarray(1, bytes.size(), bytes.size());
|
||||
memcpy(sarray_cptr<uint8>(r), bytes.data(), bytes.size());
|
||||
|
||||
return set_io_result(w, r);
|
||||
} catch (exception & ex) {
|
||||
return set_io_error(w, ex.what());
|
||||
|
|
@ -191,102 +198,44 @@ extern "C" object * lean_perform_serialized_modifications(object * env0, object
|
|||
|
||||
// =======================================
|
||||
|
||||
struct module_ext : public environment_extension {
|
||||
std::vector<module_name> m_direct_imports;
|
||||
};
|
||||
/*
|
||||
@[export lean.write_module_core]
|
||||
def writeModule (env : Environment) (fname : String) : IO Unit := */
|
||||
object * write_module_core(object * env, object * fname, object * w);
|
||||
|
||||
struct module_ext_reg {
|
||||
unsigned m_ext_id;
|
||||
module_ext_reg() { m_ext_id = environment::register_extension(new module_ext()); }
|
||||
};
|
||||
|
||||
static module_ext_reg * g_ext = nullptr;
|
||||
|
||||
static module_ext const & get_extension(environment const & env) {
|
||||
return static_cast<module_ext const &>(env.get_extension(g_ext->m_ext_id));
|
||||
void write_module(environment const & env, std::string const & olean_fn) {
|
||||
object * r = write_module_core(env.get_obj_arg(), mk_string(olean_fn), io_mk_world());
|
||||
if (io_result_is_error(r)) {
|
||||
dec_ref(r);
|
||||
throw exception(sstream() << "failed to write module '" << olean_fn << "'");
|
||||
} else {
|
||||
dec_ref(r);
|
||||
}
|
||||
}
|
||||
|
||||
static environment update(environment const & env, module_ext const & ext) {
|
||||
return env.update(g_ext->m_ext_id, new module_ext(ext));
|
||||
}
|
||||
/*
|
||||
@[export lean.import_modules_core]
|
||||
def importModules (modNames : List Name) (trustLevel : UInt32 := 0) : IO Environment :=
|
||||
*/
|
||||
object * import_modules_core(object * mod_names, uint32 trust_level, object * w);
|
||||
|
||||
static unsigned olean_hash(std::string const & data) {
|
||||
return hash(data.size(), [&] (unsigned i) { return static_cast<unsigned char>(data[i]); });
|
||||
environment import_modules(unsigned trust_lvl, std::vector<module_name> const & imports) {
|
||||
names mods(imports.begin(), imports.end());
|
||||
object * r = import_modules_core(mods.steal(), trust_lvl, io_mk_world());
|
||||
if (io_result_is_error(r)) {
|
||||
dec_ref(r);
|
||||
io_result_show_error(r); // TODO(Leo): move to exception
|
||||
throw exception("failed to import modules");
|
||||
} else {
|
||||
environment env(io_result_get_value(r), true);
|
||||
dec_ref(r);
|
||||
return env;
|
||||
}
|
||||
}
|
||||
|
||||
object * environment_add_modification_core(object * env, object * mod);
|
||||
object * environment_get_modifications_core(object * env);
|
||||
|
||||
void write_module(environment const & env, std::string const & olean_fn) {
|
||||
exclusive_file_lock output_lock(olean_fn);
|
||||
std::ofstream out(olean_fn, std::ios_base::binary);
|
||||
module_ext const & ext = get_extension(env);
|
||||
|
||||
buffer<modification*> mods;
|
||||
object * mod_list = environment_get_modifications_core(env.get_obj_arg());
|
||||
while (!is_scalar(mod_list)) {
|
||||
object * mod = cnstr_get(mod_list, 0);
|
||||
mods.push_back(&to_modification(mod));
|
||||
mod_list = cnstr_get(mod_list, 1);
|
||||
}
|
||||
|
||||
std::ostringstream out1(std::ios_base::binary);
|
||||
serializer s1(out1);
|
||||
|
||||
// store objects
|
||||
for (int i = mods.size() - 1; i >= 0; i--) {
|
||||
s1 << std::string(mods[i]->get_key());
|
||||
mods[i]->serialize(s1);
|
||||
}
|
||||
|
||||
dec(mod_list);
|
||||
|
||||
s1 << g_olean_end_file;
|
||||
|
||||
if (!out1.good()) {
|
||||
throw exception(sstream() << "error during serialization");
|
||||
}
|
||||
|
||||
std::string r = out1.str();
|
||||
unsigned h = olean_hash(r);
|
||||
|
||||
serializer s2(out);
|
||||
s2 << g_olean_header << get_version_string();
|
||||
s2 << h;
|
||||
// store imported files
|
||||
s2 << static_cast<unsigned>(ext.m_direct_imports.size());
|
||||
for (auto m : ext.m_direct_imports)
|
||||
s2 << m;
|
||||
// store object code
|
||||
s2.write_blob(r);
|
||||
|
||||
out.close();
|
||||
if (!out) throw exception("failed to write olean file");
|
||||
}
|
||||
|
||||
|
||||
struct decl_modification : public modification {
|
||||
LEAN_MODIFICATION("decl")
|
||||
declaration m_decl;
|
||||
|
||||
decl_modification() {}
|
||||
decl_modification(declaration const & decl):
|
||||
m_decl(decl) {}
|
||||
|
||||
void perform(environment & env) const override {
|
||||
env = env.add(m_decl, false);
|
||||
}
|
||||
|
||||
void serialize(serializer & s) const override {
|
||||
s << m_decl;
|
||||
}
|
||||
|
||||
static modification* deserialize(deserializer & d) {
|
||||
auto decl = read_declaration(d);
|
||||
return new decl_modification(std::move(decl));
|
||||
}
|
||||
};
|
||||
|
||||
namespace module {
|
||||
environment add(environment const & env, modification* modf) {
|
||||
return environment(environment_add_modification_core(env.get_obj_arg(), to_object(modf)));
|
||||
|
|
@ -299,135 +248,18 @@ environment add_and_perform(environment const & env, modification * modf) {
|
|||
}
|
||||
|
||||
environment add(environment const & env, declaration const & d, bool check) {
|
||||
environment new_env = env.add(d, check);
|
||||
return add(new_env, new decl_modification(d));
|
||||
return env.add(d, check);
|
||||
}
|
||||
} // end of namespace module
|
||||
|
||||
struct olean_data {
|
||||
std::vector<module_name> m_imports;
|
||||
std::string m_serialized_modifications;
|
||||
};
|
||||
static olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash) {
|
||||
std::vector<module_name> imports;
|
||||
time_task t(".olean deserialization",
|
||||
message_builder(environment(), get_global_ios(), file_name, pos_info(), message_severity::INFORMATION));
|
||||
|
||||
deserializer d1(in, optional<std::string>(file_name));
|
||||
std::string header, version;
|
||||
unsigned claimed_hash;
|
||||
d1 >> header;
|
||||
if (header != g_olean_header)
|
||||
throw exception(sstream() << "file '" << file_name << "' does not seem to be a valid object Lean file, invalid header");
|
||||
d1 >> version >> claimed_hash;
|
||||
#ifndef LEAN_IGNORE_OLEAN_VERSION
|
||||
if (version != get_version_string()) {
|
||||
throw exception(sstream() << "error importing file '" << file_name << "', it is from a different Lean version");
|
||||
}
|
||||
#endif
|
||||
|
||||
unsigned num_imports = d1.read_unsigned();
|
||||
for (unsigned i = 0; i < num_imports; i++) {
|
||||
module_name r;
|
||||
d1 >> r;
|
||||
imports.push_back(r);
|
||||
}
|
||||
|
||||
auto code = d1.read_blob();
|
||||
|
||||
if (!in.good()) {
|
||||
throw exception(sstream() << "file '" << file_name << "' has been corrupted");
|
||||
}
|
||||
|
||||
if (check_hash) {
|
||||
unsigned computed_hash = olean_hash(code);
|
||||
if (claimed_hash != computed_hash)
|
||||
throw exception(sstream() << "file '" << file_name << "' has been corrupted, checksum mismatch");
|
||||
}
|
||||
|
||||
return { imports, code };
|
||||
}
|
||||
|
||||
using modification_list = std::vector<modification*>;
|
||||
|
||||
static void import_module(modification_list const & modifications, environment & env) {
|
||||
for (auto & m : modifications) {
|
||||
m->perform(env);
|
||||
}
|
||||
}
|
||||
|
||||
modification_list parse_olean_modifications(std::string const & olean_code, std::string const & file_name) {
|
||||
modification_list ms;
|
||||
std::istringstream in(olean_code, std::ios_base::binary);
|
||||
deserializer d(in, optional<std::string>(file_name));
|
||||
object_readers & readers = get_object_readers();
|
||||
unsigned obj_counter = 0;
|
||||
while (true) {
|
||||
std::string k;
|
||||
unsigned offset = in.tellg();
|
||||
d >> k;
|
||||
if (k == g_olean_end_file) {
|
||||
break;
|
||||
}
|
||||
|
||||
auto it = readers.find(k);
|
||||
if (it == readers.end())
|
||||
throw exception(sstream() << "file '" << file_name << "' has been corrupted at offset " << offset
|
||||
<< ", unknown object: " << k);
|
||||
ms.emplace_back(it->second(d));
|
||||
|
||||
obj_counter++;
|
||||
}
|
||||
if (!in.good()) {
|
||||
throw exception(sstream() << "file '" << file_name << "' has been corrupted");
|
||||
}
|
||||
return ms;
|
||||
}
|
||||
|
||||
static void import_module_rec(environment & env, module_name const & mod, name_set & already_imported) {
|
||||
if (already_imported.contains(mod))
|
||||
return;
|
||||
auto olean_fn = find_file(*g_search_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, already_imported);
|
||||
}
|
||||
import_module(parse_olean_modifications(parsed_olean.m_serialized_modifications, olean_fn), env);
|
||||
|
||||
already_imported.insert(mod);
|
||||
}
|
||||
|
||||
environment import_modules(unsigned trust_lvl, std::vector<module_name> const & imports) {
|
||||
name_set already_imported;
|
||||
environment env(trust_lvl);
|
||||
|
||||
for (auto & import : imports)
|
||||
import_module_rec(env, import, already_imported);
|
||||
|
||||
module_ext ext = get_extension(env);
|
||||
ext.m_direct_imports = imports;
|
||||
return update(env, ext);
|
||||
}
|
||||
|
||||
void initialize_module() {
|
||||
g_modification_class = register_external_object_class(modification_finalizer, modification_foreach);
|
||||
g_ext = new module_ext_reg();
|
||||
g_object_readers = new object_readers();
|
||||
g_search_path = new search_path();
|
||||
decl_modification::init();
|
||||
}
|
||||
|
||||
void finalize_module() {
|
||||
decl_modification::finalize();
|
||||
delete g_object_readers;
|
||||
delete g_ext;
|
||||
delete g_search_path;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue