diff --git a/src/api/lean_module.h b/src/api/lean_module.h
index 26f3e35d75..f540c4565a 100644
--- a/src/api/lean_module.h
+++ b/src/api/lean_module.h
@@ -29,9 +29,6 @@ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, le
     \remark exceptions: LEAN_OTHER_EXCEPTION */
 lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex);
 
-/** \brief Store in \c r the LEAN_PATH */
-lean_bool lean_get_std_path(char const ** r, lean_exception * ex);
-
 /*@}*/
 /*@}*/
 
diff --git a/src/api/module.cpp b/src/api/module.cpp
index 45803d1b61..d6d377ba39 100644
--- a/src/api/module.cpp
+++ b/src/api/module.cpp
@@ -26,7 +26,7 @@ lean_bool lean_env_import(lean_env env, lean_ios ios, lean_list_name modules, le
     for (name const & n : to_list_name_ref(modules)) {
         imports.push_back({n, optional<unsigned>()});
     }
-    new_env = import_modules(new_env, "", imports, mk_olean_loader());
+    new_env = import_modules(new_env, "", imports, mk_olean_loader(standard_search_path().get_path()));
     *r = of_env(new environment(new_env));
     LEAN_CATCH;
 }
@@ -39,9 +39,3 @@ lean_bool lean_env_export(lean_env env, char const * fname, lean_exception * ex)
     write_module(lm, out);
     LEAN_CATCH;
 }
-
-lean_bool lean_get_std_path(char const ** r, lean_exception * ex) {
-    LEAN_TRY;
-    *r = mk_string(get_lean_path());
-    LEAN_CATCH;
-}
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 36ca274ca6..f5f1ba0f2c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2433,7 +2433,7 @@ bool parse_commands(environment & env, io_state & ios, char const * fname) {
     fs_module_vfs vfs;
     vfs.m_modules_to_load_from_source.insert(std::string(fname));
     log_tree lt;
-    module_mgr mod_mgr(&vfs, lt.get_root(), get_search_path(), env, ios);
+    module_mgr mod_mgr(&vfs, lt.get_root(), standard_search_path().get_path(), env, ios);
 
     auto mod = mod_mgr.get_module(fname);
     env = mod->get_produced_env();
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index d7a6980ba8..3cf6904e56 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -97,7 +97,6 @@ static void display_help(std::ostream & out) {
     std::cout << "  --version -v       display version number\n";
     std::cout << "  --githash          display the git commit hash number used to build this binary\n";
     std::cout << "  --run              executes the 'main' definition\n";
-    std::cout << "  --path             display the path used for finding Lean libraries and extensions\n";
     std::cout << "  --doc=file -r      generate module documentation based on module doc strings\n";
     std::cout << "  --make             create olean files\n";
     std::cout << "  --recursive        recursively find *.lean files in directory arguments\n";
@@ -114,6 +113,7 @@ 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";
@@ -133,7 +133,6 @@ static struct option g_long_options[] = {
     {"help",         no_argument,       0, 'h'},
     {"run",          required_argument, 0, 'a'},
     {"smt2",         no_argument,       0, 'Y'},
-    {"path",         no_argument,       0, 'p'},
     {"githash",      no_argument,       0, 'g'},
     {"make",         no_argument,       0, 'm'},
     {"recursive",    no_argument,       0, 'R'},
@@ -151,6 +150,7 @@ static struct option g_long_options[] = {
     {"timeout",      optional_argument, 0, 'T'},
 #if defined(LEAN_JSON)
     {"json",         no_argument,       0, 'J'},
+    {"path",         no_argument,       0, 'p'},
     {"server",       optional_argument, 0, 'S'},
 #endif
     {"doc",          required_argument, 0, 'r'},
@@ -352,7 +352,7 @@ int main(int argc, char ** argv) {
     bool json_output        = false;
 #endif
 
-    auto path = get_search_path();
+    standard_search_path path;
 
     options opts;
     optional<std::string> export_txt;
@@ -383,9 +383,6 @@ int main(int argc, char ** argv) {
         case 'Y':
             smt2 = true;
             break;
-        case 'p':
-            for (auto & p : path) std::cout << p << "\n";
-            return 0;
         case 's':
             lean::lthread::set_thread_stack_size(static_cast<size_t>((atoi(optarg)/4)*4)*static_cast<size_t>(1024));
             break;
@@ -440,6 +437,18 @@ int main(int argc, char ** argv) {
             opts = opts.update(lean::name{"trace", "as_messages"}, true);
             if (optarg) server_in = optional<std::string>(optarg);
             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);
@@ -497,7 +506,7 @@ int main(int argc, char ** argv) {
             std::cin.rdbuf(file_in->rdbuf());
         }
 
-        server(num_threads, path, env, ios).run();
+        server(num_threads, path.get_path(), env, ios).run();
         return 0;
     }
 #endif
@@ -519,7 +528,7 @@ int main(int argc, char ** argv) {
         for (int i = optind; i < argc; i++) {
             try {
                 if (doc) throw lean::exception("leandoc does not support .smt2 files");
-                ok = ::lean::smt2::parse_commands(path, env, ios, argv[i]);
+                ok = smt2::parse_commands(path.get_path(), env, ios, argv[i]);
             } catch (lean::exception & ex) {
                 ok = false;
                 type_context tc(env, ios.get_options());
@@ -545,7 +554,7 @@ int main(int argc, char ** argv) {
         set_task_queue(tq.get());
 
         fs_module_vfs vfs;
-        module_mgr mod_mgr(&vfs, lt.get_root(), path, env, ios);
+        module_mgr mod_mgr(&vfs, lt.get_root(), path.get_path(), env, ios);
 
         if (run_arg) {
             auto mod = mod_mgr.get_module(lrealpath(run_arg->c_str()));
@@ -607,7 +616,7 @@ int main(int argc, char ** argv) {
         if (only_deps) {
             for (auto & mod_fn : module_args) {
                 try {
-                    if (!display_deps(path, env, std::cout, std::cerr, mod_fn.c_str()))
+                    if (!display_deps(path.get_path(), env, std::cout, std::cerr, mod_fn.c_str()))
                         ok = false;
                 } catch (lean::exception &ex) {
                     ok = false;
diff --git a/src/shell/lean_js.cpp b/src/shell/lean_js.cpp
index d8642518cb..cfbac5070a 100644
--- a/src/shell/lean_js.cpp
+++ b/src/shell/lean_js.cpp
@@ -19,7 +19,11 @@ Author: Leonardo de Moura
 namespace lean {
 
 static search_path get_lean_js_path() {
-    return getenv("LEAN_PATH") ? get_search_path() : search_path {"/library"};
+    if (auto p = get_lean_path_from_env()) {
+        return *p;
+    } else {
+        return {"/library"};
+    }
 }
 
 class emscripten_shell {
diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp
index 84b6a1646d..fe659ce3e0 100644
--- a/src/util/lean_path.cpp
+++ b/src/util/lean_path.cpp
@@ -101,6 +101,23 @@ std::string get_exe_location() {
 bool is_path_sep(char c) { return c == g_path_sep; }
 #endif
 
+#if defined(LEAN_WINDOWS)
+std::string resolve(std::string const & rel_or_abs, std::string const & base) {
+    // TODO(gabriel): detect absolute pathnames
+    return base + g_sep + rel_or_abs;
+}
+#else
+std::string resolve(std::string const & rel_or_abs, std::string const & base) {
+    if (!rel_or_abs.empty() && rel_or_abs[0] == g_sep) {
+        // absolute
+        return rel_or_abs;
+    } else {
+        // relative
+        return base + g_sep + rel_or_abs;
+    }
+}
+#endif
+
 std::string normalize_path(std::string f) {
     for (auto & c : f) {
         if (c == g_bad_sep)
@@ -121,33 +138,6 @@ std::string get_path(std::string f) {
     }
 }
 
-search_path get_search_path() {
-    search_path path;
-
-    if (auto r = getenv("LEAN_PATH")) {
-        auto lean_path = normalize_path(r);
-        unsigned i  = 0;
-        unsigned j  = 0;
-        unsigned sz = static_cast<unsigned>(lean_path.size());
-        for (; j < sz; j++) {
-            if (is_path_sep(lean_path[j])) {
-                if (j > i)
-                    path.push_back(lean_path.substr(i, j - i));
-                i = j + 1;
-            }
-        }
-        if (j > i)
-            path.push_back(lean_path.substr(i, j - i));
-    } else {
-        std::string exe_path = get_path(get_exe_location());
-        path.push_back(exe_path + g_sep + ".." + g_sep + "library");
-        path.push_back(exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "library");
-        path.push_back(".");
-    }
-
-    return path;
-}
-
 static char g_sep_str[2];
 
 void initialize_lean_path() {
@@ -162,6 +152,108 @@ void finalize_lean_path() {
     delete g_default_file_name;
 }
 
+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 + g_sep_str + "leanpkg.path";
+        if (exists(fn)) return optional<std::string>(fn);
+
+        auto i = dir.rfind(g_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
+    return std::string(getenv("HOME")) + g_sep + ".lean" + g_sep + "leanpkg.path";
+}
+
+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(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);
+        unsigned i  = 0;
+        unsigned j  = 0;
+        unsigned sz = static_cast<unsigned>(lean_path.size());
+        search_path path;
+        for (; j < sz; j++) {
+            if (is_path_sep(lean_path[j])) {
+                if (j > i)
+                    path.push_back(lean_path.substr(i, j - i));
+                i = j + 1;
+            }
+        }
+        if (j > i)
+            path.push_back(lean_path.substr(i, j - i));
+        return optional<search_path>(path);
+    } else {
+        return optional<search_path>();
+    }
+}
+
+search_path get_builtin_search_path() {
+    search_path path;
+    std::string exe_path = get_path(get_exe_location());
+    path.push_back(exe_path + g_sep + ".." + g_sep + "library");
+    path.push_back(exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean" + g_sep + "library");
+    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 has_file_ext(std::string const & fname, char const * ext) {
     unsigned ext_len = strlen(ext);
     return fname.size() > ext_len && fname.substr(fname.size() - ext_len, ext_len) == ext;
diff --git a/src/util/lean_path.h b/src/util/lean_path.h
index ce06a39113..b4ff7193eb 100644
--- a/src/util/lean_path.h
+++ b/src/util/lean_path.h
@@ -18,7 +18,22 @@ public:
 };
 
 using search_path = std::vector<std::string>;
-search_path get_search_path();
+
+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();
@@ -51,7 +66,9 @@ std::string name_to_file(name const & fname);
 */
 void display_path(std::ostream & out, std::string const & fname);
 
+std::string resolve(std::string const & rel_or_abs, std::string const & base);
 std::string dirname(char const * fname);
+inline std::string dirname(std::string const & fn) { return dirname(fn.c_str()); }
 std::string path_append(char const * path1, char const * path2);
 
 std::string olean_of_lean(std::string const & lean_fn);