feat(shell,frontends/lean): add command line option --dir

See #821
See #788

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 <string>
 #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<std::string>(), 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<std::string>(), 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<std::string>(), use_exceptions, num_threads);
     expr e = p.parse_expr();
     expr _e; level_param_names _ps;
     std::tie(_e, _ps) = p.elaborate(e, list<expr>());

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<std::string> 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<module_name> olean_files;
     buffer<name>        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<std::string> 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<std::string> 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() {

src/frontends/lean/parser.h

@@ -100,6 +100,7 @@ class parser {
     unsigned                m_num_threads;
     scanner                 m_scanner;
     scanner::token_kind     m_curr;
+    optional<std::string>   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<std::string> 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<std::string> 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<std::string> const & base,
+                    bool use_exceptions, unsigned num_threads,
                     definition_cache * cache = nullptr, declaration_index * index = nullptr,
                     keep_theorem_mode tmode = keep_theorem_mode::All);
 

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<std::string> 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,7 +224,8 @@ 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,
+                    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();
@@ -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<std::string> 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) {
+bool parse_server_trace(environment const & env, io_state const & ios, char const * fname, optional<std::string> const & base_dir) {
-    lean::server Sv(env, ios);
+    lean::server Sv(env, ios, base_dir);
     std::ifstream in(fname);
     if (in.bad() || in.fail())
         throw exception(sstream() << "failed to open file '" << fname << "'");

src/frontends/lean/server.h

@@ -46,6 +46,7 @@ class server {
         snapshot              m_empty_snapshot;
         definition_cache &    m_cache;
         file_ptr              m_todo_file;
+        optional<std::string> m_base_dir;
         unsigned              m_todo_line_num;
         options               m_todo_options;
         mutex                 m_todo_mutex;
@@ -54,7 +55,8 @@ class server {
         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<std::string> 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<std::string>     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<std::string> 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<std::string> const & base_dir);
 
 void initialize_server();
 void finalize_server();

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

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<std::string>(), false, num_threads)) {
                 ok = false;
             }
         } catch (lean::exception & ex) {

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<unsigned> column;
     optional<std::string> export_txt;
     optional<std::string> export_all_txt;
+    optional<std::string> 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;
         }

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=<path-to-nat-lib> in the command line
+import .div
+open nat
+
+check nat.div