From f78e57fd52c4afa838aa08c8637b21beb96e7d61 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2015 08:31:09 -0800 Subject: [PATCH] feat(shell,frontends/lean): add command line option --dir See #821 See #788 --- src/api/parser.cpp | 7 ++++--- src/frontends/lean/parser.cpp | 15 +++++++++------ src/frontends/lean/parser.h | 8 +++++--- src/frontends/lean/server.cpp | 22 +++++++++++++--------- src/frontends/lean/server.h | 29 ++++++++++++++++------------- src/shell/CMakeLists.txt | 3 +++ src/shell/emscripten.cpp | 2 +- src/shell/lean.cpp | 14 ++++++++++---- tests/lean/extra/dir_option.lean | 5 +++++ 9 files changed, 66 insertions(+), 39 deletions(-) create mode 100644 tests/lean/extra/dir_option.lean diff --git a/src/api/parser.cpp b/src/api/parser.cpp index 2ec8041577..c5640c3d22 100644 --- a/src/api/parser.cpp +++ b/src/api/parser.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "frontends/lean/parser.h" #include "api/string.h" #include "api/exception.h" @@ -21,7 +22,7 @@ lean_bool lean_parse_file(lean_env env, lean_ios ios, char const * fname, lean_e io_state _ios = to_io_state_ref(ios); bool use_exceptions = true; unsigned num_threads = 1; - parse_commands(_env, _ios, fname, use_exceptions, num_threads); + parse_commands(_env, _ios, fname, optional(), use_exceptions, num_threads); *new_env = of_env(new environment(_env)); *new_ios = of_io_state(new io_state(_ios)); LEAN_CATCH; @@ -38,7 +39,7 @@ lean_bool lean_parse_commands(lean_env env, lean_ios ios, char const * str, lean io_state _ios = to_io_state_ref(ios); bool use_exceptions = true; unsigned num_threads = 1; - parse_commands(_env, _ios, in, strname, use_exceptions, num_threads); + parse_commands(_env, _ios, in, strname, optional(), use_exceptions, num_threads); *new_env = of_env(new environment(_env)); *new_ios = of_io_state(new io_state(_ios)); LEAN_CATCH; @@ -55,7 +56,7 @@ lean_bool lean_parse_expr(lean_env env, lean_ios ios, char const * str, lean_exp io_state _ios = to_io_state_ref(ios); bool use_exceptions = true; unsigned num_threads = 1; - parser p(_env, _ios, in, strname, use_exceptions, num_threads); + parser p(_env, _ios, in, strname, optional(), use_exceptions, num_threads); expr e = p.parse_expr(); expr _e; level_param_names _ps; std::tie(_e, _ps) = p.elaborate(e, list()); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 697b66d08d..0bc1aaf370 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -122,13 +122,14 @@ void parser::init_stop_at(options const & opts) { } parser::parser(environment const & env, io_state const & ios, - std::istream & strm, char const * strm_name, + std::istream & strm, char const * strm_name, optional const & base_dir, bool use_exceptions, unsigned num_threads, snapshot const * s, snapshot_vector * sv, info_manager * im, keep_theorem_mode tmode): m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name, s ? s->m_line : 1), + m_base_dir(base_dir), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { m_local_decls_size_at_beg_cmd = 0; @@ -2001,7 +2002,7 @@ void parser::parse_imports() { buffer olean_files; buffer lua_files; bool prelude = false; - std::string base = dirname(get_stream_name().c_str()); + std::string base = m_base_dir ? *m_base_dir : dirname(get_stream_name().c_str()); bool imported = false; unsigned fingerprint = 0; if (curr_is_token(get_prelude_tk())) { @@ -2289,10 +2290,11 @@ void parser::save_type_info(expr const & e) { } } -bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, +bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, + optional const & base_dir, bool use_exceptions, unsigned num_threads, definition_cache * cache, declaration_index * index, keep_theorem_mode tmode) { - parser p(env, ios, in, strm_name, use_exceptions, num_threads, nullptr, nullptr, nullptr, tmode); + parser p(env, ios, in, strm_name, base_dir, use_exceptions, num_threads, nullptr, nullptr, nullptr, tmode); p.set_cache(cache); p.set_index(index); bool r = p(); @@ -2301,12 +2303,13 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c return r; } -bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, +bool parse_commands(environment & env, io_state & ios, char const * fname, optional const & base_dir, + bool use_exceptions, unsigned num_threads, definition_cache * cache, declaration_index * index, keep_theorem_mode tmode) { std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); - return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index, tmode); + return parse_commands(env, ios, in, fname, base_dir, use_exceptions, num_threads, cache, index, tmode); } void initialize_parser() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 2ef9933652..f6a099c73a 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -100,6 +100,7 @@ class parser { unsigned m_num_threads; scanner m_scanner; scanner::token_kind m_curr; + optional m_base_dir; local_level_decls m_local_level_decls; local_expr_decls m_local_decls; bool m_has_params; // true context context contains parameters @@ -270,7 +271,7 @@ class parser { public: parser(environment const & env, io_state const & ios, - std::istream & strm, char const * str_name, + std::istream & strm, char const * str_name, optional const & base_dir, bool use_exceptions = false, unsigned num_threads = 1, snapshot const * s = nullptr, snapshot_vector * sv = nullptr, info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); @@ -550,10 +551,11 @@ public: }; }; -bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, +bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, optional const & base_dir, bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); -bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads, +bool parse_commands(environment & env, io_state & ios, char const * fname, optional const & base, + bool use_exceptions, unsigned num_threads, definition_cache * cache = nullptr, declaration_index * index = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All); diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index e0bb983005..a8d2f03d70 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -161,9 +161,10 @@ unsigned server::file::copy_to(std::string & block, unsigned starting_from) { return num_lines; } -server::worker::worker(environment const & env, io_state const & ios, definition_cache & cache): +server::worker::worker(environment const & env, io_state const & ios, definition_cache & cache, optional const & base_dir): m_empty_snapshot(env, ios.get_options()), m_cache(cache), + m_base_dir(base_dir), m_todo_line_num(0), m_todo_options(ios.get_options()), m_terminate(false), @@ -223,8 +224,9 @@ server::worker::worker(environment const & env, io_state const & ios, definition tmp_ios.set_options(join(s.m_options, _ios.get_options())); bool use_exceptions = false; unsigned num_threads = 1; - parser p(s.m_env, tmp_ios, strm, todo_file->m_fname.c_str(), use_exceptions, num_threads, - &s, &todo_file->m_snapshots, &todo_file->m_info); + parser p(s.m_env, tmp_ios, strm, todo_file->m_fname.c_str(), m_base_dir, + use_exceptions, num_threads, + &s, &todo_file->m_snapshots, &todo_file->m_info); p.set_cache(&m_cache); p(); } catch (interrupted &) { @@ -282,10 +284,12 @@ void server::worker::set_todo(file_ptr const & f, unsigned line_num, options con m_todo_cv.notify_all(); } -server::server(environment const & env, io_state const & ios, unsigned num_threads): +server::server(environment const & env, io_state const & ios, optional const & base_dir, + unsigned num_threads): m_env(env), m_ios(ios), m_out(ios.get_regular_channel().get_stream()), + m_base_dir(base_dir), m_num_threads(num_threads), m_empty_snapshot(m_env, m_ios.get_options()), - m_worker(env, ios, m_cache) { + m_worker(env, ios, m_cache, m_base_dir) { #if !defined(LEAN_MULTI_THREAD) lean_unreachable(); #endif @@ -490,7 +494,7 @@ void server::set_option(std::string const & line) { std::istringstream strm(cmd); m_out << "-- BEGINSET" << std::endl; try { - parser p(m_env, m_ios, strm, "SET_command", true); + parser p(m_env, m_ios, strm, "SET_command", m_base_dir, true); p(); m_ios.set_options(p.ios().get_options()); } catch (exception & ex) { @@ -516,7 +520,7 @@ void server::eval_core(environment const & env, options const & o, std::string c io_state ios(m_ios, o); m_out << "-- BEGINEVAL" << std::endl; try { - parser p(env, ios, strm, "EVAL_command", true); + parser p(env, ios, strm, "EVAL_command", m_base_dir, true); p(); } catch (exception & ex) { m_out << ex.what() << std::endl; @@ -920,8 +924,8 @@ bool server::operator()(std::istream & in) { return true; } -bool parse_server_trace(environment const & env, io_state const & ios, char const * fname) { - lean::server Sv(env, ios); +bool parse_server_trace(environment const & env, io_state const & ios, char const * fname, optional const & base_dir) { + lean::server Sv(env, ios, base_dir); std::ifstream in(fname); if (in.bad() || in.fail()) throw exception(sstream() << "failed to open file '" << fname << "'"); diff --git a/src/frontends/lean/server.h b/src/frontends/lean/server.h index 9c0a192f4f..56c5fdc365 100644 --- a/src/frontends/lean/server.h +++ b/src/frontends/lean/server.h @@ -43,18 +43,20 @@ class server { typedef std::shared_ptr file_ptr; typedef std::unordered_map file_map; class worker { - snapshot m_empty_snapshot; - definition_cache & m_cache; - file_ptr m_todo_file; - unsigned m_todo_line_num; - options m_todo_options; - mutex m_todo_mutex; - condition_variable m_todo_cv; - file_ptr m_last_file; - atomic_bool m_terminate; - interruptible_thread m_thread; + snapshot m_empty_snapshot; + definition_cache & m_cache; + file_ptr m_todo_file; + optional m_base_dir; + unsigned m_todo_line_num; + options m_todo_options; + mutex m_todo_mutex; + condition_variable m_todo_cv; + file_ptr m_last_file; + atomic_bool m_terminate; + interruptible_thread m_thread; public: - worker(environment const & env, io_state const & ios, definition_cache & cache); + worker(environment const & env, io_state const & ios, definition_cache & cache, + optional const & base_dir); ~worker(); void set_todo(file_ptr const & f, unsigned line_num, options const & o); void request_interrupt(); @@ -66,6 +68,7 @@ class server { environment m_env; io_state m_ios; std::ostream & m_out; + optional m_base_dir; unsigned m_num_threads; snapshot m_empty_snapshot; definition_cache m_cache; @@ -101,12 +104,12 @@ class server { void find_goal_matches(unsigned line_num, unsigned col_num, std::string const & filters); public: - server(environment const & env, io_state const & ios, unsigned num_threads = 1); + server(environment const & env, io_state const & ios, optional const & base_dir, unsigned num_threads = 1); ~server(); bool operator()(std::istream & in); }; -bool parse_server_trace(environment const & env, io_state const & ios, char const * fname); +bool parse_server_trace(environment const & env, io_state const & ios, char const * fname, optional const & base_dir); void initialize_server(); void finalize_server(); diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 0d97ac0df3..2afe13dc55 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -61,6 +61,9 @@ add_test(NAME "show_goal_bag" add_test(NAME "print_info" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") +add_test(NAME "dir_option" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra" + COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" "--dir=${LEAN_SOURCE_DIR}/../library/data/nat" "dir_option.lean") if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) # The following test cannot be executed on Windows because of the # bash script timeout.sh diff --git a/src/shell/emscripten.cpp b/src/shell/emscripten.cpp index 504b3f4ee4..6d8c313a1a 100644 --- a/src/shell/emscripten.cpp +++ b/src/shell/emscripten.cpp @@ -54,7 +54,7 @@ public: try { environment temp_env(env); io_state temp_ios(ios); - if (!parse_commands(temp_env, temp_ios, input_filename.c_str(), false, num_threads)) { + if (!parse_commands(temp_env, temp_ios, input_filename.c_str(), optional(), false, num_threads)) { ok = false; } } catch (lean::exception & ex) { diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index d8949b8873..d1216d0ce7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -126,6 +126,7 @@ static void display_help(std::ostream & out) { std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif std::cout << " -D name=value set a configuration option (see set_option command)\n"; + std::cout << " --dir=directory display information about identifier or token in the given posivition\n"; std::cout << "Frontend query interface:\n"; std::cout << " --line=value line number for query\n"; std::cout << " --col=value column number for query\n"; @@ -186,10 +187,11 @@ static struct option g_long_options[] = { {"goal", no_argument, 0, 'G'}, {"hole", no_argument, 0, 'Z'}, {"info", no_argument, 0, 'I'}, + {"dir", required_argument, 0, 'T'}, {0, 0, 0, 0} }; -#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZAI" +#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZAIT:" #if defined(LEAN_TRACK_MEMORY) #define OPT_STR2 OPT_STR "M:012" @@ -267,6 +269,7 @@ int main(int argc, char ** argv) { optional column; optional export_txt; optional export_all_txt; + optional base_dir; bool show_goal = false; bool show_hole = false; bool show_info = false; @@ -381,6 +384,9 @@ int main(int argc, char ** argv) { case 'A': export_all_txt = std::string(optarg); break; + case 'T': + base_dir = std::string(optarg); + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -488,7 +494,7 @@ int main(int argc, char ** argv) { if (only_deps) { if (!display_deps(env, std::cout, std::cerr, argv[i])) ok = false; - } else if (!parse_commands(env, ios, argv[i], false, num_threads, + } else if (!parse_commands(env, ios, argv[i], base_dir, false, num_threads, cache_ptr, index_ptr, tmode)) { ok = false; } @@ -497,7 +503,7 @@ int main(int argc, char ** argv) { lean::system_import(argv[i]); break; case input_kind::Trace: - ok = lean::parse_server_trace(env, ios, argv[i]); + ok = lean::parse_server_trace(env, ios, argv[i], base_dir); break; default: lean_unreachable(); @@ -512,7 +518,7 @@ int main(int argc, char ** argv) { if (ok && server && (default_k == input_kind::Lean || default_k == input_kind::HLean)) { signal(SIGINT, on_ctrl_c); ios.set_option(lean::name("pp", "beta"), true); - lean::server Sv(env, ios, num_threads); + lean::server Sv(env, ios, base_dir, num_threads); if (!Sv(std::cin)) ok = false; } diff --git a/tests/lean/extra/dir_option.lean b/tests/lean/extra/dir_option.lean new file mode 100644 index 0000000000..36b26da3df --- /dev/null +++ b/tests/lean/extra/dir_option.lean @@ -0,0 +1,5 @@ +-- Test for --dir option, to be able to execute this file, we must provide --dir= in the command line +import .div +open nat + +check nat.div