From 0bb155a427474d376e451fd8d551db80d756e084 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Oct 2016 19:55:47 -0700 Subject: [PATCH] chore(*): remove .clean support In Lean2, we used to cache elaborated definitions in .clean files. The main goal was to optimize each flycheck invocation produced by Emacs. The Lean3 definition package was not updating this cache. Moreover, it is not necessary because the new compilation server subsumes it. --- bin/linja.in | 64 +------ src/frontends/lean/builtin_cmds.cpp | 7 - src/frontends/lean/parser.cpp | 24 +-- src/frontends/lean/parser.h | 17 +- src/frontends/lean/token_table.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/definition_cache.cpp | 256 ---------------------------- src/library/definition_cache.h | 60 ------- src/shell/lean.cpp | 41 +---- 9 files changed, 18 insertions(+), 455 deletions(-) delete mode 100644 src/library/definition_cache.cpp delete mode 100644 src/library/definition_cache.h diff --git a/bin/linja.in b/bin/linja.in index 2f77a4c240..191f0f5bba 100755 --- a/bin/linja.in +++ b/bin/linja.in @@ -103,7 +103,7 @@ if platform.system().startswith("MSYS"): else: g_linja_path = os.path.abspath(os.path.realpath(__file__)) g_lean_bin_dir = os.path.dirname(g_linja_path) -g_phony_targets = ["all", "clean", "clear-cache"] +g_phony_targets = ["all"] g_project_filename = ".project" g_lean_path = "USE DEFAULT" # System will search automatically g_ninja_path = "USE DEFAULT" # System will search automatically @@ -292,16 +292,6 @@ def process_args(args): args.project_dir = find_file_upward(g_project_filename) if args.project_dir: os.chdir(args.project_dir) - if args.cache: - args.cache = process_target(args.cache) - if len(args.targets) != 1: - error("--cache option can only be used with one target") - if not args.cache.endswith(".lean") and not args.cache.endswith(".hlean"): - error("cache argument has to end with .lean or .hlean") - if args.cache.endswith(".lean"): - args.cache = args.cache[:-4] + "clean" - else: - args.cache = args.cache[:-5] + "clean" args.phony_targets = list(set(g_phony_targets) & set(args.targets)) if args.verbose: g_logger.setLevel(logging.INFO) @@ -317,8 +307,6 @@ def get_lean_options(args): args.lean_options += ["-t", args.trust] if args.to_axiom: args.lean_options.append("--to_axiom") - if args.cache: - args.lean_options += ["-c", '%s' % args.cache] if args.lean_config_option: for item in args.lean_config_option: args.lean_options.append("-D" + item) @@ -326,7 +314,6 @@ def get_lean_options(args): def parse_arg(argv): parser = argparse.ArgumentParser(description='linja: ninja build wrapper for Lean theorem prover.') - parser.add_argument('--cache', action='store', help="Use specified cache (clean) file.") parser.add_argument('--directory', '-C', action='store', help="change to DIR before doing anything else.") parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)") parser.add_argument('--verbose', '-v', action='store_true', help="turn on verbose option") @@ -388,14 +375,12 @@ def get_lean_names(lean_file, args, using_hlean): basename, ext = os.path.splitext(lean_file) basename = normalize_drive_name(basename) item = {"base" : basename} - lean_name_exts = ["lean", "olean", "clean", "d"] + lean_name_exts = ["lean", "olean", "d"] for ext in lean_name_exts: if ext == "lean" and using_hlean: item[ext] = basename + ".hlean" else: item[ext] = basename + "." + ext - if args.cache and len(args.targets) == 1 and item['lean'] == args.targets[0]: - item['clean'] = args.cache return item def recursive_glob(directory): @@ -462,49 +447,23 @@ def find_lean_files(args): # Initialize static variable find_lean_files.cached_list = [] -def clear_cache(args): - files = find_lean_files(args) - files = find_lean_files(args) - files = find_lean_files(args) - files = find_lean_files(args) - num_of_files = len(files) - i = 0 - for item in files: - i += 1 - clean_file = item['clean'] - if os.path.isfile(clean_file): - sys.stderr.write("[%i/%i] clear cache... % -80s\r" % (i, num_of_files, clean_file)) - sys.stderr.flush() - os.remove(clean_file) - if num_of_files > 0: - sys.stderr.write("\n") - -def build_olean(lean, olean, clean, dlean, base): - (lean, olean, clean, dlean, base) = list(map(escape_ninja_char, (lean, olean, clean, dlean, base))) - if clean.startswith(base): - str = """build %s %s: LEAN %s | %s""" % (olean, clean, lean, dlean) - else: - str = """build %s: LEAN %s | %s""" % (olean, lean, dlean) +def build_olean(lean, olean, dlean, base): + (lean, olean, dlean, base) = list(map(escape_ninja_char, (lean, olean, dlean, base))) + str = """build %s: LEAN %s | %s""" % (olean, lean, dlean) if g_lean_bin_dep_flag: str += " %s" % escape_ninja_char(normalize_drive_name(g_lean_path)) str += "\n" str += " DLEAN_FILE=%s\n" % dlean str += " OLEAN_FILE=%s\n" % olean - str += " CLEAN_FILE=%s\n" % clean return str def make_build_ninja(args): with open(os.path.join(args.project_dir, "build.ninja"), "w") as f: lean_files = find_lean_files(args) - print("""rule CLEAN""", file=f) - print(""" command = """, end=' ', file=f) - print(""""%s" -t clean""" % g_ninja_path, file=f) - print(""" description = Cleaning all built files...""", file=f) - print("""rule LEAN""", file=f) print(""" depfile = ${DLEAN_FILE}""", file=f) - print(""" command = "%s" %s $in -o "${OLEAN_FILE}" -c "${CLEAN_FILE}" """ \ + print(""" command = "%s" %s $in -o "${OLEAN_FILE}" """ \ % (g_lean_path, " ".join(args.lean_options)), file=f) print("build all: phony", end=' ', file=f) @@ -512,10 +471,8 @@ def make_build_ninja(args): print(" " + escape_ninja_char(item['olean']), end=' ', file=f) print("", file=f) - print("""build clean: CLEAN""", file=f) - for item in lean_files: - print(build_olean(item['lean'], item['olean'], item['clean'], item['d'], item['base']), file=f) + print(build_olean(item['lean'], item['olean'], item['d'], item['base']), file=f) print("""default all""", file=f) @@ -563,12 +520,7 @@ def main(argv=None): argv = sys.argv[1:] args = parse_arg(argv) if args.project_dir: - if args.targets == ["clear-cache"]: - args.targets = [] - clear_cache(args) - return 0 - if not "clean" in args.targets: - make_deps_all_files(args) + make_deps_all_files(args) make_build_ninja(args) return call_ninja(args) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 85266df7a3..2e8290af73 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -309,12 +309,6 @@ environment open_export_cmd(parser & p, bool open) { static environment open_cmd(parser & p) { return open_export_cmd(p, true); } static environment export_cmd(parser & p) { return open_export_cmd(p, false); } -static environment erase_cache_cmd(parser & p) { - name n = p.check_id_next("invalid #erase_cache command, identifier expected"); - p.erase_cached_definition(n); - return p.env(); -} - static environment local_cmd(parser & p) { if (p.curr_is_token_or_id(get_attribute_tk())) { p.next(); @@ -541,7 +535,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("declare_trace", "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd)); add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd)); add_cmd(r, cmd_info("run_command", "execute an user defined command at top-level", run_command_cmd)); - add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); add_cmd(r, cmd_info("#unify", "(for debugging purposes)", unify_cmd)); add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd)); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0cb2783411..283f38ca93 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -186,7 +186,7 @@ parser::parser(environment const & env, io_state const & ios, m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name, s ? s->m_pos : pos_info(1, 0)), m_base_dir(base_dir), m_imports_parsed(false), - m_snapshot_vector(sv), m_cache(nullptr) { + m_snapshot_vector(sv) { if (s) { m_env = s->m_env; m_ios.set_options(s->m_options); @@ -267,20 +267,6 @@ void parser::scan() { } } -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, bool is_trusted) { - if (m_cache) - m_cache->add(m_env, n, pre_type, pre_value, ls, type, value, is_trusted); -} - -auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted) --> optional> { - if (m_cache) - return m_cache->find(m_env, n, pre_type, pre_value, is_trusted); - else - return optional>(); -} - bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const { if (m_stop_at) { if (start_line <= m_stop_at_line && m_stop_at_line <= end_line) @@ -2291,9 +2277,8 @@ message_builder parser::mk_message(message_severity severity) { 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) { + unsigned num_threads) { parser p(env, ios, in, strm_name, base_dir, use_exceptions, num_threads, nullptr, nullptr); - p.set_cache(cache); bool r = p(); ios = p.ios(); env = p.env(); @@ -2301,12 +2286,11 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c } bool parse_commands(environment & env, io_state & ios, char const * fname, optional const & base_dir, - bool use_exceptions, unsigned num_threads, - definition_cache * cache) { + 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, base_dir, use_exceptions, num_threads, cache); + return parse_commands(env, ios, in, fname, base_dir, use_exceptions, num_threads); } void initialize_parser() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 08bd096594..4397323791 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "library/io_state.h" #include "library/io_state_stream.h" #include "library/message_builder.h" -#include "library/definition_cache.h" #include "frontends/lean/scanner.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/local_level_decls.h" @@ -116,9 +115,6 @@ class parser : public abstract_parser { // info support snapshot_vector * m_snapshot_vector; - // cache support - definition_cache * m_cache; - // curr command token name m_cmd_token; @@ -227,14 +223,6 @@ public: cmd_table const & cmds() const { return get_cmd_table(env()); } - void set_cache(definition_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, bool is_trusted); - /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ - optional> - find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted); - void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); } - bool are_info_lines_valid(unsigned start_line, unsigned end_line) const; environment const & env() const { return m_env; } @@ -504,10 +492,9 @@ public: 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); + 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); + bool use_exceptions, unsigned num_threads); void initialize_parser(); void finalize_parser(); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 2b0675fdc6..2a4596e3c3 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -108,7 +108,7 @@ void init_token_table(token_table & t) { "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "open", "export", "override", "@[", "attribute", "persistent", "instance", "include", "omit", "init_quotient", - "init_hits", "declare_trace", "run_command", "add_key_equivalence", "#erase_cache", + "init_hits", "declare_trace", "run_command", "add_key_equivalence", "#compile", "#unify", nullptr}; pair aliases[] = diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 81e52d37bd..1550639417 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -3,7 +3,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp max_sharing.cpp shared_environment.cpp module.cpp private.cpp placeholder.cpp aliases.cpp update_declaration.cpp scoped_ext.cpp standard_kernel.cpp sorry.cpp replace_visitor.cpp - explicit.cpp num.cpp string.cpp head_map.cpp definition_cache.cpp + explicit.cpp num.cpp string.cpp head_map.cpp class.cpp util.cpp print.cpp annotation.cpp quote.cpp typed_expr.cpp protected.cpp reducible.cpp init_module.cpp exception.cpp fingerprint.cpp flycheck.cpp pp_options.cpp diff --git a/src/library/definition_cache.cpp b/src/library/definition_cache.cpp deleted file mode 100644 index 994fb41fbd..0000000000 --- a/src/library/definition_cache.cpp +++ /dev/null @@ -1,256 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/interrupt.h" -#include "kernel/for_each_fn.h" -#include "library/placeholder.h" -#include "library/kernel_serializer.h" -#include "library/definition_cache.h" -#include "library/fingerprint.h" - -namespace lean { -/** \brief Similar to expr_eq_fn, but allows different placeholders - with different names. We cannot use the hashcode to speedup comparasion. -*/ -class expr_eq_modulo_placeholders_fn { - name_map m_map; // for comparing placeholder names - - bool compare(name const & a, name const & b, bool placeholders) { - if (!placeholders) { - return a == b; - } else if (auto it = m_map.find(a)) { - return *it == b; - } else { - m_map.insert(a, b); - return true; - } - } - - bool compare(level const & l1, level const & l2) { - if (kind(l1) != kind(l2)) return false; - if (is_eqp(l1, l2)) return true; - bool placeholders = is_placeholder(l1) && is_placeholder(l2); - switch (kind(l1)) { - case level_kind::Zero: - return true; - case level_kind::Param: - return compare(param_id(l1), param_id(l2), placeholders); - case level_kind::Global: - return compare(global_id(l1), global_id(l2), placeholders); - case level_kind::Meta: - return compare(meta_id(l1), meta_id(l2), placeholders); - case level_kind::Max: - if (get_depth(l1) != get_depth(l2)) - return false; - return - compare(max_lhs(l1), max_lhs(l2)) && - compare(max_rhs(l1), max_rhs(l2)); - case level_kind::IMax: - if (get_depth(l1) != get_depth(l2)) - return false; - return - compare(imax_lhs(l1), imax_lhs(l2)) && - compare(imax_rhs(l1), imax_rhs(l2)); - case level_kind::Succ: - if (get_depth(l1) != get_depth(l2)) - return false; - return - is_explicit(l1) == is_explicit(l2) && - (is_explicit(l1) || compare(succ_of(l1), succ_of(l2))); - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - bool compare(levels const & ls1, levels const & ls2) { - return ::lean::compare(ls1, ls2, - [&](level const & l1, level const & l2) { return compare(l1, l2); }); - } - - bool compare(expr const & a, expr const & b) { - if (is_eqp(a, b)) return true; - if (a.kind() != b.kind()) return false; - if (get_weight(a) != get_weight(b)) return false; - check_system("expression equality modulo placeholder test"); - bool placeholders = is_placeholder(a) && is_placeholder(b); - switch (a.kind()) { - case expr_kind::Var: - return var_idx(a) == var_idx(b); - case expr_kind::Constant: - return - compare(const_name(a), const_name(b), placeholders) && - compare(const_levels(a), const_levels(b)); - case expr_kind::Meta: - return - compare(mlocal_name(a), mlocal_name(b), placeholders) && - compare(mlocal_type(a), mlocal_type(b)); - case expr_kind::Local: - return - compare(mlocal_name(a), mlocal_name(b), placeholders) && - compare(mlocal_type(a), mlocal_type(b)) && - local_pp_name(a) == local_pp_name(b) && - local_info(a) == local_info(b); - case expr_kind::App: - return - compare(app_fn(a), app_fn(b)) && - compare(app_arg(a), app_arg(b)); - case expr_kind::Lambda: case expr_kind::Pi: - return - compare(binding_domain(a), binding_domain(b)) && - compare(binding_body(a), binding_body(b)) && - binding_info(a) == binding_info(b); - case expr_kind::Let: - return - compare(let_type(a), let_type(b)) && - compare(let_value(a), let_value(b)) && - compare(let_body(a), let_body(b)); - case expr_kind::Sort: - return compare(sort_level(a), sort_level(b)); - case expr_kind::Macro: - if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b)) - return false; - for (unsigned i = 0; i < macro_num_args(a); i++) { - if (!compare(macro_arg(a, i), macro_arg(b, i))) - return false; - } - return true; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - -public: - expr_eq_modulo_placeholders_fn() {} - bool operator()(expr const & a, expr const & b) { return compare(a, b); } -}; - -definition_cache::entry::entry(expr const & pre_t, expr const & pre_v, - level_param_names const & ps, expr const & t, expr const & v, - dependencies const & deps, uint64 fingerprint, bool is_trusted): - m_pre_type(pre_t), m_pre_value(pre_v), m_params(ps), - m_type(t), m_value(v), m_dependencies(deps), m_fingerprint(fingerprint), m_is_trusted(is_trusted) {} - -definition_cache::definition_cache() {} - -void definition_cache::load(std::istream & in) { - lock_guard lc(m_mutex); - deserializer d(in); - unsigned num; - d >> num; - for (unsigned i = 0; i < num; i++) { - name n; - level_param_names ls; - expr pre_type, pre_value, type, value; - d >> n >> pre_type >> pre_value >> ls >> type >> value; - dependencies deps; - unsigned num; - d >> num; - for (unsigned i = 0; i < num; i++) { - name n; unsigned h; - d >> n >> h; - deps.insert(n, h); - } - uint64 fingerprint; - bool is_trusted; - d >> fingerprint >> is_trusted; - add_core(n, pre_type, pre_value, ls, type, value, deps, fingerprint, is_trusted); - } -} - -void definition_cache::collect_dependencies(environment const & env, expr const & e, dependencies & deps) { - for_each(e, [&](expr const & e, unsigned) { - if (!is_constant(e)) - return true; - name const & n = const_name(e); - if (deps.contains(n)) - return true; - auto d = env.find(n); - if (!d) - return true; - deps.insert(n, hash_bi(d->get_type())); - return true; - }); -} - -void definition_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, - dependencies const & deps, uint64 fingerprint, bool is_trusted) { - m_definitions.insert(n, entry(pre_type, pre_value, ls, type, value, deps, fingerprint, is_trusted)); -} - -void definition_cache::add(environment const & env, name const & n, expr const & pre_type, expr const & pre_value, - level_param_names const & ls, expr const & type, expr const & value, bool is_trusted) { - dependencies deps; - collect_dependencies(env, type, deps); - collect_dependencies(env, value, deps); - uint64 fingerprint = get_fingerprint(env); - lock_guard lc(m_mutex); - add_core(n, pre_type, pre_value, ls, type, value, deps, fingerprint, is_trusted); -} - -void definition_cache::erase(name const & n) { - lock_guard lc(m_mutex); - m_definitions.erase(n); -} - -void definition_cache::clear() { - lock_guard lc(m_mutex); - m_definitions.clear(); -} - -/** \brief Return true iff the type of all declarations in deps still have the same hashcode - stored in deps. */ -bool definition_cache::check_dependencies(environment const & env, dependencies const & deps) { - bool ok = true; - deps.for_each([&](name const & n, unsigned h) { - if (ok) { - if (auto d = env.find(n)) { - if (h != hash_bi(d->get_type())) - ok = false; - } else { - ok = false; - } - } - }); - return ok; -} - -optional> -definition_cache::find(environment const & env, name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted) { - entry e; - { - lock_guard lc(m_mutex); - if (auto it = m_definitions.find(n)) { - e = *it; - } else { - return optional>(); - } - } - level_param_names ls; - if (e.m_is_trusted == is_trusted && - expr_eq_modulo_placeholders_fn()(e.m_pre_type, pre_type) && - expr_eq_modulo_placeholders_fn()(e.m_pre_value, pre_value) && - get_fingerprint(env) == e.m_fingerprint && - check_dependencies(env, e.m_dependencies)) { - return some(std::make_tuple(e.m_params, e.m_type, e.m_value)); - } else { - return optional>(); - } -} - -void definition_cache::save(std::ostream & out) { - lock_guard lc(m_mutex); - serializer s(out); - s << m_definitions.size(); - m_definitions.for_each([&](name const & n, entry const & e) { - s << n << e.m_pre_type << e.m_pre_value << e.m_params - << e.m_type << e.m_value; - s << static_cast(e.m_dependencies.size()); - e.m_dependencies.for_each([&](name const & n, unsigned h) { - s << n << h; - }); - s << e.m_fingerprint << e.m_is_trusted; - }); -} -} diff --git a/src/library/definition_cache.h b/src/library/definition_cache.h deleted file mode 100644 index e6dd3b06e8..0000000000 --- a/src/library/definition_cache.h +++ /dev/null @@ -1,60 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/int64.h" -#include "util/thread.h" -#include "util/name_map.h" -#include "util/optional.h" -#include "kernel/expr.h" - -namespace lean { -/** \brief Cache for mapping definitions (type, value) before elaboration to (level_names, type, value) - after elaboration. -*/ -class definition_cache { - typedef name_map dependencies; // store the hash code for the type of used constants - struct entry { - expr m_pre_type; - expr m_pre_value; - level_param_names m_params; - expr m_type; - expr m_value; - dependencies m_dependencies; - uint64 m_fingerprint; - bool m_is_trusted; - entry() {} - entry(expr const & pre_t, expr const & pre_v, level_param_names const & ps, expr const & t, expr const & v, - dependencies const & deps, uint64 fingerprint, bool is_trusted); - }; - mutex m_mutex; - name_map m_definitions; - void collect_dependencies(environment const & env, expr const & e, dependencies & deps); - bool check_dependencies(environment const & env, dependencies const & deps); - 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, dependencies const & deps, uint64 fingerprint, bool is_trusted); -public: - definition_cache(); - /** \brief Add the cache entry (n, pre_type, pre_value) -> (ls, type, value) */ - void add(environment const & env, name const & n, expr const & pre_type, expr const & pre_value, - level_param_names const & ls, expr const & type, expr const & value, bool is_trusted); - /** \brief Return (if available) elaborated (level_names, type, value) for (n, pre_type, pre_value). - The pre_type and pre_value are compared modulo placeholders names if the cached values. - In principle, we could have compared only the name and pre_type, but we only want to use cached values if the - user intent (captured by pre_value) did not change. - */ - optional> - find(environment const & env, name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted); - /** \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); - /** \brief Remove the entry named \c n from the cache. */ - void erase(name const & n); - /** \brief Clear the whole cache */ - void clear(); -}; -} diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 3ac348ae50..8ec933e9f2 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -29,7 +29,6 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/type_context.h" #include "library/io_state_stream.h" -#include "library/definition_cache.h" #include "library/export.h" #include "library/message_builder.h" #include "frontends/lean/parser.h" @@ -51,7 +50,6 @@ using lean::io_state; using lean::io_state_stream; using lean::regular; using lean::mk_environment; -using lean::definition_cache; using lean::pos_info; using lean::pos_info_provider; using lean::optional; @@ -137,7 +135,6 @@ static struct option g_long_options[] = { {"threads", required_argument, 0, 'j'}, #endif {"quiet", no_argument, 0, 'q'}, - {"cache", required_argument, 0, 'c'}, {"deps", no_argument, 0, 'd'}, {"json", no_argument, 0, 'J'}, {"server", no_argument, 0, 'S'}, @@ -157,7 +154,7 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#define OPT_STR "PFdD:qupgvhk:012t:012o:E:c:L:012O:012GZAIT:B:" +#define OPT_STR "PFdD:qupgvhk:012t:012o:E:L:012O:012GZAIT:B:" #if defined(LEAN_TRACK_MEMORY) #define OPT_STR2 OPT_STR "M:012" @@ -223,8 +220,6 @@ int main(int argc, char ** argv) { bool smt2 = false; bool only_deps = false; unsigned num_threads = 1; - bool read_cache = false; - bool save_cache = false; bool json_output = false; bool server = false; options opts; @@ -268,11 +263,6 @@ int main(int argc, char ** argv) { output = optarg; export_objects = true; break; - case 'c': - cache_name = optarg; - read_cache = true; - save_cache = true; - break; case 'M': lean::set_max_memory_megabyte(atoi(optarg)); opts = opts.update(lean::get_max_memory_opt_name(), atoi(optarg)); @@ -346,13 +336,10 @@ int main(int argc, char ** argv) { #endif if (show_hole && line && column) { opts = set_show_hole(opts, *line, *column); - save_cache = false; } else if (show_goal && line && column) { opts = set_show_goal(opts, *line, *column); - save_cache = false; } else if (show_info && line && column) { opts = set_show_info(opts, *line, *column); - save_cache = false; } #if !defined(LEAN_MULTI_THREAD) @@ -393,24 +380,6 @@ int main(int argc, char ** argv) { return 0; } - definition_cache cache; - definition_cache * cache_ptr = nullptr; - if (read_cache) { - try { - cache_ptr = &cache; - shared_file_lock cache_lock(cache_name); - std::ifstream in(cache_name, std::ifstream::binary); - if (!in.bad() && !in.fail()) - cache.load(in); - } catch (lean::throwable & ex) { - cache_ptr = nullptr; - auto out = lean::message_builder(env, ios, argv[optind], lean::pos_info(1, 1), lean::WARNING); - out << "failed to load cache file '" << cache_name << "'\n"; - out.set_exception(ex); - out << "cache is going to be ignored"; - out.report(); - } - } try { bool ok = true; for (int i = optind; i < argc; i++) { @@ -418,8 +387,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], base_dir, false, num_threads, - cache_ptr)) { + } else if (!parse_commands(env, ios, argv[i], base_dir, false, num_threads)) { ok = false; } } catch (lean::exception & ex) { @@ -427,11 +395,6 @@ int main(int argc, char ** argv) { lean::message_builder(env, ios, argv[i], lean::pos_info(1, 1), lean::ERROR).set_exception(ex).report(); } } - if (save_cache) { - exclusive_file_lock cache_lock(cache_name); - std::ofstream out(cache_name, std::ofstream::binary); - cache.save(out); - } if (export_objects && ok) { exclusive_file_lock output_lock(output); std::ofstream out(output, std::ofstream::binary);