michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): disable quasie-hash consing in new threads

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 04:11:17 +01:00
parent f942c6f64c
commit 8da44f1cd5
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -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;

6
src/util/worker_queue.h
View file

@ -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) {