chore(*): annotate candidates for thread local cache reset

src/frontends/lean/elaborator.cpp

@@ -69,6 +69,7 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET(type_context_cache_manager, get_tcm, true /* use binder information at infer_cache */);
 
 static name * g_elab_strategy = nullptr;

src/kernel/abstract.cpp

@@ -95,6 +95,7 @@ public:
     }
 };
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(mk_binding_cache, get_mk_binding_cache);
 
 template<bool is_lambda>

src/kernel/expr.cpp

@@ -406,6 +406,7 @@ expr_macro::~expr_macro() {}
 // Constructors
 LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, false);
 typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(expr_cache, get_expr_cache);
 
 struct cache_expr_insert_fn {

src/kernel/expr_eq_fn.cpp

@@ -49,6 +49,7 @@ struct eq_cache {
     }
 };
 
+/* CACHE_RESET: No */
 MK_THREAD_LOCAL_GET_DEF(eq_cache, get_eq_cache);
 
 /** \brief Functional object for comparing expressions.

src/kernel/for_each_fn.cpp

@@ -48,6 +48,7 @@ struct for_each_cache {
     }
 };
 
+/* CACHE_RESET: NO */
 MK_CACHE_STACK(for_each_cache, LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY)
 
 class for_each_fn {

src/kernel/instantiate.cpp

@@ -189,6 +189,7 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, level
         });
 }
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 

src/kernel/level.cpp

@@ -247,6 +247,7 @@ bool is_one(level const & l) { return l == mk_level_one(); }
 
 typedef typename std::unordered_set<level, level_hash> level_cache;
 LEAN_THREAD_VALUE(bool, g_level_cache_enabled, false);
+/* CACHE_RESET: No */
 MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
 bool enable_level_caching(bool f) {
     bool r = g_level_cache_enabled;

src/kernel/replace_fn.cpp

@@ -52,6 +52,7 @@ struct replace_cache {
     }
 };
 
+/* CACHE_RESET: NO */
 MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
 
 class replace_rec_fn {

src/library/app_builder.cpp

@@ -123,6 +123,7 @@ public:
 
 typedef cache_compatibility_helper<app_builder_cache> app_builder_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(app_builder_cache_helper, get_abch);
 
 /** Return an app_builder_cache for the transparency_mode in ctx, and compatible with the environment. */

src/library/congr_lemma.cpp

@@ -41,6 +41,7 @@ struct congr_lemma_cache {
 
 typedef cache_compatibility_helper<congr_lemma_cache> congr_lemma_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(congr_lemma_cache_helper, get_clch);
 
 congr_lemma_cache & get_congr_lemma_cache_for(type_context const & ctx) {

src/library/fun_info.cpp

@@ -53,6 +53,7 @@ struct fun_info_cache {
 
 typedef cache_compatibility_helper<fun_info_cache> fun_info_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(fun_info_cache_helper, get_fich);
 
 fun_info_cache & get_fun_info_cache_for(type_context const & ctx) {

src/library/tactic/ac_tactics.cpp

@@ -30,6 +30,7 @@ struct ac_manager_old::cache {
         m_instance_fingerprint(get_instance_fingerprint(env)) {}
 };
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(ac_manager_old::cache_ptr, get_cache_ptr);
 
 static ac_manager_old::cache_ptr get_cache(environment const & env) {

src/library/tactic/simp_lemmas.cpp

@@ -1199,6 +1199,9 @@ public:
     }
 };
 
+/* CACHE_RESET: YES
+
+   Do we still need this cache? Can we use user_attr_cache infrastructure. */
 MK_THREAD_LOCAL_GET_DEF(simp_lemmas_cache, get_cache);
 
 simp_lemmas get_simp_lemmas(environment const & env, simp_lemmas_token tk) {

src/library/tactic/smt/congruence_closure.cpp

@@ -94,6 +94,7 @@ public:
     }
 };
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(ext_congr_lemma_cache_manager, get_clcm);
 
 congruence_closure::congruence_closure(type_context & ctx, state & s, defeq_canonizer::state & dcs,

src/library/tactic/smt/ematch.cpp

@@ -90,6 +90,7 @@ vm_obj ematch_state::mk_vm_ematch_config() const {
     return mk_vm_constructor(0, mk_vm_nat(get_config().m_max_instances), mk_vm_nat(get_config().m_max_generation));
 }
 
+/* CACHE_RESET: NO */
 /* Allocator for ematching constraints. */
 MK_THREAD_LOCAL_GET(small_object_allocator, get_emc_allocator, "ematch constraint");
 

src/library/tactic/tactic_state.cpp

@@ -321,6 +321,7 @@ vm_obj tactic_target(vm_obj const & o) {
     return tactic::mk_success(to_obj(g->get_type()), s);
 }
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm);
 
 type_context mk_type_context_for(environment const & env, options const & o, metavar_context const & mctx,

src/library/tactic/user_attribute.cpp

@@ -232,6 +232,10 @@ struct user_attr_cache {
     name_hash_map<entry> m_cache;
 };
 
+/* CACHE_RESET: NO
+
+   This cache contains vm_objects.
+*/
 MK_THREAD_LOCAL_GET_DEF(user_attr_cache, get_user_attribute_cache);
 
 static bool check_dep_fingerprints(environment const & env, list<name> const & dep_names, list<unsigned> const & dep_fingerprints) {

src/library/type_context.h

@@ -41,7 +41,10 @@ bool is_at_least_instances(transparency_mode m);
 transparency_mode ensure_semireducible_mode(transparency_mode m);
 transparency_mode ensure_instances_mode(transparency_mode m);
 
-/* \brief Cached information for type_context. */
+/* \brief Cached information for type_context.
+
+   TODO(Leo): reevaluate the cache validation policies we use.
+ */
 class type_context_cache {
     typedef std::unordered_map<name, optional<declaration>, name_hash> transparency_cache;
     typedef std::unordered_map<name, bool, name_hash> name2bool;

src/util/fresh_name.cpp

@@ -20,7 +20,9 @@ static void register_fresh_name_prefix(name const & p) {
     g_fresh_name_prefixes->insert(p);
 }
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(name, get_prefix);
+/* CACHE_RESET: YES */
 LEAN_THREAD_VALUE(unsigned, g_next_idx, 0);
 
 static bool is_fresh_prefix(name const & p) {
@@ -37,6 +39,7 @@ name mk_fresh_name() {
         prefix = name::mk_internal_unique_name();
         register_fresh_name_prefix(prefix);
     }
+    /* REMARK: after we implement RESET operation we will not need the following test anymore */
     if (g_next_idx == std::numeric_limits<unsigned>::max()) {
         // avoid overflow
         prefix = name(prefix, g_next_idx);