diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 94c4d2dfe3..065010b746 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -16,5 +16,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp locals.cpp normalize.cpp discr_tree.cpp - task_queue.cpp mt_task_queue.cpp st_task_queue.cpp + task_queue.cpp mt_task_queue.cpp st_task_queue.cpp task_helper.cpp messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp) diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp index 33a0f10cfe..4a99db35e9 100644 --- a/src/library/mt_task_queue.cpp +++ b/src/library/mt_task_queue.cpp @@ -10,6 +10,7 @@ Author: Gabriel Ebner #include "library/mt_task_queue.h" #include "util/interrupt.h" #include "util/flet.h" +#include "task_helper.h" #if defined(LEAN_MULTI_THREAD) namespace lean { @@ -105,7 +106,7 @@ void mt_task_queue::spawn_worker() { scoped_current_task scope_cur_task(&t); lock.unlock(); if (cb) cb(t->m_task); - is_ok = t->execute(); + is_ok = execute_task_with_scopes(&*t); lock.lock(); } reset_interrupt(); diff --git a/src/library/st_task_queue.cpp b/src/library/st_task_queue.cpp index 0670f0184d..04d3f7eece 100644 --- a/src/library/st_task_queue.cpp +++ b/src/library/st_task_queue.cpp @@ -6,6 +6,7 @@ Author: Gabriel Ebner */ #include #include "library/st_task_queue.h" +#include "task_helper.h" namespace lean { @@ -44,7 +45,7 @@ void st_task_queue::submit(generic_task_result const & t) { } if (m_progress_cb) m_progress_cb(t->m_task); - bool is_ok = t->execute(); + bool is_ok = execute_task_with_scopes(&*t); t->m_state = is_ok ? task_result_state::FINISHED : task_result_state::FAILED; t->clear_task(); } diff --git a/src/library/task_helper.cpp b/src/library/task_helper.cpp new file mode 100644 index 0000000000..2ed6066978 --- /dev/null +++ b/src/library/task_helper.cpp @@ -0,0 +1,44 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#include +#include +#include +#include "library/task_helper.h" + +namespace lean { + +bool execute_task_with_scopes(generic_task_result_cell * task) { + lean_assert(!task->has_evaluated()); + try { + scoped_task_context ctx(task->m_task->get_module_id(), task->m_task->get_task_pos()); + scope_message_context scope_msg_ctx(task->m_task->get_bucket()); + try { + scope_traces_as_messages scope_traces(task->m_task->get_module_id(), task->m_task->get_pos()); + task->execute_and_store_result(); + } catch (task_cancellation_exception) { + throw; + } catch (interrupted) { + throw; + } catch (throwable & ex) { + environment env; + message_builder builder(env, get_global_ios(), task->m_task->get_module_id(), task->m_task->get_pos(), ERROR); + builder.set_exception(ex); + builder.report(); + throw; + } + return true; + } catch (interrupted) { + task->m_ex = std::make_exception_ptr( + task_cancellation_exception(generic_task_result(task))); + return false; + } catch (...) { + task->m_ex = std::current_exception(); + return false; + } +} + +} diff --git a/src/library/task_helper.h b/src/library/task_helper.h new file mode 100644 index 0000000000..95b6c4c99a --- /dev/null +++ b/src/library/task_helper.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Gabriel Ebner +*/ +#pragma once +#include "library/task_queue.h" + +namespace lean { + +bool execute_task_with_scopes(generic_task_result_cell * task); + +} diff --git a/src/library/task_queue.cpp b/src/library/task_queue.cpp index 202835ad06..4e2124f8be 100644 --- a/src/library/task_queue.cpp +++ b/src/library/task_queue.cpp @@ -5,8 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #include -#include -#include #include "library/task_queue.h" namespace lean { @@ -30,36 +28,6 @@ void generic_task_result_cell::clear_task() { } } -bool generic_task_result_cell::execute() { - lean_assert(!has_evaluated()); - try { - scoped_task_context ctx(m_task->get_module_id(), m_task->get_task_pos()); - scope_message_context scope_msg_ctx(m_task->get_bucket()); - try { - scope_traces_as_messages scope_traces(m_task->get_module_id(), m_task->get_pos()); - execute_and_store_result(); - } catch (task_cancellation_exception) { - throw; - } catch (interrupted) { - throw; - } catch (throwable & ex) { - environment env; - message_builder builder(env, get_global_ios(), m_task->get_module_id(), m_task->get_pos(), ERROR); - builder.set_exception(ex); - builder.report(); - throw; - } - return true; - } catch (interrupted) { - m_ex = std::make_exception_ptr( - task_cancellation_exception(generic_task_result(this))); - return false; - } catch (...) { - m_ex = std::current_exception(); - return false; - } -} - LEAN_THREAD_PTR(task_queue, g_tq); scope_global_task_queue::scope_global_task_queue(task_queue * tq) { m_old_tq = g_tq; diff --git a/src/library/task_queue.h b/src/library/task_queue.h index 7e7cddf2c4..a85c3256a3 100644 --- a/src/library/task_queue.h +++ b/src/library/task_queue.h @@ -24,7 +24,7 @@ enum class task_result_state { }; class generic_task; -class generic_task_result_cell { +struct generic_task_result_cell { MK_LEAN_RC() void dealloc() { delete this; } @@ -51,7 +51,6 @@ class generic_task_result_cell { } virtual void execute_and_store_result() = 0; - bool execute(); }; class generic_task_result {