feat(library/module): relative module path

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/Makefile.common

@@ -1,5 +1,6 @@
 TOP := $(dir $(lastword $(MAKEFILE_LIST)))
-LEAN_FILES = $(shell find . -type f -name '*.lean')
+DIR = $(shell pwd)
+LEAN_FILES = $(shell find $(DIR) -type f -name '*.lean')
 OLEAN_FILES = $(LEAN_FILES:.lean=.olean)
 DEP_FILES = $(LEAN_FILES:.lean=.d)
 

src/frontends/lean/parser.cpp

@@ -1033,7 +1033,7 @@ void parser::parse_script(bool as_expr) {
         });
 }
 
-static optional<std::string> find_file(name const & f, char const * ext) {
+static optional<std::string> try_file(name const & f, char const * ext) {
     try {
         return optional<std::string>(find_file(f, {ext}));
     } catch (...) {
@@ -1041,6 +1041,14 @@ static optional<std::string> find_file(name const & f, char const * ext) {
     }
 }
 
+static optional<std::string> try_file(std::string const & base, optional<unsigned> const & k, name const & f, char const * ext) {
+    try {
+        return optional<std::string>(find_file(base, k, f, ext));
+    } catch (...) {
+        return optional<std::string>();
+    }
+}
+
 static std::string g_lua_module_key("lua_module");
 static void lua_module_reader(deserializer & d, module_idx, shared_environment &,
                               std::function<void(asynch_update_fn const &)> &,
@@ -1056,17 +1064,31 @@ static void lua_module_reader(deserializer & d, module_idx, shared_environment &
 register_module_object_reader_fn g_lua_module_reader(g_lua_module_key, lua_module_reader);
 
 void parser::parse_imports() {
-    buffer<name> olean_files;
+    buffer<module_name> olean_files;
-    buffer<name> lua_files;
+    buffer<name>        lua_files;
+    std::string base = dirname(get_stream_name().c_str());
     while (curr_is_token(g_import)) {
         m_last_cmd_pos = pos();
         next();
-        while (curr_is_identifier()) {
+        while (true) {
+            optional<unsigned> k;
+            while (curr_is_token(g_period)) {
+                next();
+                if (!k)
+                    k = 0;
+                else
+                    k = *k + 1;
+            }
+            if (!curr_is_identifier())
+                break;
             name f            = get_name_val();
-            if (auto it = find_file(f, ".lua")) {
+            if (auto it = try_file(f, ".lua")) {
+                if (k)
+                    throw parser_error(sstream() << "invalid import, failed to import '" << f
+                                       << "', relative paths are not supported for .lua files", pos());
                 lua_files.push_back(f);
-            } else if (auto it = find_file(f, ".olean")) {
+            } else if (auto it = try_file(base, k, f, ".olean")) {
-                olean_files.push_back(f);
+                olean_files.push_back(module_name(k, f));
             } else {
                 m_found_errors = true;
                 if (!m_use_exceptions && m_show_errors) {
@@ -1083,7 +1105,7 @@ void parser::parse_imports() {
     unsigned num_threads = 0;
     if (get_parser_parallel_import(m_ios.get_options()))
         num_threads = m_num_threads;
-    m_env = import_modules(m_env, olean_files.size(), olean_files.data(), num_threads, true, m_ios);
+    m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads, true, m_ios);
     for (auto const & f : lua_files) {
         std::string rname = find_file(f, {".lua"});
         system_import(rname.c_str());

src/library/kernel_bindings.cpp

@@ -1056,16 +1056,16 @@ static int environment_for_each_universe(lua_State * L) {
     return 0;
 }
 
-static void to_name_buffer(lua_State * L, int i, buffer<name> & r) {
+static void to_module_name_buffer(lua_State * L, int i, buffer<module_name> & r) {
     if (lua_isstring(L, i) || is_name(L, i)) {
-        r.push_back(to_name_ext(L, i));
+        r.push_back(module_name(to_name_ext(L, i)));
     } else {
         luaL_checktype(L, i, LUA_TTABLE);
         lua_pushvalue(L, i);
         int sz = objlen(L, -1);
         for (int i = 1; i <= sz; i++) {
             lua_rawgeti(L, -1, i);
-            r.push_back(to_name_ext(L, -1));
+            r.push_back(module_name(to_name_ext(L, -1)));
             lua_pop(L, 1);
         }
     }
@@ -1073,18 +1073,19 @@ static void to_name_buffer(lua_State * L, int i, buffer<name> & r) {
 
 static int import_modules(environment const & env, lua_State * L, int s) {
     int nargs = lua_gettop(L);
-    buffer<name> mnames;
+    buffer<module_name> mnames;
-    to_name_buffer(L, s, mnames);
+    to_module_name_buffer(L, s, mnames);
     unsigned num_threads = 1;
     bool     keep_proofs = false;
     if (nargs > s) {
         num_threads = get_uint_named_param(L, s+1, "num_threads", num_threads);
         keep_proofs = get_bool_named_param(L, s+1, "keep_proofs", keep_proofs);
     }
+    std::string base;
     if (nargs > s+1 && is_io_state(L, s+2))
-        return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, to_io_state(L, s+2)));
+        return push_environment(L, import_modules(env, base, mnames.size(), mnames.data(), num_threads, keep_proofs, to_io_state(L, s+2)));
     else
-        return push_environment(L, import_modules(env, mnames.size(), mnames.data(), num_threads, keep_proofs, get_io_state(L)));
+        return push_environment(L, import_modules(env, base, mnames.size(), mnames.data(), num_threads, keep_proofs, get_io_state(L)));
 }
 
 static int import_modules(lua_State * L) {

src/library/module.cpp

@@ -31,8 +31,8 @@ namespace lean {
 typedef std::pair<std::string, std::function<void(serializer &)>> writer;
 
 struct module_ext : public environment_extension {
-    list<name>   m_direct_imports;
+    list<module_name> m_direct_imports;
-    list<writer> m_writers;
+    list<writer>      m_writers;
 };
 
 struct module_ext_reg {
@@ -51,9 +51,29 @@ 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.is_relative())
+        s << true << *n.get_k() << n.get_name();
+    else
+        s << false << n.get_name();
+    return s;
+}
+
+module_name read_module_name(deserializer & d) {
+    if (d.read_bool()) {
+        unsigned k; name n;
+        d >> k >> n;
+        return module_name(k, n);
+    } else {
+        name n;
+        d >> n;
+        return module_name(n);
+    }
+}
+
 void export_module(std::ostream & out, environment const & env) {
     module_ext const & ext = get_extension(env);
-    buffer<name> imports;
+    buffer<module_name> imports;
     buffer<writer const *> writers;
     to_buffer(ext.m_direct_imports, imports);
     std::reverse(imports.begin(), imports.end());
@@ -171,7 +191,6 @@ struct import_modules_fn {
     atomic<bool>                   m_all_modules_imported;
 
     struct module_info {
-        name                                      m_name;
         std::string                               m_fname;
         atomic<unsigned>                          m_counter; // number of dependencies to be processed
         unsigned                                  m_module_idx;
@@ -198,11 +217,12 @@ struct import_modules_fn {
         }
     }
 
-    module_info_ptr load_module_file(name const & mname) {
+    module_info_ptr load_module_file(std::string const & base, module_name const & mname) {
-        auto it = m_module_info.find(mname);
+        // TODO(Leo): support module_name
+        std::string fname = find_file(base, mname.get_k(), mname.get_name(), {".olean"});
+        auto it    = m_module_info.find(fname);
         if (it)
             return *it;
-        std::string fname = find_file(mname, {".olean"});
         if (m_visited.contains(fname))
             throw exception(sstream() << "circular dependency detected at '" << fname << "'");
         m_visited.insert(fname);
@@ -219,9 +239,9 @@ struct import_modules_fn {
         // Enforce version?
 
         unsigned num_imports  = d1.read_unsigned();
-        buffer<name> imports;
+        buffer<module_name> imports;
         for (unsigned i = 0; i < num_imports; i++)
-            imports.push_back(read_name(d1));
+            imports.push_back(read_module_name(d1));
 
         unsigned code_size    = d1.read_unsigned();
         std::vector<char> code(code_size);
@@ -233,17 +253,17 @@ struct import_modules_fn {
             throw exception(sstream() << "file '" << fname << "' has been corrupted, checksum mismatch");
 
         module_info_ptr r = std::make_shared<module_info>();
-        r->m_name         = mname;
         r->m_fname        = fname;
         r->m_counter      = imports.size();
         r->m_module_idx   = g_null_module_idx;
         m_import_counter++;
+        std::string new_base = dirname(fname.c_str());
         std::swap(r->m_obj_code, code);
         for (auto i : imports) {
-            auto d = load_module_file(i);
+            auto d = load_module_file(new_base, i);
             d->m_dependents.push_back(r);
         }
-        m_module_info.insert(mname, r);
+        m_module_info.insert(fname, r);
         r->m_module_idx = m_next_module_idx++;
 
         if (imports.empty())
@@ -425,31 +445,31 @@ struct import_modules_fn {
         return env;
     }
 
-    void store_direct_imports(unsigned num_modules, name const * modules) {
+    void store_direct_imports(unsigned num_modules, module_name const * modules) {
         m_senv.update([&](environment const & env) -> environment {
                 module_ext ext = get_extension(env);
                 for (unsigned i = 0; i < num_modules; i++)
-                    ext.m_direct_imports = list<name>(modules[i], ext.m_direct_imports);
+                    ext.m_direct_imports = cons(modules[i], ext.m_direct_imports);
                 return update(env, ext);
             });
     }
 
-    environment operator()(unsigned num_modules, name const * modules) {
+    environment operator()(std::string const & base, unsigned num_modules, module_name const * modules) {
         store_direct_imports(num_modules, modules);
         for (unsigned i = 0; i < num_modules; i++)
-            load_module_file(modules[i]);
+            load_module_file(base, modules[i]);
         process_asynch_tasks();
         return process_delayed_tasks();
     }
 };
 
-environment import_modules(environment const & env, unsigned num_modules, name const * modules,
+environment import_modules(environment const & env, std::string const & base, unsigned num_modules, module_name const * modules,
                            unsigned num_threads, bool keep_proofs, io_state const & ios) {
-    return import_modules_fn(env, num_threads, keep_proofs, ios)(num_modules, modules);
+    return import_modules_fn(env, num_threads, keep_proofs, ios)(base, num_modules, modules);
 }
 
-environment import_module(environment const & env, name const & module,
+environment import_module(environment const & env, std::string const & base, module_name const & module,
                           unsigned num_threads, bool keep_proofs, io_state const & ios) {
-    return import_modules(env, 1, &module, num_threads, keep_proofs, ios);
+    return import_modules(env, base, 1, &module, num_threads, keep_proofs, ios);
 }
 }

src/library/module.h

@@ -8,11 +8,24 @@ Author: Leonardo de Moura
 #include <string>
 #include <iostream>
 #include "util/serializer.h"
+#include "util/optional.h"
 #include "kernel/inductive/inductive.h"
 #include "library/shared_environment.h"
 #include "library/io_state.h"
 
 namespace lean {
+class module_name {
+    optional<unsigned> m_relative;
+    name               m_name;
+public:
+    module_name(name const & n):m_name(n) {}
+    module_name(unsigned k, name const & n):m_relative(k), m_name(n) {}
+    module_name(optional<unsigned> const & k, name const & n):m_relative(k), m_name(n) {}
+    name const & get_name() const { return m_name; }
+    bool is_relative() const { return static_cast<bool>(m_relative); }
+    optional<unsigned> const & get_k() const { return m_relative; }
+};
+
 /**
    \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.
@@ -21,9 +34,9 @@ namespace lean {
    If \c keep_proofs is false, then the proof of the imported theorems is discarded after being
    checked. The idea is to save memory.
 */
-environment import_modules(environment const & env, unsigned num_modules, name const * modules,
+environment import_modules(environment const & env, std::string const & base, unsigned num_modules, module_name const * modules,
                            unsigned num_threads, bool keep_proofs, io_state const & ios);
-environment import_module(environment const & env, name const & module,
+environment import_module(environment const & env, std::string const & base, module_name const & module,
                           unsigned num_threads, bool keep_proofs, io_state const & ios);
 
 /**

src/util/lean_path.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/name.h"
 #include "util/optional.h"
+#include "util/realpath.h"
 
 #ifndef LEAN_DEFAULT_MODULE_FILE_NAME
 #define LEAN_DEFAULT_MODULE_FILE_NAME "default"
@@ -218,7 +219,7 @@ optional<std::string> check_file(std::string const & path, std::string const & f
         file += ext;
     std::ifstream ifile(file);
     if (ifile)
-        return optional<std::string>(file);
+        return optional<std::string>(realpath(file.c_str()));
     else
         return optional<std::string>();
 }
@@ -244,6 +245,21 @@ std::string find_file(std::string fname, std::initializer_list<char const *> con
     throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH");
 }
 
+std::string find_file(std::string const & base, optional<unsigned> const & rel, name const & fname, char const * ext) {
+    if (!rel) {
+        return find_file(fname.to_string(g_sep_str.c_str()), {ext});
+    } else {
+        auto path = base;
+        for (unsigned i = 0; i < *rel; i++) {
+            path += g_sep;
+            path += "..";
+        }
+        if (auto r = check_file(path, fname.to_string(g_sep_str.c_str()), ext))
+            return *r;
+        throw exception(sstream() << "file '" << fname << "' not found at '" << path << "'");
+    }
+}
+
 std::string find_file(std::string fname) {
     return find_file(fname, {".olean", ".lean", ".lua"});
 }

src/util/lean_path.h

@@ -23,6 +23,9 @@ std::string find_file(std::string fname, std::initializer_list<char const *> con
 std::string find_file(name const & fname);
 std::string find_file(name const & fname, 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(std::string const & base, optional<unsigned> const & k, name const & fname, char const * ext);
+
 /** \brief Return true iff fname ends with ".lean" */
 bool is_lean_file(std::string const & fname);
 /** \brief Return true iff fname ends with ".olean" */