Remove leanpkg.path support

src/library/module.cpp

@@ -105,8 +105,8 @@ extern "C" object * lean_find_olean(object * mod_name, object * w) {
 
 extern "C" object * lean_set_search_path(object * w) {
     try {
-        standard_search_path path;
-        set_search_path(path.get_path());
+        search_path path = get_lean_path_from_env().value_or(get_builtin_search_path());
+        set_search_path(path);
         return w;
     } catch (exception & ex) {
         return set_io_error(w, ex.what());

src/shell/CMakeLists.txt

@@ -22,7 +22,7 @@ add_custom_target(stdlib
   # '-G Ninja' complains otherwise
   BYPRODUCTS "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a"
   WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
-  COMMAND make -j8 "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$<TARGET_FILE:lean_stage0>" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1"
+  COMMAND ${CMAKE_COMMAND} -E env "LEAN_PATH=." make -j8 "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" "LEAN=$<TARGET_FILE:lean_stage0>" "LEANC_OPTS=${LEANC_OPTS}" "STAGE1_OUT=${CMAKE_BINARY_DIR}/stage1"
   DEPENDS lean_stage0)
 install(FILES "${CMAKE_BINARY_DIR}/stage1/libleanstdlib.a" DESTINATION lib)
 
@@ -92,8 +92,6 @@ add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
 endif()
 add_test(lean_ghash1   "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
 add_test(lean_ghash2   "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
-add_test(lean_path1    "${CMAKE_CURRENT_BINARY_DIR}/lean" -p)
-add_test(lean_path2    "${CMAKE_CURRENT_BINARY_DIR}/lean" --path)
 add_test(lean_new_frontend "${CMAKE_CURRENT_BINARY_DIR}/lean" --new-frontend "${LEAN_SOURCE_DIR}/../library/init/core.lean")
 add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
 add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")

src/shell/lean.cpp

@@ -197,7 +197,6 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "  --deps             just print dependencies of a Lean input\n";
 #if defined(LEAN_JSON)
-    std::cout << "  --path             display the path used for finding Lean libraries and extensions\n";
     std::cout << "  --json             print JSON-formatted structured error messages\n";
     std::cout << "  --server           start lean in server mode\n";
     std::cout << "  --server=file      start lean in server mode, redirecting standard input from the specified file (for debugging)\n";
@@ -228,7 +227,6 @@ static struct option g_long_options[] = {
     {"cpp",          optional_argument, 0, 'c'},
 #if defined(LEAN_JSON)
     {"json",         no_argument,       0, 'J'},
-    {"path",         no_argument,       0, 'p'},
     {"server",       optional_argument, 0, 'S'},
 #endif
     {"new-frontend", optional_argument, 0, 'n'},
@@ -242,7 +240,7 @@ static struct option g_long_options[] = {
 };
 
 static char const * g_opt_str =
-    "PdD:c:qpgvht:012j:012rM:012T:012a"
+    "PdD:c:qgvht:012j:012rM:012T:012a"
 #if defined(LEAN_MULTI_THREAD)
     "s:012"
 #endif
@@ -337,7 +335,7 @@ int main(int argc, char ** argv) {
     bool json_output = false;
 #endif
 
-    standard_search_path path;
+    search_path path = get_lean_path_from_env().value_or(get_builtin_search_path());
 
     options opts;
     optional<std::string> server_in;
@@ -404,19 +402,6 @@ int main(int argc, char ** argv) {
                 opts = opts.update(lean::name{"trace", "as_messages"}, true);
                 json_output = true;
                 break;
-            case 'p': {
-                json out;
-
-                auto & out_path = out["path"] = json::array();
-                for (auto & p : path.get_path()) out_path.push_back(p);
-
-                out["leanpkg_path_file"] = path.m_leanpkg_path_fn ? *path.m_leanpkg_path_fn
-                                                                  : path.m_user_leanpkg_path_fn;
-                out["is_user_leanpkg_path"] = !path.m_leanpkg_path_fn;
-
-                std::cout << std::setw(2) << out << std::endl;
-                return 0;
-            }
 #endif
             case 'P':
                 opts = opts.update("profiler", true);
@@ -484,7 +469,7 @@ int main(int argc, char ** argv) {
         }
         mod_fn = lrealpath(argv[optind]);
         contents = read_file(mod_fn);
-        search_path input_path = path.get_path();
+        search_path input_path = path;
         /* We accept stand-alone files as input, but imports should always be part of a package so that we can give
          * them a (stable) absolute name. */
         input_path.push_back(dirname(mod_fn));
@@ -509,11 +494,11 @@ int main(int argc, char ** argv) {
             std::vector<module_name> imports;
             auto dir = dirname(mod_fn);
             for (auto const & rel : rel_imports)
-                imports.push_back(absolutize_module_name(path.get_path(), dir, rel));
+                imports.push_back(absolutize_module_name(path, dir, rel));
 
             if (only_deps) {
                 for (auto const & import : imports) {
-                    std::string m_name = find_file(path.get_path(), import, {".lean"});
+                    std::string m_name = find_file(path, import, {".lean"});
                     auto last_idx = m_name.find_last_of(".");
                     std::string rawname = m_name.substr(0, last_idx);
                     std::string ext = m_name.substr(last_idx);
@@ -525,7 +510,7 @@ int main(int argc, char ** argv) {
 
             message_log l;
             scope_message_log scope_log(l);
-            set_search_path(path.get_path());
+            set_search_path(path);
             if (stats) {
                 timeit timer(std::cout, "import");
                 env = import_modules(trust_lvl, imports);
@@ -570,7 +555,7 @@ int main(int argc, char ** argv) {
                 std::cerr << "failed to create '" << *cpp_output << "'\n";
                 return 1;
             }
-            auto mod = module_name_of_file(path.get_path(), mod_fn);
+            auto mod = module_name_of_file(path, mod_fn);
             out << lean::ir::emit_cpp(env, mod).data();
             out.close();
         }

src/util/lean_path.cpp

@@ -26,58 +26,6 @@ static bool exists(std::string const & fn) {
     return !!std::ifstream(fn);
 }
 
-optional<std::string> get_leanpkg_path_file() {
-    auto dir = lrealpath(".");
-    while (true) {
-        auto fn = dir + get_dir_sep() + "leanpkg.path";
-        if (exists(fn)) return optional<std::string>(fn);
-
-        auto i = dir.rfind(get_dir_sep());
-        if (i == std::string::npos) {
-            return optional<std::string>();
-        } else {
-            dir = dir.substr(0, i);
-        }
-    }
-}
-
-std::string get_user_leanpkg_path() {
-    // TODO(gabriel): check if this works on windows
-    if (auto home = getenv("HOME")) {
-        return std::string(home) + get_dir_sep() + ".lean" + get_dir_sep() + "leanpkg.path";
-    } else {
-        return "/could-not-find-home";
-    }
-}
-
-static optional<std::string> begins_with(std::string const & s, std::string const & prefix) {
-    if (prefix.size() <= s.size() && s.substr(0, prefix.size()) == prefix) {
-        return optional<std::string>(s.substr(prefix.size(), s.size()));
-    } else {
-        return optional<std::string>();
-    }
-}
-
-search_path parse_leanpkg_path(std::string const & fn) {
-    std::ifstream in(fn);
-    if (!in) throw exception(sstream() << "cannot open " << fn);
-    auto fn_dir = dirname(fn);
-    search_path path;
-    while (!in.eof()) {
-        std::string line;
-        std::getline(in, line);
-
-        if (auto rest = begins_with(line, "path "))
-            path.push_back(lrealpath(resolve(*rest, fn_dir)));
-
-        if (line == "builtin_path") {
-            auto builtin = get_builtin_search_path();
-            path.insert(path.end(), builtin.begin(), builtin.end());
-        }
-    }
-    return path;
-}
-
 optional<search_path> get_lean_path_from_env() {
     if (auto r = getenv("LEAN_PATH")) {
         auto lean_path = normalize_path(r);
@@ -114,26 +62,6 @@ search_path get_builtin_search_path() {
     return path;
 }
 
-standard_search_path::standard_search_path() {
-    m_builtin = get_builtin_search_path();
-
-    m_from_env = get_lean_path_from_env();
-    m_leanpkg_path_fn = get_leanpkg_path_file();
-    m_user_leanpkg_path_fn = get_user_leanpkg_path();
-
-    if (m_leanpkg_path_fn) {
-        m_from_leanpkg_path = parse_leanpkg_path(*m_leanpkg_path_fn);
-    } else if (exists(m_user_leanpkg_path_fn)) {
-        m_from_leanpkg_path = parse_leanpkg_path(m_user_leanpkg_path_fn);
-    }
-}
-
-search_path standard_search_path::get_path() const {
-    if (m_from_env) return *m_from_env;
-    if (m_from_leanpkg_path) return *m_from_leanpkg_path;
-    return m_builtin;
-}
-
 bool is_lean_file(std::string const & fname) {
     return has_file_ext(fname, ".lean");
 }
@@ -169,10 +97,6 @@ optional<std::string> check_file(std::string const & path, std::string const & f
     return check_file_core(file, ext);
 }
 
-std::string name_to_file(name const & fname) {
-    return fname.to_string(get_dir_sep());
-}
-
 static std::string find_file(search_path const & paths, std::string fname, std::initializer_list<char const *> const & extensions) {
     bool is_known = is_known_file_ext(fname);
     fname = normalize_path(fname);
@@ -259,24 +183,6 @@ module_name absolutize_module_name(search_path const & path, std::string const &
     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;
-    find_files(base, ".lean", files);
-    find_files(base, ".olean", files);
-
-    for (auto const & file : files) {
-        auto import = file.substr(base.size() + 1, file.rfind('.') - (base.size() + 1));
-        std::replace(import.begin(), import.end(), get_dir_sep_ch(), '.');
-        if (k)
-            import = std::string(*k + 1, '.') + import;
-        auto n = import.rfind(".default");
-        if (n != static_cast<unsigned>(-1) && n == import.size() - std::string(".default").size())
-            import = import.substr(0, n);
-        imports.push_back({import, file});
-    }
-}
-
 std::string olean_of_lean(std::string const & lean_fn) {
     if (lean_fn.size() > 5 && lean_fn.substr(lean_fn.size() - 5) == ".lean") {
         return lean_fn.substr(0, lean_fn.size() - 5) + ".olean";

src/util/lean_path.h

@@ -20,22 +20,9 @@ class lean_file_not_found_exception : public exception {
 
 using search_path = std::vector<std::string>;
 
-optional<std::string> get_leanpkg_path_file();
-search_path parse_leanpkg_path(std::string const & fn);
 optional<search_path> get_lean_path_from_env();
 search_path get_builtin_search_path();
 
-struct standard_search_path {
-    search_path m_builtin;
-    optional<search_path> m_from_env;
-    optional<std::string> m_leanpkg_path_fn;
-    std::string m_user_leanpkg_path_fn;
-    optional<search_path> m_from_leanpkg_path;
-
-    standard_search_path();
-    search_path get_path() const;
-};
-
 #if !defined(LEAN_EMSCRIPTEN)
 std::string get_exe_location();
 #endif