From 73bf232feae84bcdb493be21b45b4e9d1d81bcba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Dec 2016 17:54:28 -0800
Subject: [PATCH] fix(library/module): deadlock?

This commit also undoes the hackish workaround used at e33bd2e66581

@gebner Could you please take a quick look at this fix, and check
whether it makes sense?
---
 src/library/module.cpp          | 28 +++++++++++++++++++++++++---
 src/library/tactic/ac_tactics.h |  3 ++-
 src/library/unfold_macros.cpp   |  2 +-
 3 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/src/library/module.cpp b/src/library/module.cpp
index 0de26167fa..64265420e5 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -276,13 +276,35 @@ struct decl_modification : public modification {
     LEAN_MODIFICATION("decl")
 
     declaration m_decl;
+    bool        m_from_olean;
 
     decl_modification() {}
-    decl_modification(declaration const & decl) : m_decl(decl) {}
+    decl_modification(declaration const & decl, bool from_olean = false):
+        m_decl(decl), m_from_olean(from_olean) {}
 
     void perform(environment & env) const override {
         auto decl = m_decl;
-        decl = unfold_untrusted_macros(env, decl);
+        /* Gabriel, I had to add the following condition to avoid a deadlock that was happening at Travis.
+           I managed to reproduce the deadlock on my macbook, but it doesn't happen in my Ubuntu desktop.
+           The problem was exposed by commit 7f86ad64eb9d5f644. Before this commit, unfold_untrusted_macros
+           was a no-op if the user did not set the trust level in the command line.
+
+           The procedure unfold_untrusted_macros tries to access decl.get_value(). I believe the dead lock
+           occurs when we try to perform the modification but the proof elaboration did not finish yet.
+
+           The unfold_untrusted_macros is only needed when we are importing the declaration from a .olean
+           file that has been created with a different (and higher) trust level. So, it may contain macros
+           that will not be accepted by the current kernel, and they must be unfolded.
+
+           In a single Lean session, the trust level is fixed, and we invoke unfold_untrusted_macros
+           at frontends/lean/definition_cmds.cpp before we even create the declaration. So, I added
+           the flag m_from_olean to distinguish whether the modification came from a .olean or a .lean file.
+           I'm setting it to true at deserialize.
+        */
+        if (m_from_olean) {
+            decl = unfold_untrusted_macros(env, decl);
+        }
+
         if (decl.get_name() == get_sorry_name() && has_sorry(env)) {
             // ignore double sorrys
             return;
@@ -296,7 +318,7 @@ struct decl_modification : public modification {
     }
 
     static std::shared_ptr<modification const> deserialize(deserializer & d) {
-        return std::make_shared<decl_modification>(read_declaration(d));
+        return std::make_shared<decl_modification>(read_declaration(d), true);
     }
 
     void get_task_dependencies(std::vector<generic_task_result> & deps) const override {
diff --git a/src/library/tactic/ac_tactics.h b/src/library/tactic/ac_tactics.h
index 58a8596e32..6abba8093d 100644
--- a/src/library/tactic/ac_tactics.h
+++ b/src/library/tactic/ac_tactics.h
@@ -7,7 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/type_context.h"
 
-#define LEAN_AC_MACROS_TRUST_LEVEL 10
+/* TODO(Leo): reduce after testing */
+#define LEAN_AC_MACROS_TRUST_LEVEL 10000000
 
 namespace lean {
 class ac_manager {
diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index f7ae7099fe..962ffae858 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 /* If the trust level of all macros is < LEAN_BELIEVER_TRUST_LEVEL,
    then we skip the unfold_untrusted_macros potentially expensive step.
    The following definition is commented because we are currently testing the AC macros. */
-#define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
+// #define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
 
 namespace lean {
 class unfold_untrusted_macros_fn {