From d454cc8bcdb1ab4e9f0033da451be6c74cc52208 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Nov 2016 17:14:15 -0800
Subject: [PATCH] feat(frontends/lean/elaborator): do not populate info_manager
 during thread finalization

---
 src/frontends/lean/elaborator.cpp | 3 ++-
 src/util/thread.cpp               | 7 +++++++
 src/util/thread.h                 | 2 ++
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index c0893ea934..842569b678 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include "util/flet.h"
+#include "util/thread.h"
 #include "kernel/find_fn.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
@@ -119,7 +120,7 @@ elaborator::elaborator(environment const & env, options const & opts, metavar_co
 
 elaborator::~elaborator() {
     try {
-        if (m_uses_infom && get_global_info_manager()) {
+        if (m_uses_infom && get_global_info_manager() && !in_thread_finalization()) {
             m_info.instantiate_mvars(m_ctx.mctx());
             get_global_info_manager()->merge(m_info);
         }
diff --git a/src/util/thread.cpp b/src/util/thread.cpp
index c697b78d4a..c141429f3b 100644
--- a/src/util/thread.cpp
+++ b/src/util/thread.cpp
@@ -31,9 +31,16 @@ void initialize_thread() {}
 void finalize_thread() {}
 #endif
 
+LEAN_THREAD_VALUE(bool, g_finalizing, false);
+
+bool in_thread_finalization() {
+    return g_finalizing;
+}
+
 typedef std::vector<std::pair<thread_finalizer, void*>> thread_finalizers;
 
 void run_thread_finalizers_core(thread_finalizers & fns) {
+    g_finalizing = true;
     unsigned i = fns.size();
     while (i > 0) {
         --i;
diff --git a/src/util/thread.h b/src/util/thread.h
index 8200a41928..376a40161f 100644
--- a/src/util/thread.h
+++ b/src/util/thread.h
@@ -223,4 +223,6 @@ void register_thread_finalizer(thread_finalizer fn, void * p);
 void run_thread_finalizers();
 void run_post_thread_finalizers();
 void delete_thread_finalizer_manager();
+
+bool in_thread_finalization();
 }