From 8da44f1cd5e519c3959487c611531893bdcd6ca8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Jul 2014 04:11:17 +0100
Subject: [PATCH] feat(frontends/lean/parser): disable quasie-hash consing in
 new threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp | 3 ++-
 src/util/worker_queue.h       | 6 ++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 5157798e0..d4cc53339 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -75,7 +75,8 @@ parser::parser(environment const & env, io_state const & ios,
     m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds),
-    m_pos_table(std::make_shared<pos_info_table>()), m_theorem_queue(num_threads > 1 ? num_threads - 1 : 0) {
+    m_pos_table(std::make_shared<pos_info_table>()),
+    m_theorem_queue(num_threads > 1 ? num_threads - 1 : 0, []() { enable_expr_caching(false); }) {
     m_scanner.set_line(line);
     m_num_threads = num_threads;
     m_no_undef_id_error    = false;
diff --git a/src/util/worker_queue.h b/src/util/worker_queue.h
index a457fce19..b321faf08 100644
--- a/src/util/worker_queue.h
+++ b/src/util/worker_queue.h
@@ -54,7 +54,8 @@ class worker_queue {
     }
 
 public:
-    worker_queue(unsigned num_threads):m_todo_qhead(0), m_done(false), m_failed_thread(-1), m_interrupted(false) {
+    template<typename F>
+    worker_queue(unsigned num_threads, F const & f):m_todo_qhead(0), m_done(false), m_failed_thread(-1), m_interrupted(false) {
 #ifndef LEAN_MULTI_THREAD
         num_threads = 0;
 #endif
@@ -62,6 +63,7 @@ public:
             m_thread_exceptions.push_back(exception_ptr(nullptr));
         for (unsigned i = 0; i < num_threads; i++) {
             m_threads.push_back(std::unique_ptr<interruptible_thread>(new interruptible_thread([=]() {
+                            f();
                             try {
                                 while (auto t = next_task()) {
                                     add_result((*t)());
@@ -78,7 +80,7 @@ public:
                         })));
         }
     }
-
+    worker_queue(unsigned num_threads):worker_queue(num_threads, [](){ return; }) {}
     ~worker_queue() { if (!m_done) join(); }
 
     void add(std::function<T()> const & fn) {