From 3eba8d3ffc2f0ae724e21ba574bc67e6ba126937 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 24 Feb 2017 14:48:22 +0100 Subject: [PATCH] refactor(util/task): do not propagate errors --- src/frontends/lean/definition_cmds.cpp | 10 ++-- src/library/library_task_builder.cpp | 22 +++++++ src/library/library_task_builder.h | 4 ++ src/library/module.cpp | 15 ++++- src/library/mt_task_queue.cpp | 79 ++++++++------------------ src/library/mt_task_queue.h | 1 - src/library/vm/vm_task.cpp | 2 +- src/shell/server.cpp | 6 +- src/util/log_tree.cpp | 20 ++++++- src/util/task.cpp | 14 +++-- src/util/task.h | 2 +- src/util/task_builder.h | 6 -- 12 files changed, 100 insertions(+), 81 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 2d58a8f286..e6833c3ad8 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -615,8 +615,8 @@ static expr elaborate_proof( auto_reporting_info_manager_scope scope4(file_name, use_info_manager); try { - bool recover_froerrors = true; - elaborator elab(decl_env, opts, local_pp_name(fn), mctx, lctx, recover_froerrors); + bool recover_from_errors = true; + elaborator elab(decl_env, opts, local_pp_name(fn), mctx, lctx, recover_from_errors); expr val, type; // TODO(Leo): create an aux function for retrieving this info @@ -648,7 +648,7 @@ static expr elaborate_proof( ERROR); error_msg.set_exception(ex); error_msg.report(); - throw ex; + return mk_sorry(final_type); } } @@ -668,8 +668,8 @@ static void check_example(environment const & decl_env, options const & opts, name decl_name = "_example"; try { - bool recover_froerrors = true; - elaborator elab(decl_env, opts, decl_name, mctx, lctx, recover_froerrors); + bool recover_from_errors = true; + elaborator elab(decl_env, opts, decl_name, mctx, lctx, recover_from_errors); expr val, type; std::tie(val, type) = elab.elaborate_with_type(val0, mlocal_type(fn)); diff --git a/src/library/library_task_builder.cpp b/src/library/library_task_builder.cpp index 9e42ecf287..b132b9f29a 100644 --- a/src/library/library_task_builder.cpp +++ b/src/library/library_task_builder.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #include "library/library_task_builder.h" +#include "library/message_builder.h" namespace lean { @@ -30,4 +31,25 @@ std::unique_ptr library_scopes::operator()(std::unique_ptr std::forward>(base), m_lt)); } +struct exception_reporter_imp : public delegating_task_imp { + exception_reporter_imp(std::unique_ptr && base) : + delegating_task_imp(std::forward>(base)) {} + + void execute(void * result) override { + try { + delegating_task_imp::execute(result); + } catch (std::exception & ex) { + report_message(message(logtree().get_location().m_file_name, + logtree().get_location().m_range.m_begin, + ERROR, ex.what())); + throw; + } + } +}; + +std::unique_ptr exception_reporter::operator()(std::unique_ptr && base) { + return std::unique_ptr(new exception_reporter_imp( + std::forward>(base))); +} + } \ No newline at end of file diff --git a/src/library/library_task_builder.h b/src/library/library_task_builder.h index 7d57fe9dcf..5e1fb7ee03 100644 --- a/src/library/library_task_builder.h +++ b/src/library/library_task_builder.h @@ -20,6 +20,10 @@ struct library_scopes { std::unique_ptr operator()(std::unique_ptr &&); }; +struct exception_reporter { + std::unique_ptr operator()(std::unique_ptr &&); +}; + template task add_library_task(task_builder && builder, std::string const & description, bool add_producer = true) { auto lt = logtree().mk_child({}, description, logtree().get_location()); diff --git a/src/library/module.cpp b/src/library/module.cpp index cd2af8ff16..2cf6f2e91a 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -413,16 +413,25 @@ environment add(environment const & env, certified_declaration const & d) { new_env = mark_noncomputable(new_env, _d.get_name()); new_env = update_module_defs(new_env, _d); new_env = add(new_env, std::make_shared(_d, env.trust_lvl())); - pos_info pos { g_curr_line, g_curr_column }; - add_library_task(task_builder([_d, pos] { + + if (_d.is_theorem()) { + // report errors from kernel type-checker + add_library_task(task_builder([_d] { _d.get_value(); return unit(); }) + .wrap(exception_reporter()) + .depends_on(_d.is_theorem() ? _d.get_value_task() : nullptr)); + } + + add_library_task(task_builder([_d] { if (has_sorry(_d)) { if (optional n = should_report_sorry(_d.get_name())) { - report_message(message(logtree().get_location().m_file_name, pos, WARNING, + report_message(message(logtree().get_location().m_file_name, + logtree().get_location().m_range.m_begin, WARNING, (sstream() << "declaration '" << *n << "' uses sorry").str())); } } return unit {}; }).depends_on(_d.is_theorem() ? _d.get_value_task() : nullptr)); + return add_decl_pos_info(new_env, _d.get_name()); } diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp index 8842d75633..9dcefae96e 100644 --- a/src/library/mt_task_queue.cpp +++ b/src/library/mt_task_queue.cpp @@ -110,57 +110,34 @@ void mt_task_queue::spawn_worker() { } void mt_task_queue::handle_finished(gtask const & t) { + lean_assert(get_state(t).load() > task_state::Running); + lean_assert(get_data(t)); + lean_assert(get_data(t)->m_sched_info); + + m_waiting.erase(t); get_sched_info(t).m_has_finished.notify_all(); - if (get_state(t).load() == task_state::Success) { - for (auto & rdep : get_sched_info(t).m_reverse_deps) { - switch (get_state(rdep).load()) { - case task_state::Waiting: - if (check_deps(rdep)) { - m_waiting.erase(rdep); - if (get_state(rdep).load() < task_state::Running) { - lean_assert(get_data(rdep)); - if (get_data(rdep)->m_flags.m_needs_execution) { - enqueue(rdep); - } else { - get_state(rdep) = task_state::Success; - handle_finished(rdep); - } + for (auto & rdep : get_sched_info(t).m_reverse_deps) { + switch (get_state(rdep).load()) { + case task_state::Waiting: case task_state::Queued: + if (check_deps(rdep)) { + m_waiting.erase(rdep); + if (get_state(rdep).load() < task_state::Running) { + lean_assert(get_data(rdep)); + if (get_data(rdep)->m_flags.m_needs_execution) { + enqueue(rdep); + } else { + get_state(rdep) = task_state::Success; + handle_finished(rdep); } } - break; - case task_state::Failed: case task_state::Queued: - // TODO(gabriel): why??? - m_waiting.erase(rdep); - break; - default: - lean_unreachable(); - } - } - } else { - propagate_failure(t); - } - - clear(t); -} - -void mt_task_queue::propagate_failure(gtask const & t) { - lean_assert(get_state(t).load() == task_state::Failed); - m_waiting.erase(t); - - if (get_data(t) && get_data(t)->m_sched_info) { - get_sched_info(t).m_has_finished.notify_all(); - - for (auto & rdep : get_sched_info(t).m_reverse_deps) { - if (get_data(rdep) && !get_data(rdep)->m_flags.m_propagate_errors_from_dependencies) - continue; - switch (get_state(rdep).load()) { - case task_state::Waiting: case task_state::Queued: - fail(rdep, t); - propagate_failure(rdep); - break; - default: break; - } + } + break; + case task_state::Failed: + // TODO(gabriel): removed failed tasks from reverse dependency lists? + m_waiting.erase(rdep); + break; + default: lean_unreachable(); } } @@ -250,11 +227,6 @@ bool mt_task_queue::check_deps(gtask const & t) { case task_state::Success: break; case task_state::Failed: - if (get_data(t)->m_flags.m_propagate_errors_from_dependencies) { - fail(t, dep); - propagate_failure(t); - return true; - } break; default: lean_unreachable(); } @@ -268,7 +240,6 @@ void mt_task_queue::wait_for_finish(gtask const & t) { submit_core(t, get_default_prio()); while (get_state(t).load() <= task_state::Running) { if (g_current_task) { - // std::cerr << "waiting: " << g_current_task->description() << " -> " << t.description() << std::endl; scoped_add inc_required(m_required_workers, +1); if (m_sleeping_workers == 0) { spawn_worker(); @@ -293,7 +264,7 @@ void mt_task_queue::cancel_core(gtask const & t) { m_waiting.erase(t); case task_state::Created: case task_state::Queued: fail(t, std::make_exception_ptr(cancellation_exception())); - propagate_failure(t); + handle_finished(t); return; default: return; } diff --git a/src/library/mt_task_queue.h b/src/library/mt_task_queue.h index f71918acc1..d691d94257 100644 --- a/src/library/mt_task_queue.h +++ b/src/library/mt_task_queue.h @@ -41,7 +41,6 @@ class mt_task_queue : public task_queue { void enqueue(gtask const &); bool check_deps(gtask const &); - void propagate_failure(gtask const &); void submit_core(gtask const &, unsigned); void bump_prio(gtask const &, unsigned); void cancel_core(gtask const &); diff --git a/src/library/vm/vm_task.cpp b/src/library/vm/vm_task.cpp index b2e1a0b6ec..5e5a623745 100644 --- a/src/library/vm/vm_task.cpp +++ b/src/library/vm/vm_task.cpp @@ -81,7 +81,7 @@ vm_obj vm_task_map(vm_obj const &, vm_obj const &, vm_obj const & fn, vm_obj con vm_state state(env, opts); scope_vm_state scope_vm(state); return ts_vm_obj(state.invoke(ts_fn.to_vm_obj(), arg.to_vm_obj())); - }))); + }).wrap(exception_reporter()))); } vm_obj vm_task_flatten(vm_obj const &, vm_obj const & o) { diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 6cc7d9666f..2a0b5e5dbe 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -502,7 +502,6 @@ void server::handle_complete(cmd_req const & req) { auto complete_gen_task = task_builder([=] { return autocomplete(mod_info, skip_completions, pos); }) .set_cancellation_token(m_bg_task_ctok) -// .wrap(library_scopes()) .build(); taskq().submit(task_builder([this, req, complete_gen_task] { @@ -512,7 +511,7 @@ void server::handle_complete(cmd_req const & req) { send_msg(cmd_res(req.m_seq_num, std::string(ex.what()))); } return unit{}; - }).depends_on(complete_gen_task).ignore_dependency_errors().build()); + }).depends_on(complete_gen_task).build()); } static void get_info_managers(log_tree::node const & n, std::vector & infoms) { @@ -564,7 +563,6 @@ void server::handle_info(server::cmd_req const & req) { mod_info->m_result, [] (buffer & deps, module_info::parse_result const & res) { deps.push_back(res.m_loaded_module->m_env); })).set_cancellation_token(m_bg_task_ctok) -// .wrap(library_scopes()) .build(); taskq().submit(task_builder([this, req, info_gen_task] { @@ -574,7 +572,7 @@ void server::handle_info(server::cmd_req const & req) { send_msg(cmd_res(req.m_seq_num, std::string(ex.what()))); } return unit{}; - }).depends_on(info_gen_task).ignore_dependency_errors().build()); + }).depends_on(info_gen_task).build()); } std::tuple server::load_module(module_id const & id, bool can_use_olean) { diff --git a/src/util/log_tree.cpp b/src/util/log_tree.cpp index b8878c74ca..89674383d0 100644 --- a/src/util/log_tree.cpp +++ b/src/util/log_tree.cpp @@ -167,6 +167,8 @@ void log_tree::node::print() const { } void log_tree::node::print_to(std::ostream & out, unsigned indent) const { + indent += 2; + auto l = lock(); auto begin = m_ptr->m_location.m_range.m_begin, end = m_ptr->m_location.m_range.m_end; out << m_ptr->m_location.m_file_name @@ -177,11 +179,27 @@ void log_tree::node::print_to(std::ostream & out, unsigned indent) const { << std::hex << reinterpret_cast(m_ptr->m_producer.get()) << std::dec << ")" << std::endl; + if (auto prod = m_ptr->m_producer) { + if (auto ex = prod->peek_exception()) { + for (unsigned i = 0; i < indent; i++) out << ' '; + out << "producer threw exception: "; + try { + std::rethrow_exception(ex); + } catch (std::exception & ex) { + out << ex.what(); + } catch (cancellation_exception) { + out << ""; + } catch (...) { + out << ""; + } + out << "\n"; + } + } + auto children = m_ptr->m_children; auto used_names = m_ptr->m_used_names; l.unlock(); - indent += 2; children.for_each([&] (name const & n, log_tree::node const & c) { for (unsigned i = 0; i < indent; i++) out << ' '; out << n; diff --git a/src/util/task.cpp b/src/util/task.cpp index b6e19be653..aaa7a85db0 100644 --- a/src/util/task.cpp +++ b/src/util/task.cpp @@ -19,6 +19,14 @@ void gtask_cell::cancel(std::shared_ptr const & self) { } } +std::exception_ptr gtask_cell::peek_exception() const { + if (m_state.load() == task_state::Failed) { + return m_exception; + } else { + return {}; + } +} + void task_queue::wait_for_success(gtask const & t) { while (true) { switch (t->m_state.load()) { @@ -42,11 +50,7 @@ void task_queue::execute(gtask const & t) { { buffer deps; t->m_data->m_imp->get_dependencies(deps); - if (t->m_data->m_flags.m_propagate_errors_from_dependencies) { - for (auto & dep : deps) if (dep) wait_for_success(dep); - } else { - for (auto & dep : deps) if (dep) wait_for_finish(dep); - } + for (auto & dep : deps) if (dep) wait_for_finish(dep); } t->execute(); diff --git a/src/util/task.h b/src/util/task.h index 1eef5d5066..2b60211ba4 100644 --- a/src/util/task.h +++ b/src/util/task.h @@ -25,7 +25,6 @@ struct scheduling_info { struct task_flags { bool m_do_priority_inversion = true; - bool m_propagate_errors_from_dependencies = true; bool m_needs_separate_thread = true; bool m_needs_execution = true; }; @@ -81,6 +80,7 @@ public: void cancel(std::shared_ptr const & self) override; bool peek_is_finished() const { return m_state.load() > task_state::Running; } + std::exception_ptr peek_exception() const; virtual ~gtask_cell() {} }; diff --git a/src/util/task_builder.h b/src/util/task_builder.h index a536400e83..1ee9cbf920 100644 --- a/src/util/task_builder.h +++ b/src/util/task_builder.h @@ -74,12 +74,6 @@ public: return std::move(*this); } - task_builder ignore_dependency_errors() { - lean_assert(m_imp); - m_flags.m_propagate_errors_from_dependencies = false; - return std::move(*this); - } - task_builder does_not_require_own_thread() { lean_assert(m_imp); m_flags.m_needs_separate_thread = false;