feat(frontends/lean): process theorems in parallel

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

src/frontends/lean/decl_cmds.cpp

@@ -291,9 +291,23 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         env = add_decl_alias(env, n, mk_constant(real_n));
     level_param_names new_ls;
     if (is_theorem) {
-        // TODO(Leo): delay theorems
+        if (p.num_threads() > 1) {
-        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+            // add as axiom, and create a task to prove the theorem
-        env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
+            expr saved_type       = type;
+            expr saved_value      = value;
+            environment saved_env = env;
+            std::tie(type, new_ls) = p.elaborate_type(type);
+            env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
+            p.add_delayed_theorem([=, &p]() {
+                    level_param_names new_ls;
+                    expr type, value;
+                    std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, n, saved_type, saved_value);
+                    return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value));
+                });
+        } else {
+            std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
+            env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
+        }
     } else {
         std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
         env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));

src/frontends/lean/parser.cpp

@@ -75,7 +75,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds),
-    m_pos_table(std::make_shared<pos_info_table>()) {
+    m_pos_table(std::make_shared<pos_info_table>()), m_theorem_queue(num_threads > 1 ? num_threads - 1 : 0) {
     m_scanner.set_line(line);
     m_num_threads = num_threads;
     m_no_undef_id_error    = false;
@@ -87,6 +87,15 @@ parser::parser(environment const & env, io_state const & ios,
                    [&]() { sync_command(); });
 }
 
+parser::~parser() {
+    try {
+        if (!m_theorem_queue.done()) {
+            m_theorem_queue.interrupt();
+            m_theorem_queue.join();
+        }
+    } catch (...) {}
+}
+
 bool parser::has_tactic_decls() {
     if (!m_has_tactic_decls)
         m_has_tactic_decls = ::lean::has_tactic_decls(m_env);
@@ -484,6 +493,12 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name cons
     return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
 }
 
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(environment const & env, name const & n, expr const & t,
+                                                                          expr const & v) {
+    parser_pos_provider pp = get_pos_provider();
+    return ::lean::elaborate(env, m_local_level_decls, m_ios, n, t, v, &pp);
+}
+
 [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {
     throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos);
 }
@@ -1035,6 +1050,9 @@ bool parser::parse_commands() {
                 [&]() { sync_command(); });
         }
     } catch (interrupt_parser) {}
+    for (certified_declaration const & thm : m_theorem_queue.join()) {
+        m_env.replace(thm);
+    }
     return !m_found_errors;
 }
 

src/frontends/lean/parser.h

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/thread_script_state.h"
 #include "util/script_exception.h"
+#include "util/worker_queue.h"
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
@@ -63,6 +64,8 @@ class parser {
     optional<bool>          m_has_num;
     optional<bool>          m_has_string;
     optional<bool>          m_has_tactic_decls;
+    // We process theorems in parallel
+    worker_queue<certified_declaration> m_theorem_queue;
 
     void display_error_pos(unsigned line, unsigned pos);
     void display_error_pos(pos_info p);
@@ -130,6 +133,7 @@ public:
            local_level_decls const & lds = local_level_decls(),
            local_expr_decls const & eds = local_expr_decls(),
            unsigned line = 1);
+    ~parser();
 
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }
@@ -157,6 +161,9 @@ public:
     expr mk_app(expr fn, expr arg, pos_info const & p);
     expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
 
+    unsigned num_threads() const { return m_num_threads; }
+    void add_delayed_theorem(std::function<certified_declaration()> const & fn) { m_theorem_queue.add(fn); }
+
     /** \brief Read the next token. */
     void scan() { m_curr = m_scanner.scan(m_env); }
     /** \brief Return the current token */
@@ -260,6 +267,8 @@ public:
     std::tuple<expr, level_param_names> elaborate(expr const & e) { return elaborate_at(m_env, e); }
     /** \brief Elaborate the definition n : t := v */
     std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
+    /** \brief Elaborate the definition n : t := v in the given environment*/
+    std::tuple<expr, expr, level_param_names> elaborate_definition_at(environment const & env, name const & n, expr const & t, expr const & v);
 
     parser_pos_provider get_pos_provider() const { return parser_pos_provider(m_pos_table, get_stream_name(), m_last_cmd_pos); }
 

src/util/worker_queue.h

@@ -115,5 +115,7 @@ public:
         for (auto & t : m_threads)
             t->request_interrupt();
     }
+
+    bool done() const { return m_done; }
 };
 }