From af99f153f803eb77486b1cfb57bc0e236abaebed Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 11 Sep 2018 10:53:26 -0700
Subject: [PATCH] refactor(library/module{,_mgr},frontends/lean/parser): use
 absolute module names everywhere for identifying modules, move actual
 importing from parser to module_mgr

---
 src/frontends/lean/elaborator.cpp |   4 +-
 src/frontends/lean/parser.cpp     |  52 ++--------
 src/frontends/lean/parser.h       |   7 +-
 src/library/module.cpp            | 108 +++++++--------------
 src/library/module.h              |  38 +++-----
 src/library/module_mgr.cpp        | 151 +++++++++++-------------------
 src/library/module_mgr.h          |  24 ++---
 src/shell/lean.cpp                |   8 +-
 src/util/lean_path.cpp            |  42 ++++++++-
 src/util/lean_path.h              |  35 ++++---
 10 files changed, 189 insertions(+), 280 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 9e17ab6d64..8c5d329744 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -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();
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 0458cd559a..8eddf77620 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -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() {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 85ce9025b5..a2ef6a60dc 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -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:
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 6090f6af9a..4e3bed564b 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -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();
diff --git a/src/library/module.h b/src/library/module.h
index 9e148afa73..ac25801ab1 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -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:
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index f8c60fa027..dfe0a7140d 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -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;
 }
 
diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h
index e256f4cdae..482c115f84 100644
--- a/src/library/module_mgr.h
+++ b/src/library/module_mgr.h
@@ -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; }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index af6de6c76d..27a2f33dc4 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -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);
             }
         }
diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index e55737ac01..6a569aad21 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -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;
diff --git a/src/util/lean_path.h b/src/util/lean_path.h
index 27f7b9cf8b..65eb6d3d33 100644
--- a/src/util/lean_path.h
+++ b/src/util/lean_path.h
@@ -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);
 }