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

refactor(library/module{,_mgr},frontends/lean/parser): use absolute module names everywhere for identifying modules, move actual importing from parser to module_mgr

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-11 10:53:26 -07:00 • committed by Leonardo de Moura
parent 716de48078
commit af99f153f8
10 changed files with 189 additions and 280 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -3267,7 +3267,7 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
<< "review := fun ⟨" << view_pat.str() << "⟩, syntax.node (syntax_node.mk " << esc_macro.to_string() << " [" << reviews.str() << "]) }";
trace_elab_detail(tout() << "expansion of node! macro:\n" << struc.str(););
std::istringstream in(struc.str());
parser p(m_env, get_global_ios(), nullptr, in, "foo");
parser p(m_env, get_global_ios(), in, "foo");
p.set_imports_parsed();
p.parse_command_like();
p.parse_command_like();
@ -3325,7 +3325,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
<< review_cases.str()
<< "]) }";
std::istringstream in(struc.str());
parser p(m_env, get_global_ios(), nullptr, in, "foo");
parser p(m_env, get_global_ios(), in, "foo");
p.set_imports_parsed();
p.parse_command_like();
p.parse_command_like();

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

@ -143,12 +143,10 @@ parser::all_id_local_scope::all_id_local_scope(parser & p):
flet<id_behavior>(p.m_id_behavior, id_behavior::AllLocal) {}
parser::parser(environment const & env, io_state const & ios,
module_loader const & import_fn,
std::istream & strm, std::string const & file_name,
bool use_exceptions) :
m_env(env), m_ngen(*g_frontend_fresh), m_ios(ios),
m_use_exceptions(use_exceptions),
m_import_fn(import_fn),
m_file_name(file_name),
m_scanner(strm, m_file_name.c_str()),
m_imports_parsed(false) {
@ -2176,7 +2174,7 @@ void parser::parse_mod_doc_block() {
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & imports) {
void parser::parse_imports(std::vector<rel_module_name> & imports) {
init_scanner();
scanner::field_notation_scope scope(m_scanner, false);
m_last_cmd_pos = pos();
@ -2186,7 +2184,7 @@ void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & im
prelude = true;
}
if (!prelude) {
module_name m("init");
rel_module_name m("init");
imports.push_back(m);
}
while (curr_is_token(get_import_tk())) {
@ -2216,15 +2214,11 @@ void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & im
if (!curr_is_identifier())
break;
name f = get_name_val();
fingerprint = hash(fingerprint, f.hash());
if (k_init) {
fingerprint = hash(fingerprint, h);
}
if (k_init) {
module_name m(f, k);
rel_module_name m(k, f);
imports.push_back(m);
} else {
module_name m(f);
rel_module_name m(f);
imports.push_back(m);
}
next();
@ -2233,45 +2227,13 @@ void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & im
}
void parser::process_imports() {
unsigned fingerprint = 0;
std::vector<module_name> imports;
std::exception_ptr exception_during_scanning;
try {
parse_imports(fingerprint, imports);
} catch (parser_exception) {
exception_during_scanning = std::current_exception();
}
buffer<import_error> 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) {
try {
std::rethrow_exception(e.m_ex);
} catch (throwable & t) {
parser_exception error((sstream() << "invalid import: " << e.m_import.m_name << "\n" << t.what()).str(),
m_file_name.c_str(), m_last_cmd_pos);
if (!m_use_exceptions && m_show_errors)
report_message(error);
if (m_use_exceptions)
throw error;
}
}
}
std::vector<rel_module_name> imports;
parse_imports(imports);
// we assume the module manager has already imported the modules into `m_env`
m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
m_env = replay_export_decls_core(m_env, m_ios);
m_imports_parsed = true;
if (exception_during_scanning) std::rethrow_exception(exception_during_scanning);
}
void parser::get_imports(std::vector<module_name> & imports) {
scope_pos_info_provider scope1(*this);
unsigned fingerprint;
parse_imports(fingerprint, imports);
}
bool parser::parse_command_like() {

7
src/frontends/lean/parser.h
View file

@ -14,7 +14,6 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/expr_maps.h"
#include "library/util.h"
#include "library/module.h"
#include "library/abstract_parser.h"
#include "library/io_state.h"
#include "library/io_state_stream.h"
@ -40,7 +39,6 @@ class parser : public abstract_parser {
io_state m_ios;
bool m_use_exceptions;
bool m_show_errors;
module_loader m_import_fn;
std::string m_file_name;
scanner m_scanner;
token_kind m_curr;
@ -203,7 +201,6 @@ class parser : public abstract_parser {
public:
parser(environment const & env, io_state const & ios,
module_loader const & import_fn,
std::istream & strm, std::string const & file_name,
bool use_exceptions = false);
~parser();
@ -437,7 +434,7 @@ public:
bool parse_command_like();
void parse_command(cmd_meta const & meta);
void parse_imports(unsigned & fingerprint, std::vector<module_name> &);
void parse_imports(std::vector<rel_module_name> &);
struct local_scope {
parser & m_p; environment m_env;
@ -539,8 +536,6 @@ public:
/** return true iff profiling is enabled */
bool profiling() const { return m_profile; }
void get_imports(std::vector<module_name> &);
class in_notation_ctx {
scanner::in_notation_ctx m_ctx;
public:

108
src/library/module.cpp
View file

@ -2,7 +2,7 @@
Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
*/
#include <unordered_map>
#include <vector>
@ -97,26 +97,6 @@ static environment update(environment const & env, module_ext const & ext) {
static char const * g_olean_end_file = "EndFile";
static char const * g_olean_header = "oleanfile";
serializer & operator<<(serializer & s, module_name const & n) {
if (n.m_relative)
s << true << *n.m_relative << n.m_name;
else
s << false << n.m_name;
return s;
}
deserializer & operator>>(deserializer & d, module_name & r) {
if (d.read_bool()) {
unsigned k;
d >> k >> r.m_name;
r.m_relative = { k };
} else {
d >> r.m_name;
r.m_relative = optional<unsigned>();
}
return d;
}
static unsigned olean_hash(std::string const & data) {
return hash(data.size(), [&] (unsigned i) { return static_cast<unsigned char>(data[i]); });
}
@ -133,7 +113,7 @@ void write_module(loaded_module const & mod, std::ostream & out) {
s1 << g_olean_end_file;
if (!out1.good()) {
throw exception(sstream() << "error during serialization of '" << mod.m_module_name << "'");
throw exception(sstream() << "error during serialization of '" << mod.m_name << "'");
}
std::string r = out1.str();
@ -150,9 +130,9 @@ void write_module(loaded_module const & mod, std::ostream & out) {
s2.write_blob(r);
}
loaded_module export_module(environment const & env, std::string const & mod_name) {
loaded_module export_module(environment const & env, module_name const & mod) {
loaded_module out;
out.m_module_name = mod_name;
out.m_name = mod;
module_ext const & ext = get_extension(env);
@ -271,44 +251,48 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch
return { imports, code };
}
static void import_module(environment & env, std::string const & module_file_name, module_name const & ref,
module_loader const & mod_ldr, buffer<import_error> & import_errors) {
try {
auto res = mod_ldr(module_file_name, ref);
auto & ext0 = get_extension(env);
if (ext0.m_imported.contains(name(res->m_module_name))) return;
for (auto &dep : res->m_imports) {
import_module(env, res->m_module_name, dep, mod_ldr, import_errors);
}
import_module(res->m_modifications, res->m_module_name, env);
auto ext = get_extension(env);
ext.m_imported.insert(name(res->m_module_name));
env = update(env, ext);
} catch (throwable) {
import_errors.push_back({module_file_name, ref, std::current_exception()});
static void import_module(modification_list const & modifications, environment & env) {
for (auto & m : modifications) {
m->perform(env);
}
}
environment import_modules(environment const & env0, std::string const & module_file_name,
std::vector<module_name> const & refs, module_loader const & mod_ldr,
static void import_module_rec(environment & env, module_name const & mod,
module_loader const & mod_ldr, buffer<import_error> & import_errors) {
try {
auto res = mod_ldr(mod);
auto & ext0 = get_extension(env);
if (ext0.m_imported.contains(name(res->m_name))) return;
for (auto &dep : res->m_imports) {
import_module_rec(env, dep, mod_ldr, import_errors);
}
import_module(res->m_modifications, env);
auto ext = get_extension(env);
ext.m_imported.insert(name(res->m_name));
env = update(env, ext);
} catch (throwable) {
import_errors.push_back({mod, std::current_exception()});
}
}
environment import_modules(environment const & env0, std::vector<module_name> const & imports, module_loader const & mod_ldr,
buffer<import_error> & import_errors) {
environment env = env0;
for (auto & ref : refs)
import_module(env, module_file_name, ref, mod_ldr, import_errors);
for (auto & import : imports)
import_module_rec(env, import, mod_ldr, import_errors);
module_ext ext = get_extension(env);
ext.m_direct_imports = refs;
ext.m_direct_imports = imports;
return update(env, ext);
}
environment import_modules(environment const & env0, std::string const & module_file_name,
std::vector<module_name> const & refs, module_loader const & mod_ldr) {
environment import_modules(environment const & env0, std::vector<module_name> const & imports, module_loader const & mod_ldr) {
buffer<import_error> import_errors;
auto env = import_modules(env0, module_file_name, refs, mod_ldr, import_errors);
auto env = import_modules(env0, imports, mod_ldr, import_errors);
if (!import_errors.empty()) std::rethrow_exception(import_errors.back().m_ex);
return env;
}
@ -341,30 +325,6 @@ modification_list parse_olean_modifications(std::string const & olean_code, std:
return ms;
}
void import_module(modification_list const & modifications, std::string const & /* file_name */, environment & env) {
for (auto & m : modifications) {
m->perform(env);
}
}
module_loader mk_olean_loader(std::vector<std::string> const & path) {
bool check_hash = false;
return[=] (std::string const & module_fn, module_name const & ref) {
auto base_dir = dirname(module_fn);
auto fn = find_file(path, base_dir, ref.m_relative, ref.m_name, ".olean");
std::ifstream in(fn, std::ios_base::binary);
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 });
};
}
module_loader mk_dummy_loader() {
return[=] (std::string const &, module_name const &) -> std::shared_ptr<loaded_module const> {
throw exception("module importing disabled");
};
}
void initialize_module() {
g_ext = new module_ext_reg();
g_object_readers = new object_readers();

38
src/library/module.h
View file

@ -2,7 +2,7 @@
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
*/
#pragma once
#include <string>
@ -13,6 +13,7 @@ Author: Leonardo de Moura
#include "runtime/optional.h"
#include "library/io_state.h"
#include "kernel/environment.h"
#include "util/lean_path.h"
namespace lean {
class corrupted_file_exception : public exception {
@ -20,61 +21,48 @@ public:
corrupted_file_exception(std::string const & fname);
};
struct module_name {
name m_name;
optional<unsigned> m_relative;
module_name() {}
module_name(name const & n, unsigned k):m_name(n), m_relative(k) {}
explicit module_name(name const & n):m_name(n) {}
};
struct modification;
using modification_list = std::vector<std::shared_ptr<modification const>>;
/** \brief A finished module. The in-memory representation of a .olean file. */
struct loaded_module {
std::string m_module_name;
module_name m_name; // not serialized
std::vector<module_name> m_imports;
modification_list m_modifications;
};
using module_loader = std::function<std::shared_ptr<loaded_module const> (std::string const &, module_name const &)>;
module_loader mk_olean_loader(std::vector<std::string> const &);
module_loader mk_dummy_loader();
/** \brief Mapping from module name to module. Used to separate this file from the module_mgr. */
using module_loader = std::function<std::shared_ptr<loaded_module const> (module_name const &)>;
/** \brief Return an environment based on \c env, where all modules in \c modules are imported.
Modules included directly or indirectly by them are also imported.
The environment \c env is usually an empty environment.
The environment \c env is usually an empty environment (but with the trust level set).
*/
environment
import_modules(environment const & env,
std::string const & current_mod, std::vector<module_name> const & ref,
module_loader const & mod_ldr);
using module_id = std::string;
import_modules(environment const & env, std::vector<module_name> const & imports, module_loader const & mod_ldr);
struct import_error {
module_id m_mod;
module_name m_import;
std::exception_ptr m_ex;
};
environment
import_modules(environment const & env,
std::string const & current_mod, std::vector<module_name> const & ref,
module_loader const & mod_ldr, buffer<import_error> & errors);
import_modules(environment const & env, std::vector<module_name> const & imports, module_loader const & mod_ldr,
buffer<import_error> & errors);
/** \brief Store/Export module using \c env. */
loaded_module export_module(environment const & env, std::string const & mod_name);
loaded_module export_module(environment const & env, module_name const & mod);
void write_module(loaded_module const & mod, std::ostream & out);
/** \brief Check whether we should try to load the given .olean file according to its header and Lean version. */
bool is_candidate_olean_file(std::string const & file_name);
/* TODO: Replace with `loaded_module`. This class used to be used for delaying the actual modifications parsing,
* but that is not the case anymore, nor will it be necessary in the new design. */
struct olean_data {
std::vector<module_name> m_imports;
std::string m_serialized_modifications;
};
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);
void import_module(modification_list const & modifications, std::string const & file_name, environment & env);
struct modification {
public:

151
src/library/module_mgr.cpp
View file

@ -2,7 +2,7 @@
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
Authors: Gabriel Ebner, Sebastian Ullrich
*/
#include <utility>
#include <string>
@ -17,48 +17,13 @@ Author: Gabriel Ebner
#include "frontends/lean/parser.h"
namespace lean {
static module_loader mk_loader(module_id const & cur_mod, std::vector<module_info::dependency> const & deps) {
auto deps_per_mod_ptr = std::make_shared<std::unordered_map<module_id, std::vector<module_info::dependency>>>();
auto & deps_per_mod = *deps_per_mod_ptr;
buffer<module_info const *> to_process;
for (auto & d : deps) {
if (d.m_mod_info) {
deps_per_mod[cur_mod].push_back(d);
to_process.push_back(d.m_mod_info.get());
}
}
while (!to_process.empty()) {
module_info const & m = *to_process.back();
to_process.pop_back();
if (deps_per_mod.count(m.m_id)) continue;
for (auto & d : m.m_deps) {
if (d.m_mod_info) {
deps_per_mod[m.m_id].push_back(d);
if (!deps_per_mod.count(d.m_mod_info->m_id))
to_process.push_back(d.m_mod_info.get());
}
}
}
return[deps_per_mod_ptr] (std::string const & current_module, module_name const & import) -> std::shared_ptr<loaded_module const> {
try {
for (auto & d : deps_per_mod_ptr->at(current_module)) {
if (d.m_import_name.m_name == import.m_name && d.m_import_name.m_relative == import.m_relative) {
return d.m_mod_info->m_result.m_loaded_module;
}
}
} catch (std::out_of_range) {
// In files with syntax errors, it can happen that the
// initial dependency scan does not find all dependencies.
}
throw exception(sstream() << "could not resolve import: " << import.m_name);
};
module_loader module_mgr::mk_loader() {
return [this](module_name const & n) { return get_module(n)->m_result.m_loaded_module; }; // NOLINT
}
static std::shared_ptr<module_info> load_module(module_id const & id, bool can_use_olean) {
auto lean_fn = id;
static std::pair<std::string, std::shared_ptr<module_info>>
load_module(search_path const & path, module_name const & mod_name, bool can_use_olean) {
auto lean_fn = find_file(path, mod_name, {".lean"});
auto lean_mtime = get_mtime(lean_fn);
try {
@ -68,26 +33,28 @@ static std::shared_ptr<module_info> load_module(module_id const & id, bool can_u
if (olean_mtime != -1 && olean_mtime >= lean_mtime &&
can_use_olean &&
is_candidate_olean_file(olean_fn)) {
return std::make_shared<module_info>(id, read_file(olean_fn, std::ios_base::binary), module_src::OLEAN, olean_mtime);
auto mod = std::make_shared<module_info>(mod_name,
read_file(olean_fn, std::ios_base::binary), module_src::OLEAN, olean_mtime);
return std::make_pair(olean_fn, mod);
}
} catch (exception) {}
return std::make_shared<module_info>(id, read_file(lean_fn), module_src::LEAN, lean_mtime);
return std::make_pair(lean_fn, std::make_shared<module_info>(mod_name, read_file(lean_fn), module_src::LEAN, lean_mtime));
}
static void compile_olean(std::shared_ptr<module_info> const & mod) {
static void compile_olean(search_path const & path, std::shared_ptr<module_info> const & mod) {
if (mod->m_compiled_olean)
return;
mod->m_compiled_olean = true;
for (auto & dep : mod->m_deps)
if (dep.m_mod_info)
compile_olean(dep.m_mod_info);
compile_olean(path, dep.m_mod_info);
if (mod->m_source != module_src::LEAN || mod->m_log.has_errors())
return;
auto res = mod->m_result;
auto olean_fn = olean_of_lean(mod->m_id);
auto olean_fn = olean_of_lean(find_file(path, mod->m_name, {".lean"}));
exclusive_file_lock output_lock(olean_fn);
std::ofstream out(olean_fn, std::ios_base::binary);
write_module(*res.m_loaded_module, out);
@ -95,95 +62,81 @@ static void compile_olean(std::shared_ptr<module_info> const & mod) {
if (!out) throw exception("failed to write olean file");
}
static module_id resolve(search_path const & path,
module_id const & module_file_name,
module_name const & ref) {
auto base_dir = dirname(module_file_name);
try {
return find_file(path, base_dir, ref.m_relative, ref.m_name, ".lean");
} catch (lean_file_not_found_exception) {
return olean_file_to_lean_file(find_file(path, base_dir, ref.m_relative, ref.m_name, ".olean"));
}
}
void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set module_stack) {
if (auto & existing_mod = m_modules[id])
void module_mgr::build_module(module_name const & mod_name, bool can_use_olean, name_set module_stack) {
if (auto const & existing_mod = m_modules.find(mod_name))
return;
auto orig_module_stack = module_stack;
if (module_stack.contains(name(id))) {
throw exception(sstream() << "cyclic import: " << id);
if (module_stack.contains(mod_name)) {
throw exception(sstream() << "cyclic import: " << mod_name);
}
module_stack.insert(name(id));
module_stack.insert(mod_name);
scope_global_ios scope_ios(m_ios);
scope_traces_as_messages scope_trace_msgs(id, {1, 0});
scope_traces_as_messages scope_trace_msgs(mod_name.to_string(), {1, 0});
auto mod = load_module(id, can_use_olean);
std::string file_name; std::shared_ptr<module_info> mod;
std::tie(file_name, mod) = load_module(m_path, mod_name, can_use_olean);
scope_message_log scope_log(mod->m_log);
if (mod->m_source == module_src::OLEAN) {
std::istringstream in2(mod->m_contents, std::ios_base::binary);
auto olean_fn = olean_of_lean(id);
bool check_hash = false;
auto parsed_olean = parse_olean(in2, olean_fn, check_hash);
auto parsed_olean = parse_olean(in2, file_name, check_hash);
// we never need to re-parse .olean files, so discard content
mod->m_contents.clear();
mod->m_trans_mtime = mod->m_mtime;
for (auto & d : parsed_olean.m_imports) {
auto d_id = resolve(m_path, id, d);
build_module(d_id, true, module_stack);
build_module(d, true, module_stack);
auto & d_mod = m_modules[d_id];
mod->m_deps.push_back({ d_id, d, d_mod });
auto const & d_mod = *m_modules.find(d);
mod->m_deps.push_back({ d, d_mod });
mod->m_trans_mtime = std::max(mod->m_trans_mtime, d_mod->m_trans_mtime);
}
if (mod->m_trans_mtime > mod->m_mtime)
return build_module(id, false, orig_module_stack);
return build_module(mod_name, false, orig_module_stack);
mod->m_compiled_olean = true;
module_info::parse_result res;
auto deps = mod->m_deps;
loaded_module lm {
id, parsed_olean.m_imports,
parse_olean_modifications(parsed_olean.m_serialized_modifications, id) };
mod_name, parsed_olean.m_imports,
parse_olean_modifications(parsed_olean.m_serialized_modifications, file_name) };
res.m_loaded_module = std::make_shared<loaded_module const>(lm);
mod->m_result = res;
m_modules[id] = mod;
m_modules[mod_name] = mod;
} else if (mod->m_source == module_src::LEAN) {
build_lean(mod, module_stack);
m_modules[id] = mod;
build_lean(mod, file_name, module_stack);
m_modules[mod_name] = mod;
} else {
throw exception("unknown module source");
}
}
void module_mgr::build_lean(std::shared_ptr<module_info> const & mod, name_set const & module_stack) {
auto id = mod->m_id;
auto imports = get_direct_imports(id, mod->m_contents);
void module_mgr::build_lean(std::shared_ptr<module_info> const & mod, std::string const & file_name, name_set const & module_stack) {
auto mod_name = mod->m_name;
auto imports = get_direct_imports(file_name, mod->m_contents);
mod->m_trans_mtime = mod->m_mtime;
for (auto & d : imports) {
module_id d_id;
std::shared_ptr<module_info> d_mod;
try {
d_id = resolve(m_path, id, d);
build_module(d_id, true, module_stack);
d_mod = m_modules[d_id];
build_module(d, true, module_stack);
d_mod = m_modules[d];
mod->m_trans_mtime = std::max(mod->m_trans_mtime, d_mod->m_trans_mtime);
} catch (throwable & ex) {
message_builder(m_initial_env, m_ios, id, {1, 0}, ERROR).set_exception(ex).report();
message_builder(m_initial_env, m_ios, file_name, {1, 0}, ERROR).set_exception(ex).report();
}
mod->m_deps.push_back(module_info::dependency { d_id, d, d_mod });
build_module(d_id, true, module_stack);
mod->m_deps.push_back(module_info::dependency { d, d_mod });
build_module(d, true, module_stack);
}
auto ldr = mk_loader(id, mod->m_deps);
std::istringstream in(mod->m_contents);
parser p(m_initial_env, m_ios, ldr, in, id);
auto env = import_modules(m_initial_env, imports, mk_loader());
parser p(env, m_ios, in, file_name);
bool done = false;
while (!done) {
@ -203,31 +156,35 @@ void module_mgr::build_lean(std::shared_ptr<module_info> const & mod, name_set c
}
mod->m_result = module_info::parse_result {
p.get_options(), std::make_shared<loaded_module const>(export_module(p.mk_snapshot()->m_env, id)) };
p.get_options(), std::make_shared<loaded_module const>(export_module(p.mk_snapshot()->m_env, mod_name)) };
if (m_save_olean) {
compile_olean(mod);
compile_olean(m_path, mod);
}
}
std::shared_ptr<module_info const> module_mgr::get_module(module_id const & id) {
std::shared_ptr<module_info const> module_mgr::get_module(module_name const & mod_name) {
name_set module_stack;
build_module(id, true, module_stack);
return m_modules.at(id);
build_module(mod_name, true, module_stack);
return *m_modules.find(mod_name);
}
std::vector<module_name> module_mgr::get_direct_imports(module_id const & id, std::string const & contents) {
std::vector<module_name> imports;
std::vector<module_name> module_mgr::get_direct_imports(std::string const & file_name, std::string const & contents) {
std::vector<rel_module_name> rel_imports;
try {
std::istringstream in(contents);
bool use_exceptions = true;
parser p(get_initial_env(), m_ios, nullptr, in, id, use_exceptions);
parser p(get_initial_env(), m_ios, in, file_name, use_exceptions);
try {
p.init_scanner();
} catch (...) {}
p.get_imports(imports);
p.parse_imports(rel_imports);
} catch (...) {}
std::vector<module_name> imports;
auto dir = dirname(file_name);
for (auto const & rel : rel_imports)
imports.push_back(absolutize_module_name(m_path, dir, rel));
return imports;
}

24
src/library/module_mgr.h
View file

@ -2,7 +2,7 @@
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
Authors: Gabriel Ebner, Sebastian Ullrich
*/
#pragma once
#include <string>
@ -26,14 +26,14 @@ enum class module_src {
};
struct module_info {
module_id m_id;
module_name m_name;
std::string m_file_name;
std::string m_contents;
module_src m_source = module_src::LEAN;
time_t m_mtime = -1, m_trans_mtime = -1;
struct dependency {
module_id m_id;
module_name m_import_name;
module_name m_name;
std::shared_ptr<module_info> m_mod_info;
};
std::vector<dependency> m_deps;
@ -48,8 +48,8 @@ struct module_info {
module_info() {}
module_info(module_id const & id, std::string const & contents, module_src src, time_t mtime)
: m_id(id), m_contents(contents), m_source(src), m_mtime(mtime) {}
module_info(module_name const & name, std::string const & contents, module_src src, time_t mtime)
: m_name(name), m_contents(contents), m_source(src), m_mtime(mtime) {}
};
class module_mgr {
@ -59,18 +59,20 @@ class module_mgr {
environment m_initial_env;
io_state m_ios;
std::unordered_map<module_id, std::shared_ptr<module_info>> m_modules;
name_map<std::shared_ptr<module_info>> m_modules;
void build_module(module_id const & id, bool can_use_olean, name_set module_stack);
void build_module(module_name const & mod, bool can_use_olean, name_set module_stack);
std::vector<module_name> get_direct_imports(module_id const & id, std::string const & contents);
void build_lean(std::shared_ptr<module_info> const & mod, name_set const & module_stack);
std::vector<module_name>
get_direct_imports(std::string const & file_name, std::string const & contents);
void build_lean(std::shared_ptr<module_info> const & mod, std::string const & file_name, name_set const & module_stack);
public:
module_mgr(search_path const & path,
environment const & initial_env, io_state const & ios) :
m_path(path), m_initial_env(initial_env), m_ios(ios) {}
std::shared_ptr<module_info const> get_module(module_id const &);
std::shared_ptr<module_info const> get_module(module_name const &);
module_loader mk_loader();
void set_save_olean(bool save_olean) { m_save_olean = save_olean; }
bool get_save_olean() const { return m_save_olean; }

8
src/shell/lean.cpp
View file

@ -458,24 +458,24 @@ int main(int argc, char ** argv) {
for (auto & f : args) module_args.push_back(lrealpath(f));
struct input_mod {
module_id m_id;
std::string m_file_name;
std::shared_ptr<module_info const> m_mod_info;
};
std::vector<input_mod> mods;
for (auto & mod : module_args) {
auto mod_info = mod_mgr.get_module(mod);
auto mod_info = mod_mgr.get_module(module_name_of_file(path.get_path(), mod));
mods.push_back({mod, mod_info});
}
for (auto & mod : mods) {
if (test_suite) {
std::ofstream out(mod.m_id + ".test_suite.out");
std::ofstream out(mod.m_file_name + ".test_suite.out");
for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) {
out << msg;
}
}
if (test_suite) {
std::ofstream status(mod.m_id + ".status");
std::ofstream status(mod.m_file_name + ".status");
status << (!mod.m_mod_info->m_log.has_errors() ? 0 : 1);
}
}

42
src/util/lean_path.cpp
View file

@ -68,7 +68,7 @@ search_path parse_leanpkg_path(std::string const & fn) {
std::getline(in, line);
if (auto rest = begins_with(line, "path "))
path.push_back(resolve(*rest, fn_dir));
path.push_back(lrealpath(resolve(*rest, fn_dir)));
if (line == "builtin_path") {
auto builtin = get_builtin_search_path();
@ -88,12 +88,12 @@ optional<search_path> get_lean_path_from_env() {
for (; j < sz; j++) {
if (is_path_sep(lean_path[j])) {
if (j > i)
path.push_back(lean_path.substr(i, j - i));
path.push_back(lrealpath(lean_path.substr(i, j - i)));
i = j + 1;
}
}
if (j > i)
path.push_back(lean_path.substr(i, j - i));
path.push_back(lrealpath(lean_path.substr(i, j - i)));
return optional<search_path>(path);
} else {
return optional<search_path>();
@ -104,8 +104,12 @@ search_path get_builtin_search_path() {
search_path path;
#if !defined(LEAN_EMSCRIPTEN)
std::string exe_path = dirname(get_exe_location());
path.push_back(exe_path + get_dir_sep() + ".." + get_dir_sep() + "library");
path.push_back(exe_path + get_dir_sep() + ".." + get_dir_sep() + "lib" + get_dir_sep() + "lean" + get_dir_sep() + "library");
auto lib_path = exe_path + get_dir_sep() + ".." + get_dir_sep() + "library";
if (exists(lib_path))
path.push_back(lrealpath(lib_path));
auto installed_lib_path = exe_path + get_dir_sep() + ".." + get_dir_sep() + "lib" + get_dir_sep() + "lean" + get_dir_sep() + "library";
if (exists(installed_lib_path))
path.push_back(lrealpath(installed_lib_path));
#endif
return path;
}
@ -227,6 +231,34 @@ std::string find_file(search_path const & paths, name const & fname, std::initia
return find_file(paths, fname.to_string(get_dir_sep()), exts);
}
name module_name_of_file(search_path const & paths, std::string const & fname0) {
auto fname = normalize_path(fname0);
lean_assert(is_lean_file(fname));
fname = fname.substr(0, fname.size() - std::string(".lean").size());
for (auto & path : paths) {
if (path.size() < fname.size() && fname.substr(0, path.size()) == path) {
size_t pos = path.size();
if (fname[pos] == get_dir_sep_ch())
pos++;
name n;
while (pos < fname.size()) {
auto sep_pos = fname.find(get_dir_sep_ch(), pos);
n = name(n, fname.substr(pos, sep_pos - pos).c_str());
pos = sep_pos;
if (pos != std::string::npos)
pos++;
}
return n;
}
}
throw exception(sstream() << "file '" << fname0 << "' not part of any known Lean packages");
}
module_name absolutize_module_name(search_path const & path, std::string const & base, rel_module_name const & rel) {
// TODO(Sebastian): Should make sure that the result of `find_file` is still in the same package as `base`
return module_name_of_file(path, find_file(path, base, rel.m_updirs, rel.m_name, ".lean"));
}
void find_imports_core(std::string const & base, optional<unsigned> const & k,
std::vector<pair<std::string, std::string>> & imports) {
std::vector<std::string> files;

35
src/util/lean_path.h
View file

@ -40,25 +40,38 @@ struct standard_search_path {
std::string get_exe_location();
#endif
/** \brief Hierarchical names are converted into paths using the path separator. Example: foo.bar is converted into foo/bar */
std::string find_file(search_path const &, name const & fname);
std::string find_file(search_path const &, name const & fname, std::initializer_list<char const *> const & exts);
/** \brief A module name is an absolute import path like 'init.lean.core'. We do not use actual absolute file paths
* because we store module names in .olean files, which should not be completely system-specific.
*/
using module_name = name;
struct rel_module_name {
optional<unsigned> m_updirs;
module_name m_name;
rel_module_name(unsigned int const & updirs, module_name const & name) : m_updirs(some(updirs)), m_name(name) {}
explicit rel_module_name(module_name const & name) : m_name(name) {}
};
/** \brief Hierarchical names are converted into paths using the path separator. Example: foo.bar is converted into 'foo/bar.lean' */
std::string find_file(search_path const &, module_name const & mod_name);
std::string find_file(search_path const &, module_name const & mod_name, std::initializer_list<char const *> const & exts);
/** \brief \brief Similar to previous find_file, but if k is not none then search at the k-th parent of base. */
std::string find_file(search_path const &, std::string const & base, optional<unsigned> const & rel, name const & fname,
std::string find_file(search_path const &, std::string const & base, optional<unsigned> const & rel, module_name const & mod_name,
std::initializer_list<char const *> const & extensions);
std::string find_file(search_path const &, std::string const & base, optional<unsigned> const & k, name const & fname, char const * ext);
std::string find_file(search_path const &, std::string const & base, optional<unsigned> const & k, module_name const & mod_name, char const * ext);
/** \brief Inverse function of \c find_file */
module_name module_name_of_file(search_path const &, std::string const & fname);
/** \brief Resolve path like '.instances' in 'library/init/data/list' to 'init.data.list.instances' */
module_name absolutize_module_name(search_path const &, std::string const & base, rel_module_name const & rel);
void find_imports(search_path const &, std::string const & base, optional<unsigned> const & k,
std::vector<pair<std::string, std::string>> & imports_and_files);
/** \brief Return true iff fname ends with ".lean" */
bool is_lean_file(std::string const & fname);
/** \brief Return true iff fname ends with ".olean" */
bool is_olean_file(std::string const & fname);
/** \brief Return a string that replaces hierachical name separator '::' with a path separator. */
std::string name_to_file(name const & fname);
std::string olean_of_lean(std::string const & lean_fn);
std::string olean_file_to_lean_file(std::string const & olean);
}