feat(frontends/lean): add option --cache

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

src/frontends/lean/decl_cmds.cpp

@@ -269,21 +269,45 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));
         p.add_local_expr(n, ref);
     }
+    expr pre_type  = type;
+    expr pre_value = value;
     level_param_names new_ls;
-    if (is_theorem) {
+    bool found_cached = false;
-        if (p.num_threads() > 1) {
+    if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) {
-            // add as axiom, and create a task to prove the theorem
+        optional<certified_declaration> cd;
-            p.add_delayed_theorem(env, real_n, ls, type, value);
+        try {
-            std::tie(type, new_ls) = p.elaborate_type(type);
+            level_param_names c_ls; expr c_type, c_value;
-            env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
+            std::tie(c_ls, c_type, c_value) = *it;
+            if (is_theorem)
+                cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
+            else
+                cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque));
+            env = module::add(env, *cd);
+            found_cached = true;
+        } catch (exception&) {}
+    }
+
+    if (!found_cached) {
+        if (is_theorem) {
+            if (p.num_threads() > 1) {
+                // add as axiom, and create a task to prove the theorem
+                p.add_delayed_theorem(env, real_n, ls, type, value);
+                std::tie(type, new_ls) = p.elaborate_type(type);
+                env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type)));
+            } else {
+                std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
+                new_ls = append(ls, new_ls);
+                env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value)));
+                p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
+            }
         } else {
             std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
-            env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
+            new_ls = append(ls, new_ls);
+            env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, modifiers.m_is_opaque)));
+            p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
         }
-    } else {
-        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque);
-        env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
     }
+
     if (real_n != n)
         env = add_expr_alias_rec(env, n, real_n);
     if (modifiers.m_is_instance)

src/frontends/lean/parser.cpp

@@ -88,7 +88,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds),
     m_pos_table(std::make_shared<pos_info_table>()),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
-    m_snapshot_vector(sv), m_info_manager(im) {
+    m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr) {
     m_num_threads = num_threads;
     m_no_undef_id_error    = false;
     m_found_errors = false;
@@ -109,6 +109,19 @@ parser::~parser() {
     } catch (...) {}
 }
 
+void parser::cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
+                              level_param_names const & ls, expr const & type, expr const & value) {
+    if (m_cache)
+        m_cache->add(n, pre_type, pre_value, ls, type, value);
+}
+
+optional<std::tuple<level_param_names, expr, expr>> parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) {
+    if (m_cache)
+        return m_cache->find(n, pre_type, pre_value);
+    else
+        return optional<std::tuple<level_param_names, expr, expr>>();
+}
+
 expr parser::mk_sorry(pos_info const & p) {
     m_used_sorry = true;
     {
@@ -1252,18 +1265,20 @@ 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,
-                    unsigned num_threads) {
+                    unsigned num_threads, definitions_cache * cache) {
     parser p(env, ios, in, strm_name, use_exceptions, num_threads);
+    p.set_cache(cache);
     bool r = p();
     ios = p.ios();
     env = p.env();
     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, bool use_exceptions, unsigned num_threads,
+                    definitions_cache * cache) {
     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);
+    return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache);
 }
 }

src/frontends/lean/parser.h

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 #include "library/io_state_stream.h"
 #include "library/kernel_bindings.h"
+#include "library/definitions_cache.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/parser_config.h"
@@ -90,6 +91,9 @@ class parser {
     info_manager *          m_info_manager;
     std::vector<type_info_data> m_pre_info_data; // type information before elaboration
 
+    // cache support
+    definitions_cache *     m_cache;
+
     void display_warning_pos(unsigned line, unsigned pos);
     void display_warning_pos(pos_info p);
     void display_error_pos(unsigned line, unsigned pos);
@@ -167,6 +171,12 @@ public:
            snapshot_vector * sv = nullptr, info_manager * im = nullptr);
     ~parser();
 
+    void set_cache(definitions_cache * c) { m_cache = c; }
+    void cache_definition(name const & n, expr const & pre_type, expr const & pre_value,
+                          level_param_names const & ls, expr const & type, expr const & value);
+    /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */
+    optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
+
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }
     local_level_decls const & get_local_level_decls() const { return m_local_level_decls; }
@@ -309,6 +319,8 @@ public:
     bool operator()() { return parse_commands(); }
 };
 
-bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads);
+bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads,
-bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads);
+                    definitions_cache * cache = nullptr);
+bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
+                    definitions_cache * cache = nullptr);
 }

src/frontends/lean/theorem_queue.cpp

@@ -18,7 +18,10 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
             expr type, value;
             bool is_opaque = true; // theorems are always opaque
             std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
-            return check(env, mk_theorem(n, append(ls, new_ls), type, value));
+            new_ls = append(ls, new_ls);
+            auto r = check(env, mk_theorem(n, new_ls, type, value));
+            m_parser.cache_definition(n, t, v, new_ls, type, value);
+            return r;
         });
 }
 std::vector<certified_declaration> const & theorem_queue::join() { return m_queue.join(); }

src/library/definitions_cache.cpp

@@ -120,7 +120,8 @@ public:
 
 definitions_cache::definitions_cache() {}
 
-definitions_cache::definitions_cache(std::istream & in) {
+void definitions_cache::load(std::istream & in) {
+    lock_guard<mutex> lc(m_mutex);
     deserializer d(in);
     unsigned num;
     d >> num;
@@ -129,17 +130,28 @@ definitions_cache::definitions_cache(std::istream & in) {
         level_param_names ls;
         expr pre_type, pre_value, type, value;
         d >> n >> pre_type >> pre_value >> ls >> type >> value;
-        add(n, pre_type, pre_value, ls, type, value);
+        add_core(n, pre_type, pre_value, ls, type, value);
     }
 }
 
+void definitions_cache::add_core(name const & n, expr const & pre_type, expr const & pre_value,
+                                 level_param_names const & ls, expr const & type, expr const & value) {
+    m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value));
+}
+
 void definitions_cache::add(name const & n, expr const & pre_type, expr const & pre_value,
                             level_param_names const & ls, expr const & type, expr const & value) {
-    m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value));
+    lock_guard<mutex> lc(m_mutex);
+    add_core(n, pre_type, pre_value, ls, type, value);
 }
 
 optional<std::tuple<level_param_names, expr, expr>> definitions_cache::find(name const & n, expr const & pre_type, expr const & pre_value) {
-    if (auto it = m_definitions.find(n)) {
+    entry const * it;
+    {
+        lock_guard<mutex> lc(m_mutex);
+        it = m_definitions.find(n);
+    }
+    if (it) {
         level_param_names ls;
         expr c_pre_type, c_pre_value, type, value;
         std::tie(c_pre_type, c_pre_value, ls, type, value) = *it;
@@ -151,6 +163,7 @@ optional<std::tuple<level_param_names, expr, expr>> definitions_cache::find(name
 }
 
 void definitions_cache::save(std::ostream & out) {
+    lock_guard<mutex> lc(m_mutex);
     serializer s(out);
     s << m_definitions.size();
     m_definitions.for_each([&](name const & n, entry const & e) {

src/library/definitions_cache.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/thread.h"
 #include "util/name_map.h"
 #include "util/optional.h"
 #include "kernel/expr.h"
@@ -15,10 +16,12 @@ namespace lean {
 */
 class definitions_cache {
     typedef std::tuple<expr, expr, level_param_names, expr, expr> entry;
+    mutex           m_mutex;
     name_map<entry> m_definitions;
+    void add_core(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls,
+                  expr const & type, expr const & value);
 public:
     definitions_cache();
-    definitions_cache(std::istream & in);
     /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */
     void add(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value);
     /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value).
@@ -29,5 +32,7 @@ public:
     optional<std::tuple<level_param_names, expr, expr>> find(name const & n, expr const & pre_type, expr const & pre_value);
     /** \brief Store the cache content into the given stream */
     void save(std::ostream & out);
+    /** \brief Load the cache content from the given stream */
+    void load(std::istream & in);
 };
 }

src/shell/lean.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/hott_kernel.h"
 #include "library/module.h"
 #include "library/io_state_stream.h"
+#include "library/definitions_cache.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
@@ -43,6 +44,7 @@ using lean::mk_environment;
 using lean::mk_hott_environment;
 using lean::set_environment;
 using lean::set_io_state;
+using lean::definitions_cache;
 
 enum class input_kind { Unspecified, Lean, Lua };
 
@@ -76,6 +78,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --threads=num -j  number of threads used to process lean files\n";
     std::cout << "  --deps            just print dependencies of a Lean input\n";
     std::cout << "  --flycheck        print structured error message for flycheck\n";
+    std::cout << "  --cache=file -c   load/save cached definitions from/to the given file\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -109,6 +112,7 @@ static struct option g_long_options[] = {
     {"quiet",       no_argument,       0, 'q'},
     {"hott",        no_argument,       0, 'H'},
     {"threads",     required_argument, 0, 'j'},
+    {"cache",       required_argument, 0, 'c'},
     {"deps",        no_argument,       0, 'D'},
     {"flycheck",    no_argument,       0, 'F'},
 #if defined(LEAN_USE_BOOST)
@@ -118,9 +122,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "FDHSqlupgvhj:012k:012s:012t:012o:";
+static char const * g_opt_str = "FDHSqlupgvhj:012k:012s:012t:012o:c:";
 #else
-static char const * g_opt_str = "FDHSqlupgvhj:012k:012t:012o:";
+static char const * g_opt_str = "FDHSqlupgvhj:012k:012t:012o:c:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -136,7 +140,9 @@ int main(int argc, char ** argv) {
     bool flycheck        = false;
     lean_mode mode       = lean_mode::Standard;
     unsigned num_threads = 1;
+    bool use_cache       = false;
     std::string output;
+    std::string cache_name;
     input_kind default_k = input_kind::Lean; // default
     while (true) {
         int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
@@ -178,9 +184,13 @@ int main(int argc, char ** argv) {
             lean::set_thread_stack_size(atoi(optarg)*1024);
             break;
         case 'o':
-            output = optarg;
+            output         = optarg;
             export_objects = true;
             break;
+        case 'c':
+            cache_name = optarg;
+            use_cache  = true;
+            break;
         case 't':
             trust_lvl = atoi(optarg);
             break;
@@ -209,6 +219,14 @@ int main(int argc, char ** argv) {
     script_state S = lean::get_thread_script_state();
     set_environment set1(S, env);
     set_io_state    set2(S, ios);
+    definitions_cache   cache;
+    definitions_cache * cache_ptr = nullptr;
+    if (use_cache) {
+        cache_ptr = &cache;
+        std::ifstream in(cache_name);
+        if (!in.bad() && !in.fail())
+            cache.load(in);
+    }
 
     try {
         bool ok = true;
@@ -225,7 +243,7 @@ int main(int argc, char ** argv) {
             if (k == input_kind::Lean) {
                 if (only_deps) {
                     display_deps(env, std::cout, argv[i]);
-                } else if (!parse_commands(env, ios, argv[i], false, num_threads)) {
+                } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) {
                     ok = false;
                 }
             } else if (k == input_kind::Lua) {
@@ -245,6 +263,10 @@ int main(int argc, char ** argv) {
             if (!Sv(std::cin))
                 ok = false;
         }
+        if (use_cache) {
+            std::ofstream out(cache_name, std::ofstream::binary);
+            cache.save(out);
+        }
         if (export_objects && ok) {
             std::ofstream out(output, std::ofstream::binary);
             export_module(out, env);