From af78fd0a3ca4c8d5a0c271bc71cb8fce840459c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Sep 2016 10:51:25 -0700 Subject: [PATCH] fix(library/tactic/user_attribute): make sure it compiles when using older versions of g++ --- src/library/tactic/user_attribute.cpp | 8 +++++++- tests/lean/caching_user_attribute.lean.expected.out | 2 ++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index e58c875535..ac196a939a 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/src/library/tactic/user_attribute.cpp @@ -49,6 +49,7 @@ private: struct entry { unsigned m_fingerprint; vm_obj m_val; + entry(unsigned f, vm_obj const & val):m_fingerprint(f), m_val(val) {} }; name_hash_map m_cache; @@ -58,6 +59,10 @@ public: if (it != m_cache.end()) { if (it->second.m_fingerprint == attr.get_fingerprint(env)) return it->second.m_val; + lean_trace("user_attributes_cache", tout() << "cached result for [" << attr.get_name() << "] " + << "has been found, but cache fingerprint does not match\n";); + } else { + lean_trace("user_attributes_cache", tout() << "no cached result for [" << attr.get_name() << "]\n";); } lean_trace("user_attributes_cache", tout() << "recomputing cache for [" << attr.get_name() << "]\n";); @@ -66,7 +71,8 @@ public: auto cached = invoke(cache_handler, to_vm_list(to_list(instances), [&](const name & inst) { return to_obj(env.get(inst)); })); - return m_cache[attr.get_name()] = entry {attr.get_fingerprint(env), cached}; + m_cache.erase(attr.get_name()); + m_cache.insert(mk_pair(attr.get_name(), entry(attr.get_fingerprint(env), cached))); return cached; } }; diff --git a/tests/lean/caching_user_attribute.lean.expected.out b/tests/lean/caching_user_attribute.lean.expected.out index e9bd9addaa..dad07c836a 100644 --- a/tests/lean/caching_user_attribute.lean.expected.out +++ b/tests/lean/caching_user_attribute.lean.expected.out @@ -1,3 +1,4 @@ +[user_attributes_cache] no cached result for [foo] [user_attributes_cache] recomputing cache for [foo] eq.refl eq.mp @@ -5,6 +6,7 @@ eq.mp eq.refl eq.mp +[user_attributes_cache] cached result for [foo] has been found, but cache fingerprint does not match [user_attributes_cache] recomputing cache for [foo] eq.refl eq.mpr