From 9c79b361dc4a0835c66e4dea6ddc8ea4cace4d59 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Jun 2017 13:39:12 -0700
Subject: [PATCH] fix(library/type_context): non deterministic failure at
 bitwise.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 src/library/type_context.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 0a5d3cd7e5..065e00d0d7 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -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();