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

refactor(util/lean_path): support leanpkg.path files

Browse source
This commit is contained in:
Gabriel Ebner 2017-04-12 15:57:21 +02:00 • committed by Leonardo de Moura
parent baa4c48f1f
commit d79909a1b8
7 changed files with 163 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/lean_module.h
View file

@ -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);
/*@}*/
/*@}*/

8
src/api/module.cpp
View file

@ -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;
}

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

@ -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();

29
src/shell/lean.cpp
View file

@ -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;

6
src/shell/lean_js.cpp
View file

@ -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 {

146
src/util/lean_path.cpp
View file

@ -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;

19
src/util/lean_path.h
View file

@ -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);