From e448e4e129d76f7735135775de1ace69fef64866 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 21 Nov 2016 14:04:26 -0500 Subject: [PATCH] refactor(util/task_queue): merge module_task into task and cancel by position --- src/frontends/lean/definition_cmds.cpp | 20 +++---- src/frontends/lean/parser.cpp | 1 + src/kernel/type_checker.cpp | 6 +- src/library/module_mgr.cpp | 53 +++++++---------- src/library/module_mgr.h | 80 -------------------------- src/library/versioned_msg_buf.cpp | 18 ------ src/library/versioned_msg_buf.h | 5 -- src/shell/server.cpp | 30 +++++----- src/util/mt_task_queue.cpp | 37 ++++++++++-- src/util/mt_task_queue.h | 8 ++- src/util/st_task_queue.cpp | 2 + src/util/st_task_queue.h | 2 + src/util/task_queue.cpp | 39 ++++++++++++- src/util/task_queue.h | 38 ++++++++++-- 14 files changed, 163 insertions(+), 176 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index a8711abf65..1a041fbb21 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -573,7 +573,7 @@ static expr inline_new_defs(environment const & old_env, environment const & new }); } -class proof_elaboration_task : public module_task { +class proof_elaboration_task : public task { environment m_decl_env; options m_opts; bool m_use_info_manager; @@ -596,23 +596,22 @@ public: bool is_rfl_lemma, expr const & final_type, metavar_context const & mctx, local_context const & lctx, parser_pos_provider const & prov) : - module_task(optional(prov.get_some_pos()), task_kind::elab), m_decl_env(decl_env), m_opts(opts), m_use_info_manager(get_global_info_manager() != nullptr), m_params(params.begin(), params.end()), m_fn(fn), m_val(val), m_finfo(finfo), m_is_rfl_lemma(is_rfl_lemma), m_final_type(final_type), m_mctx(mctx), m_lctx(lctx), m_pos_provider(prov) {} void description(std::ostream & out) const override { - out << "proving " << local_pp_name(m_fn) << " (" << get_module() << ")"; + out << "proving " << local_pp_name(m_fn) << " (" << get_module_id() << ")"; } - expr execute_core() override { + expr execute() override { scoped_expr_caching disable(false); // FIXME: otherwise sigma.eq fails to elaborate auto tc = std::make_shared(m_decl_env, m_opts, m_mctx, m_lctx); scope_trace_env scope2(m_decl_env, m_opts, *tc); scope_pos_info_provider scope3(m_pos_provider); scoped_info_manager scope4( - m_use_info_manager ? get_scope_message_context().enable_info_manager(get_module()) + m_use_info_manager ? get_scope_message_context().enable_info_manager(get_module_id()) : nullptr); try { @@ -635,7 +634,7 @@ public: } }; -class example_checking_task : public module_task { +class example_checking_task : public task { environment m_decl_env; options m_opts; bool m_use_info_manager; @@ -658,24 +657,25 @@ public: expr const & fn, expr const & val, metavar_context const & mctx, local_context const & lctx, parser_pos_provider const & prov) : - module_task(optional(prov.get_some_pos()), task_kind::print), m_decl_env(decl_env), m_opts(opts), m_use_info_manager(get_global_info_manager() != nullptr), m_modifiers(modifiers), m_univ_params(univ_params), m_params(params.begin(), params.end()), m_fn(fn), m_val(val), m_mctx(mctx), m_lctx(lctx), m_pos_provider(prov) { } + task_kind get_kind() const override { return task_kind::print; } + void description(std::ostream & out) const override { - out << "checking example on line " << m_pos_provider.get_some_pos().first << " (" << get_module() << ")"; + out << "checking example on line " << m_pos_provider.get_some_pos().first << " (" << get_module_id() << ")"; } - unit execute_core() override { + unit execute() override { scoped_expr_caching disable(false); // FIXME: otherwise sigma.eq fails to elaborate auto tc = std::make_shared(m_decl_env, m_opts, m_mctx, m_lctx); scope_trace_env scope2(m_decl_env, m_opts, *tc); scope_pos_info_provider scope3(m_pos_provider); scoped_info_manager scope4( - m_use_info_manager ? get_scope_message_context().enable_info_manager(get_module()) + m_use_info_manager ? get_scope_message_context().enable_info_manager(get_module_id()) : nullptr); try { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 918aabcecc..1734e97e4b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2159,6 +2159,7 @@ bool parser::parse_commands() { if (m_stop_at && pos().first > m_stop_at_line) { throw interrupt_parser(); } + scoped_task_context scope_task_ctx(get_current_module(), pos()); scope_message_context scope_msg_ctx; scoped_info_manager scope_infom( // TODO(gabriel): separate flag for snapshots/infos? m_snapshot_vector ? scope_msg_ctx.enable_info_manager(m_file_name) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 30d9f79e1d..bca44aa46c 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -757,12 +757,12 @@ static void check_definition(environment const & env, declaration const & d, typ } } -class proof_checking_task : public module_task { +class proof_checking_task : public task { environment m_env; declaration m_decl; public: proof_checking_task(environment const & env, declaration const & d) : - module_task({}, task_kind::elab), m_env(env), m_decl(d) { + m_env(env), m_decl(d) { lean_assert(d.is_theorem()); } @@ -774,7 +774,7 @@ public: return { m_decl.get_value_task() }; } - expr execute_core() override { + expr execute() override { bool memoize = true; bool trusted_only = m_decl.is_trusted(); type_checker checker(m_env, memoize, trusted_only); diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 3b6188e0ff..01c6d5deba 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -33,7 +33,7 @@ void module_mgr::mark_out_of_date(module_id const & id, buffer & to_r } } -class parse_lean_task : public module_task { +class parse_lean_task : public task { environment m_initial_env; std::string m_contents; snapshot_vector m_snapshots; @@ -44,13 +44,13 @@ public: parse_lean_task(std::string const & contents, environment const & initial_env, snapshot_vector const & snapshots, bool use_snapshots, std::vector> const & deps) : - module_task(optional(), task_kind::parse), m_initial_env(initial_env), m_contents(contents), m_snapshots(snapshots), m_use_snapshots(use_snapshots), m_deps(deps) {} + task_kind get_kind() const override { return task_kind::parse; } void description(std::ostream & out) const override { - out << "parsing " << get_module(); + out << "parsing " << get_module_id(); } std::vector get_dependencies() override { @@ -59,7 +59,7 @@ public: return deps; } - module_info::parse_result execute_core() override { + module_info::parse_result execute() override { module_loader import_fn = [=] (module_id const & base, module_name const & import) { for (auto d : m_deps) { if (std::get<0>(d) == base && @@ -79,7 +79,7 @@ public: bool use_exceptions = false; std::istringstream in(m_contents); - parser p(m_initial_env, get_global_ios(), import_fn, in, get_module(), + parser p(m_initial_env, get_global_ios(), import_fn, in, get_module_id(), use_exceptions, (m_snapshots.empty() || !m_use_snapshots) ? nullptr : &m_snapshots.back(), m_use_snapshots ? &m_snapshots : nullptr); @@ -104,13 +104,12 @@ public: } }; -class olean_compilation_task : public module_task { +class olean_compilation_task : public task { module_info m_mod; public: - olean_compilation_task(module_info const & mod) : - module_task(optional(), task_kind::parse), - m_mod(mod) {} + olean_compilation_task(module_info const & mod) : m_mod(mod) {} + task_kind get_kind() const override { return task_kind::parse; } std::vector get_dependencies() override { if (auto res = m_mod.m_result.peek()) { @@ -125,10 +124,10 @@ public: } void description(std::ostream & out) const override { - out << "saving object code for " << get_module(); + out << "saving object code for " << get_module_id(); } - unit execute_core() override { + unit execute() override { if (m_mod.m_source != module_src::LEAN) throw exception("cannot build olean from olean"); auto res = m_mod.m_result.get(); @@ -159,7 +158,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set scope_global_ios scope_ios(m_ios); scoped_message_buffer scoped_msg_buf(m_msg_buf); - scoped_module_id scoped_mod_mgr(id); + scoped_task_context(id, {1, 0}); message_bucket_id bucket_id { id, m_current_period }; scope_message_context scope_msg_ctx(bucket_id); scope_traces_as_messages scope_trace_msgs(id, {1, 0}); @@ -204,6 +203,10 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set res.m_ok = true; mod.m_result = mk_pure_task_result(res, "Loading " + olean_fn); + get_global_task_queue().cancel_if( + [=] (generic_task * t) { + return t->get_version() < m_current_period && t->get_module_id() == id; + }); if (auto old = m_modules[id].m_result) old.cancel(); m_modules[id] = mod; } else if (src == module_src::LEAN) { @@ -218,6 +221,8 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set return; } } + auto task_pos = snapshots.empty() ? pos_info {1, 0} : snapshots.back().m_pos; + scoped_task_context scope_task_ctx2(id, task_pos); scope_message_context scope_msg_ctx2(bucket_name); @@ -248,7 +253,9 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set if (m_save_olean) mod.m_olean_task = get_global_task_queue().submit(mod); - if (auto old = m_modules[id].m_result) old.cancel(); + get_global_task_queue().cancel_if([=] (generic_task * t) { + return t->get_version() < m_current_period && t->get_module_id() == id && t->get_pos() >= task_pos; + }); m_modules[id] = mod; } else { throw exception("unknown module source"); @@ -389,24 +396,4 @@ std::tuple fs_module_vfs::load_module(module_id return std::make_tuple(read_file(lean_fn), module_src::LEAN, lean_mtime); } -LEAN_THREAD_PTR(module_id, g_scoped_module_id); -scoped_module_id::scoped_module_id(module_id const & module) : m_mod(module) { - m_old = g_scoped_module_id; - g_scoped_module_id = &m_mod; -} -scoped_module_id::~scoped_module_id() { - g_scoped_module_id = m_old; -} -module_id const & get_global_module_id() { - return *g_scoped_module_id; -} - -void generic_module_task::set_result(generic_task_result const & self) { - if (m_auto_cancel) { - if (auto vmb = dynamic_cast(m_msg_buf)) - vmb->cancel_when_invalidated(m_bucket, self); - } - generic_task::set_result(self); -} - } diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index e3c9255624..7211b3e4f6 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -19,8 +19,6 @@ Author: Gabriel Ebner namespace lean { -typedef std::string module_id; - enum class module_src { OLEAN, LEAN, @@ -116,82 +114,4 @@ public: io_state get_io_state() const { return m_ios; } }; -module_id const & get_global_module_id(); -class scoped_module_id { - module_id * m_old; - module_id m_mod; -public: - scoped_module_id(module_id const &); - ~scoped_module_id(); -}; - -class generic_module_task : public generic_task { -public: - enum class task_kind { parse, elab, print }; - -private: - template friend class module_task; - message_buffer * m_msg_buf; - io_state m_ios; - module_id m_mod; - message_bucket_id m_bucket; - optional m_pos; - bool m_auto_cancel; - task_kind m_kind; - -public: - generic_module_task(optional const & pos, task_kind kind, bool auto_cancel) : - m_msg_buf(&get_global_message_buffer()), m_ios(get_global_ios()), - m_mod(get_global_module_id()), - m_bucket(get_scope_message_context().new_sub_bucket()), - m_pos(pos), m_auto_cancel(auto_cancel), m_kind(kind) {} - - void set_result(generic_task_result const & self) override; - - task_kind get_kind() const { return m_kind; } - - module_id get_module() const { return m_mod; } - pos_info get_pos_or_something() const { return m_pos ? *m_pos : pos_info{1, 0}; } -}; - -template -class module_task : public task, public generic_module_task { -public: - module_task(optional const & pos, task_kind kind, bool auto_cancel = true) : - generic_module_task(pos, kind, auto_cancel) {} - - void set_result(generic_task_result const & self) override { - generic_module_task::set_result(self); - } - - virtual T execute_core() = 0; - - T execute() final override; -}; - -template -T module_task::execute() { - scoped_module_id scoped_mod_id(m_mod); - scope_global_ios scoped_ios(m_ios); - scoped_message_buffer scoped_msg_buf(m_msg_buf); - scope_message_context scope_msg_ctx(m_bucket); - if (m_auto_cancel && !m_msg_buf->is_bucket_valid(m_bucket)) { - throw interrupted(); - } - try { - scope_traces_as_messages scope_traces(get_module(), get_pos_or_something()); - return execute_core(); - } catch (task_cancellation_exception) { - throw; - } catch (interrupted) { - throw; - } catch (throwable & ex) { - environment env; - message_builder builder(env, m_ios, get_module(), get_pos_or_something(), ERROR); - builder.set_exception(ex); - builder.report(); - throw; - } -} - } diff --git a/src/library/versioned_msg_buf.cpp b/src/library/versioned_msg_buf.cpp index 2717f3e67d..08d1b508af 100644 --- a/src/library/versioned_msg_buf.cpp +++ b/src/library/versioned_msg_buf.cpp @@ -20,7 +20,6 @@ void versioned_msg_buf::start_bucket(message_bucket_id const & bucket) { auto & buf = m_buf[bucket.m_bucket]; if (buf.m_version < bucket.m_version) { buf.m_version = bucket.m_version; - buf.m_cancel_on_invalidation.reset(); buf.m_msgs.clear(); buf.m_infom.reset(); } @@ -55,16 +54,9 @@ void versioned_msg_buf::finish_bucket(message_bucket_id const & bucket, name_set }); } -void versioned_msg_buf::cancel_bucket(name const & bucket) { - auto & bck_buf = m_buf[bucket]; - bck_buf.m_children.for_each([&] (name const & c) { cancel_bucket(c); }); - if (auto & t = bck_buf.m_cancel_on_invalidation) { t.cancel(); t.reset(); } -} - void versioned_msg_buf::erase_bucket(name const & bucket) { auto & bck_buf = m_buf[bucket]; bck_buf.m_children.for_each([&] (name const & c) { erase_bucket(c); }); - if (auto & t = bck_buf.m_cancel_on_invalidation) t.cancel(); m_buf.erase(bucket); } @@ -114,14 +106,4 @@ std::vector versioned_msg_buf::get_info_managers() { return result; } -void versioned_msg_buf::cancel_when_invalidated(message_bucket_id const & bucket, generic_task_result const & t) { - unique_lock lock(m_mutex); - - auto & buf = m_buf[bucket.m_bucket]; - if (buf.m_version < bucket.m_version) { - if (auto & t_old = buf.m_cancel_on_invalidation) t_old.cancel(); - buf.m_cancel_on_invalidation = t; - } -} - } diff --git a/src/library/versioned_msg_buf.h b/src/library/versioned_msg_buf.h index 7149ddbb71..c5e46cb82a 100644 --- a/src/library/versioned_msg_buf.h +++ b/src/library/versioned_msg_buf.h @@ -20,15 +20,12 @@ class versioned_msg_buf : public message_buffer { std::unique_ptr m_infom; period m_version = 0; - generic_task_result m_cancel_on_invalidation; - name_set m_children; }; mutex m_mutex; std::unordered_map m_buf; - void cancel_bucket(name const & bucket); void erase_bucket(name const & bucket); bool is_bucket_valid_core(message_bucket_id const & bucket); @@ -41,8 +38,6 @@ public: bool is_bucket_valid(message_bucket_id const & bucket) override; void report_info_manager(message_bucket_id const & bucket, info_manager const & infom) override; - void cancel_when_invalidated(message_bucket_id const & bucket, generic_task_result const & t); - std::vector get_messages(); std::vector get_info_managers(); }; diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 9d0945b5be..5603c97481 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -45,6 +45,8 @@ server::server(unsigned num_threads, environment const & initial_env, io_state c m_ios.set_regular_channel(std::make_shared()); m_ios.set_diagnostic_channel(std::make_shared()); + scope_global_ios scoped_ios(m_ios); + scoped_message_buffer scope_msg_buf(&m_msg_buf); #if defined(LEAN_MULTI_THREAD) if (num_threads == 0) m_tq = new st_task_queue; @@ -380,23 +382,21 @@ mt_tq_prioritizer mk_interactive_prioritizer(module_id const & roi) { task_priority p; p.m_prio = DEFAULT_PRIO; - if (auto mod_task = dynamic_cast(t)) { - bool in_roi = mod_task->get_module() == roi; + bool in_roi = t->get_module_id() == roi; - if (!in_roi) - p.m_not_before = { chrono::steady_clock::now() + chrono::seconds(10) }; + if (!in_roi) + p.m_not_before = { chrono::steady_clock::now() + chrono::seconds(10) }; - switch (mod_task->get_kind()) { - case generic_module_task::task_kind::parse: - p.m_prio = in_roi ? ROI_PARSING_PRIO : PARSING_PRIO; - break; - case generic_module_task::task_kind::elab: - p.m_prio = in_roi ? ROI_ELAB_PRIO : ELAB_PRIO; - break; - case generic_module_task::task_kind::print: - p.m_prio = in_roi ? ROI_PRINT_PRIO : PRINT_PRIO; - break; - } + switch (t->get_kind()) { + case task_kind::parse: + p.m_prio = in_roi ? ROI_PARSING_PRIO : PARSING_PRIO; + break; + case task_kind::elab: + p.m_prio = in_roi ? ROI_ELAB_PRIO : ELAB_PRIO; + break; + case task_kind::print: + p.m_prio = in_roi ? ROI_PRINT_PRIO : PRINT_PRIO; + break; } return p; diff --git a/src/util/mt_task_queue.cpp b/src/util/mt_task_queue.cpp index b4ff5341ac..29aa7508ce 100644 --- a/src/util/mt_task_queue.cpp +++ b/src/util/mt_task_queue.cpp @@ -46,7 +46,8 @@ mt_task_queue::mt_task_queue(unsigned num_workers) : }) {} mt_task_queue::mt_task_queue(unsigned num_workers, mt_tq_prioritizer const & prioritizer) : - m_required_workers(num_workers), m_prioritizer(prioritizer) { + m_required_workers(num_workers), m_prioritizer(prioritizer), + m_ios(get_global_ios()), m_msg_buf(&get_global_message_buffer()) { for (unsigned i = 0; i < num_workers; i++) spawn_worker(); } @@ -68,7 +69,10 @@ void mt_task_queue::spawn_worker() { this_worker->m_thread = thread([=] { this_worker->m_interrupt_flag = get_interrupt_flag(); - scope_global_task_queue scope(this); + scope_global_task_queue scope_tq(this); + scope_global_ios scope_ios(m_ios); + scoped_message_buffer scope_msg_buf(m_msg_buf); + unique_lock lock(m_mutex); scoped_add dec_required(m_required_workers, -1); while (true) { @@ -147,6 +151,7 @@ void mt_task_queue::propagate_failure(generic_task_result const & tr) { void mt_task_queue::submit(generic_task_result const & t) { unique_lock lock(m_mutex); + check_interrupted(); t->m_task->m_prio = m_prioritizer(t->m_task); if (check_deps(t)) { if (!t->has_evaluated()) enqueue(t); @@ -228,9 +233,28 @@ void mt_task_queue::wait(generic_task_result const & t) { } } -void mt_task_queue::cancel(generic_task_result const & t) { - if (!t) return; +void mt_task_queue::cancel_if(const std::function & pred) { + std::vector to_cancel; unique_lock lock(m_mutex); + + for (auto & w : m_workers) + if (w->m_current_task && pred(w->m_current_task->m_task)) + to_cancel.push_back(w->m_current_task); + + for (auto & q : m_queue) + for (auto & t : q.second) + if (t->m_task && pred(t->m_task)) + to_cancel.push_back(t); + + for (auto & t : m_waiting) + if (t->m_task && pred(t->m_task)) + to_cancel.push_back(t); + + for (auto & t : to_cancel) + cancel_core(t); +} + +void mt_task_queue::cancel_core(generic_task_result const & t) { switch (t->m_state.load()) { case task_result_state::QUEUED: t->m_ex = std::make_exception_ptr(task_cancellation_exception(t)); @@ -249,6 +273,11 @@ void mt_task_queue::cancel(generic_task_result const & t) { default: return; } } +void mt_task_queue::cancel(generic_task_result const & t) { + if (!t) return; + unique_lock lock(m_mutex); + cancel_core(t); +} bool mt_task_queue::empty() { unique_lock lock(m_mutex); diff --git a/src/util/mt_task_queue.h b/src/util/mt_task_queue.h index 959e7f2963..c9206443e1 100644 --- a/src/util/mt_task_queue.h +++ b/src/util/mt_task_queue.h @@ -12,6 +12,7 @@ Author: Gabriel Ebner #include #include #include +#include #include "util/optional.h" #include "util/task_queue.h" @@ -42,9 +43,11 @@ class mt_task_queue : public task_queue { condition_variable m_wake_up_worker; mt_tq_prioritizer m_prioritizer; - progress_cb m_progress_cb; + io_state m_ios; + message_buffer * m_msg_buf; + generic_task_result dequeue(); void enqueue(generic_task_result const &); @@ -52,6 +55,7 @@ class mt_task_queue : public task_queue { void propagate_failure(generic_task_result const &); void submit(generic_task_result const &) override; void bump_prio(generic_task_result const &, task_priority const &); + void cancel_core(generic_task_result const &); void reprioritize_core(); @@ -66,6 +70,8 @@ public: void wait(generic_task_result const & t) override; void cancel(generic_task_result const & t) override; + void cancel_if(const std::function &pred) override; + void set_progress_callback(progress_cb const & cb) override; void reprioritize(mt_tq_prioritizer const & p); diff --git a/src/util/st_task_queue.cpp b/src/util/st_task_queue.cpp index cd1eaaf687..2c775640c0 100644 --- a/src/util/st_task_queue.cpp +++ b/src/util/st_task_queue.cpp @@ -36,4 +36,6 @@ void st_task_queue::set_progress_callback(progress_cb const & cb) { m_progress_cb = cb; } +void st_task_queue::cancel_if(const std::function &) {} + } diff --git a/src/util/st_task_queue.h b/src/util/st_task_queue.h index c916a5a458..a4dbf0413d 100644 --- a/src/util/st_task_queue.h +++ b/src/util/st_task_queue.h @@ -22,6 +22,8 @@ public: void wait(generic_task_result const & t) override; void cancel(generic_task_result const & t) override; + void cancel_if(const std::function &pred) override; + void set_progress_callback(progress_cb const &) override; }; diff --git a/src/util/task_queue.cpp b/src/util/task_queue.cpp index f5dbac5389..45ca4f27dd 100644 --- a/src/util/task_queue.cpp +++ b/src/util/task_queue.cpp @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #include +#include +#include #include "util/task_queue.h" namespace lean { @@ -15,7 +17,8 @@ std::string generic_task::description() const { return out.str(); } -void generic_task::set_result(generic_task_result const &) {} +generic_task::generic_task() : m_bucket(get_scope_message_context().new_sub_bucket()), + m_mod(get_current_module()), m_pos(get_current_task_pos()) {} generic_task_result_cell::generic_task_result_cell(generic_task * t) : m_rc(0), m_task(t), m_desc(t->description()) {} @@ -30,9 +33,25 @@ void generic_task_result_cell::clear_task() { bool generic_task_result_cell::execute() { lean_assert(!has_evaluated()); try { - execute_and_store_result(); + 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) { + std::cerr << "interrupted: " << m_desc << std::endl; m_ex = std::make_exception_ptr( task_cancellation_exception(generic_task_result(this))); return false; @@ -69,4 +88,20 @@ char const *task_cancellation_exception::what() const noexcept { return m_msg.c_str(); } +LEAN_THREAD_PTR(module_id, g_cur_mod); +LEAN_THREAD_PTR(pos_info, g_cur_task_pos); +scoped_task_context::scoped_task_context(module_id const & mod, pos_info const & pos) : m_id(mod), m_pos(pos) { + m_old_id = g_cur_mod; + m_old_pos = g_cur_task_pos; + g_cur_mod = &m_id; + g_cur_task_pos = &m_pos; +} +scoped_task_context::~scoped_task_context() { + g_cur_mod = m_old_id; + g_cur_task_pos = m_old_pos; +} + +module_id get_current_module() { return *g_cur_mod; } +pos_info get_current_task_pos() { return *g_cur_task_pos; } + } diff --git a/src/util/task_queue.h b/src/util/task_queue.h index db95d22e4c..21b80ed2ff 100644 --- a/src/util/task_queue.h +++ b/src/util/task_queue.h @@ -9,6 +9,7 @@ Author: Gabriel Ebner #include #include #include +#include #include "util/thread.h" #include "util/optional.h" #include "util/rc.h" @@ -103,7 +104,24 @@ struct task_priority { } }; +typedef std::string module_id; +enum class task_kind { parse, elab, print }; + +module_id get_current_module(); +pos_info get_current_task_pos(); +class scoped_task_context { + module_id * m_old_id; + pos_info * m_old_pos; + module_id m_id; + pos_info m_pos; + +public: + scoped_task_context(module_id const & mod, pos_info const & pos); + ~scoped_task_context(); +}; + class generic_task { + template friend class task; friend class task_queue; friend class st_task_queue; friend class mt_task_queue; @@ -112,24 +130,34 @@ class generic_task { std::vector m_reverse_deps; condition_variable m_has_finished; + // metadata + message_bucket_id m_bucket; + module_id m_mod; + pos_info m_pos; + public: + generic_task(); virtual ~generic_task() {} + virtual void description(std::ostream &) const = 0; std::string description() const; virtual std::vector get_dependencies() { return {}; } - virtual void set_result(generic_task_result const & self); - virtual bool is_tiny() const { return false; } + virtual task_kind get_kind() const { return task_kind::elab; } + virtual pos_info get_pos() const { return get_task_pos(); } + + message_bucket_id const & get_bucket() const { return m_bucket; } + period get_version() const { return m_bucket.m_version; } + module_id const & get_module_id() const { return m_mod; } + pos_info const & get_task_pos() const { return m_pos; } }; template class task : public generic_task { public: typedef T result; - virtual ~task() {} - virtual T execute() = 0; }; @@ -211,7 +239,6 @@ public: task_result task( new task_result_cell( new T(std::forward(args)...))); - task->m_task->set_result(task); submit(task); return task; } @@ -233,6 +260,7 @@ public: virtual void wait(generic_task_result const & t) = 0; virtual void cancel(generic_task_result const & t) = 0; + virtual void cancel_if(std::function const & pred) = 0; // NOLINT using progress_cb = std::function; // NOLINT // disabling lint because it this this is cast ^^^