fix(library/type_context): non deterministic failure at bitwise.lean

We were getting the following error non deterministically:

```
library/init/data/nat/bitwise.lean:131:6: error: exact tactic failed, type mismatch, given expression has type
  z = f ff 0 z
but is expected to have type
  eq.rec z e = f ff 0 (binary_rec f z 0)
state:
C : ℕ → Sort u,
f : Π (b : bool) (n : ℕ), C n → C (bit b n),
z : C 0,
h : f ff 0 z = z,
b : bool,
n : ℕ,
b0 : bit b n = 0,
bf : bodd 0 = b,
n0 : shiftr 0 1 = n,
e : 0 = bit ff 0
⊢ eq.rec z e = f ff 0 (binary_rec f z 0)
```

This error was happening because of the type_context.unfold_lemmas new
flag. The type context thread local cache must be flushed whenever the
value of type_context.unfold_lemmas has changed.
This commit is contained in:
Leonardo de Moura 2017-06-01 13:39:12 -07:00
parent 291b61555a
commit 9c79b361dc

View file

@ -180,7 +180,11 @@ type_context_cache_ptr type_context_cache_manager::release() {
}
type_context_cache_ptr type_context_cache_manager::mk(environment const & env, options const & o) {
if (!m_cache_ptr || get_class_instance_max_depth(o) != m_max_depth) return mk_cache(env, o, m_use_bi);
if (!m_cache_ptr ||
get_class_instance_max_depth(o) != m_max_depth ||
get_unfold_lemmas(o) != get_unfold_lemmas(m_cache_ptr->m_options)) {
return mk_cache(env, o, m_use_bi);
}
if (is_eqp(env, m_env)) {
m_cache_ptr->m_options = o;
return release();