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<std::tuple<level_param_names, expr, expr>> {
-    if (m_cache)
-        return m_cache->find(m_env, n, pre_type, pre_value, is_trusted);
-    else
-        return optional<std::tuple<level_param_names, expr, expr>>();
-}
-
 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<std::string> 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<std::string> 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<std::tuple<level_param_names, expr, expr>>
-    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<std::string> 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<std::string> 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<char const *, char const *> 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<name> 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<mutex> 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<mutex> 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<mutex> lc(m_mutex);
-    m_definitions.erase(n);
-}
-
-void definition_cache::clear() {
-    lock_guard<mutex> 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<std::tuple<level_param_names, expr, expr>>
-definition_cache::find(environment const & env, name const & n, expr const & pre_type, expr const & pre_value, bool is_trusted) {
-    entry e;
-    {
-        lock_guard<mutex> lc(m_mutex);
-        if (auto it = m_definitions.find(n)) {
-            e = *it;
-        } else {
-            return optional<std::tuple<level_param_names, expr, expr>>();
-        }
-    }
-    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<std::tuple<level_param_names, expr, expr>>();
-    }
-}
-
-void definition_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) {
-            s << n << e.m_pre_type << e.m_pre_value << e.m_params
-              << e.m_type << e.m_value;
-            s << static_cast<unsigned>(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<unsigned> 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<entry> 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<std::tuple<level_param_names, expr, expr>>
-    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);