feat(frontends/lean): add 'import' command, add command line option for setting number of threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/interactive.cpp

@@ -12,9 +12,9 @@ Author: Leonardo de Moura
 #include "frontends/lean/interactive.h"
 
 namespace lean {
-interactive::interactive(environment const & env, io_state const & ios, script_state const & ss,
+interactive::interactive(environment const & env, io_state const & ios, script_state const & ss, unsigned num_threads,
                          char const * ack_cmd, char const * snapshot_cmd, char const * restore_cmd, char const * restart_cmd):
-    m_env(env), m_ios(ios), m_ss(ss), m_line(1),
+    m_env(env), m_ios(ios), m_ss(ss), m_num_threads(num_threads), m_line(1),
     m_ack_cmd(ack_cmd), m_snapshot_cmd(snapshot_cmd), m_restore_cmd(restore_cmd), m_restart_cmd(restart_cmd) {
     save_snapshot();
 }
@@ -22,7 +22,7 @@ interactive::interactive(environment const & env, io_state const & ios, script_s
 void interactive::parse_block(std::string const & str, char const * strm_name) {
     if (str.size() > 0) {
         std::istringstream block(str);
-        parser p(m_env, m_ios, block, strm_name, &m_ss, false, m_lds, m_eds, m_line);
+        parser p(m_env, m_ios, block, strm_name, &m_ss, false, m_num_threads, m_lds, m_eds, m_line);
         p();
         m_env  = p.env();
         m_ios  = p.ios();

src/frontends/lean/interactive.h

@@ -35,6 +35,7 @@ class interactive {
     environment               m_env;
     io_state                  m_ios;
     script_state              m_ss;
+    unsigned                  m_num_threads;
     local_level_decls         m_lds;
     local_expr_decls          m_eds;
     unsigned                  m_line;
@@ -47,6 +48,7 @@ class interactive {
     void restore(unsigned new_line, std::string & block);
 public:
     interactive(environment const & env, io_state const & ios, script_state const & ss,
+                unsigned num_threads = 1,
                 char const * ack_cmd = "#ACK", char const * snapshot_cmd = "#SNAPSHOT",
                 char const * res_cmd = "#RESTORE", char const * restart_cmd = "#RESTART");
     environment const & env() const { return m_env; }

src/frontends/lean/parser.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/script_exception.h"
 #include "util/sstream.h"
 #include "util/flet.h"
+#include "util/lean_path.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "kernel/abstract.h"
@@ -21,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/choice.h"
 #include "library/placeholder.h"
 #include "library/deep_copy.h"
+#include "library/module.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/notation_cmd.h"
@@ -58,7 +60,7 @@ parser::param_universe_scope::~param_universe_scope() {
 
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
-               script_state * ss, bool use_exceptions,
+               script_state * ss, bool use_exceptions, unsigned num_threads,
                local_level_decls const & lds, local_expr_decls const & eds,
                unsigned line):
     m_env(env), m_ios(ios), m_ss(ss),
@@ -66,6 +68,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds),
     m_pos_table(std::make_shared<pos_info_table>()) {
     m_scanner.set_line(line);
+    m_num_threads = num_threads;
     m_type_use_placeholder = true;
     m_found_errors = false;
     updt_options();
@@ -340,7 +343,8 @@ static name g_infix("infix");
 static name g_infixl("infixl");
 static name g_infixr("infixr");
 static name g_postfix("postfix");
-static name g_notation("postfix");
+static name g_notation("notation");
+static name g_import("import");
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
 
@@ -890,11 +894,49 @@ void parser::parse_script(bool as_expr) {
         });
 }
 
+static optional<std::string> find_file(name const & f, char const * ext) {
+    try {
+        return optional<std::string>(find_file(f, {ext}));
+    } catch (...) {
+        return optional<std::string>();
+    }
+}
+
+void parser::parse_imports() {
+    buffer<std::string> olean_files;
+    buffer<std::string> lua_files;
+    while (curr_is_token(g_import)) {
+        m_last_cmd_pos = pos();
+        next();
+        while (curr_is_identifier()) {
+            name f            = get_name_val();
+            if (auto it = find_file(f, ".lua")) {
+                if (!m_ss)
+                    throw parser_error("invalid import, Lua interpreter is not available", pos());
+                lua_files.push_back(*it);
+            } else if (auto it = find_file(f, ".olean")) {
+                olean_files.push_back(*it);
+            } else {
+                throw parser_error(sstream() << "invalid import, unknow module '" << f << "'", pos());
+            }
+            next();
+        }
+    }
+    m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios);
+    using_script([&](lua_State *) {
+            m_ss->exec_unprotected([&]() {
+                    for (auto const & f : lua_files) {
+                        m_ss->import_explicit(f.c_str());
+                    }});
+        });
+}
+
 bool parser::parse_commands() {
     // We disable hash-consing while parsing to make sure the pos-info are correct.
     scoped_expr_caching disable(false);
     try {
         bool done = false;
+        parse_imports();
         while (!done) {
             protected_call([&]() {
                     check_interrupted();
@@ -924,18 +966,19 @@ bool parser::parse_commands() {
 }
 
 
-bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions) {
+bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions,
-    parser p(env, ios, in, strm_name, S, use_exceptions);
+                    unsigned num_threads) {
+    parser p(env, ios, in, strm_name, S, use_exceptions, num_threads);
     bool r = p();
     ios = p.ios();
     env = p.env();
     return r;
 }
 
-bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions) {
+bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions, unsigned num_threads) {
     std::ifstream in(fname);
     if (in.bad() || in.fail())
         throw exception(sstream() << "failed to open file '" << fname << "'");
-    return parse_commands(env, ios, in, fname, S, use_exceptions);
+    return parse_commands(env, ios, in, fname, S, use_exceptions, num_threads);
 }
 }

src/frontends/lean/parser.h

@@ -53,6 +53,7 @@ class parser {
     bool                    m_verbose;
     bool                    m_use_exceptions;
     bool                    m_show_errors;
+    unsigned                m_num_threads;
 
     scanner                 m_scanner;
     scanner::token_kind     m_curr;
@@ -105,6 +106,7 @@ class parser {
     level parse_level_nud();
     level parse_level_led(level left);
 
+    void parse_imports();
     void parse_command();
     void parse_script(bool as_expr = false);
     bool parse_commands();
@@ -133,6 +135,7 @@ public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,
            script_state * ss = nullptr, bool use_exceptions = false,
+           unsigned num_threads = 1,
            local_level_decls const & lds = local_level_decls(),
            local_expr_decls const & eds = local_expr_decls(),
            unsigned line = 1);
@@ -246,7 +249,7 @@ public:
 };
 
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
-                    script_state * S, bool use_exceptions);
+                    script_state * S, bool use_exceptions, unsigned num_threads);
 bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S,
-                    bool use_exceptions);
+                    bool use_exceptions, unsigned num_threads);
 }

src/shell/lean.cpp

@@ -68,6 +68,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --quiet -q        do not print verbose messages\n";
     std::cout << "  --interactive -i  read blocks of commands from the input stream\n";
     std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
+    std::cout << "  --threads=num -r  number of threads used to process lean files\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -100,6 +101,7 @@ static struct option g_long_options[] = {
     {"interactive", no_argument,       0, 'i'},
     {"quiet",       no_argument,       0, 'q'},
     {"hott",        no_argument,       0, 'H'},
+    {"threads",     required_argument, 0, 'r'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",      required_argument, 0, 's'},
 #endif
@@ -107,9 +109,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "Hiqlupgvhc:012s:012t:012o:";
+static char const * g_opt_str = "Hiqlupgvhr:012c:012s:012t:012o:";
 #else
-static char const * g_opt_str = "Hiqlupgvhc:012t:012o:";
+static char const * g_opt_str = "Hiqlupgvhr:012c:012t:012o:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -122,6 +124,7 @@ int main(int argc, char ** argv) {
     bool quiet           = false;
     bool interactive     = false;
     lean_mode mode       = lean_mode::Standard;
+    unsigned num_threads = 1;
     std::string output;
     input_kind default_k = input_kind::Lean; // default
     while (true) {
@@ -129,6 +132,9 @@ int main(int argc, char ** argv) {
         if (c == -1)
             break; // end of command line
         switch (c) {
+        case 'r':
+            num_threads = atoi(optarg);
+            break;
         case 'H':
             mode = lean_mode::HoTT;
             lean::init_lean_path("hott");
@@ -201,7 +207,7 @@ int main(int argc, char ** argv) {
                 }
             }
             if (k == input_kind::Lean) {
-                if (!parse_commands(env, ios, argv[i], &S, false))
+                if (!parse_commands(env, ios, argv[i], &S, false, num_threads))
                     ok = false;
             } else if (k == input_kind::Lua) {
                 try {
@@ -216,7 +222,7 @@ int main(int argc, char ** argv) {
         }
         if (ok && interactive && default_k == input_kind::Lean) {
             signal(SIGINT, on_ctrl_c);
-            lean::interactive in(env, ios, S);
+            lean::interactive in(env, ios, S, num_threads);
             in(std::cin, "[stdin]");
         }
         if (export_objects) {

src/util/lean_path.cpp

@@ -218,6 +218,14 @@ std::string find_file(std::string fname) {
     return find_file(fname, {".olean", ".lean", ".lua"});
 }
 
+std::string find_file(name const & fname) {
+    return find_file(fname.to_string(g_sep_str.c_str()));
+}
+
+std::string find_file(name const & fname, std::initializer_list<char const *> const & exts) {
+    return find_file(fname.to_string(g_sep_str.c_str()), exts);
+}
+
 char const * get_lean_path() {
     return g_lean_path.c_str();
 }

src/util/lean_path.h

@@ -17,9 +17,11 @@ char const * get_lean_path();
    exception if the file was not found.
 */
 std::string find_file(std::string fname);
-
 std::string find_file(std::string fname, std::initializer_list<char const *> const & exts);
 
+/** \brief Hierarchical names are converted into paths using the path separator. Example: foo.bar is converted into foo/bar */
+std::string find_file(name const & fname);
+std::string find_file(name const & fname, std::initializer_list<char const *> const & exts);
 
 /** \brief Return true iff fname ends with ".lean" */
 bool is_lean_file(std::string const & fname);

src/util/script_state.cpp

@@ -128,7 +128,7 @@ struct script_state::imp {
     }
 
     bool import(char const * fname) {
-        return import_explicit(find_file(fname));
+        return import_explicit(find_file(std::string(fname)));
     }
 };