From 33679a11b9efd3ac660f30fa38540a631e96aa8a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 27 Jun 2017 18:48:25 +0200 Subject: [PATCH] feat(shell/lean,util/log_tree): show currently executing task in lean --make @dselsam @johoelzl This should make it easier to diagnose which proofs time out or take a very long time. --- src/frontends/lean/module_parser.cpp | 4 +- src/library/library_task_builder.cpp | 7 ++- src/shell/lean.cpp | 67 ++++++++++++++++------------ src/shell/server.cpp | 2 +- src/util/log_tree.cpp | 22 ++++++++- src/util/log_tree.h | 7 ++- 6 files changed, 75 insertions(+), 34 deletions(-) diff --git a/src/frontends/lean/module_parser.cpp b/src/frontends/lean/module_parser.cpp index 8b099351f7..428db1300f 100644 --- a/src/frontends/lean/module_parser.cpp +++ b/src/frontends/lean/module_parser.cpp @@ -109,7 +109,9 @@ module_parser::parse_next_command_like(optional> const & depe auto ctok = mk_cancellation_token(global_cancellation_token()); scope_cancellation_token scope_ctok(&ctok); auto lt = logtree().mk_child( - "_next", "parsing", {m_parser.m_file_name, {begin_pos, m_end_pos}}, + "_next", + (sstream() << "parsing at line " << begin_pos.first).str(), + {m_parser.m_file_name, {begin_pos, m_end_pos}}, log_tree::DefaultLevel, true); if (dependencies || m_separate_tasks) { auto task = task_builder(std::move(fn)) diff --git a/src/library/library_task_builder.cpp b/src/library/library_task_builder.cpp index 164403dc90..1739d1293d 100644 --- a/src/library/library_task_builder.cpp +++ b/src/library/library_task_builder.cpp @@ -22,7 +22,12 @@ struct library_scopes_imp : public delegating_task_imp { void execute(void * result) override { scope_global_ios scope1(m_ios); scope_log_tree scope2(m_lt); - delegating_task_imp::execute(result); + if (m_lt) m_lt.set_state(log_tree::state::Running); + try { + delegating_task_imp::execute(result); + } catch (interrupted) { + m_lt.set_state(log_tree::state::Cancelled); + } } }; diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index c21fd5e467..54c492e69c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -228,6 +228,7 @@ class progress_message_stream { bool m_showing_task = false; std::ostream & m_out; bool m_use_json; + log_tree::node m_lt; bool m_show_progress; std::unique_ptr m_timer; @@ -240,8 +241,8 @@ class progress_message_stream { } public: - progress_message_stream(std::ostream & out, bool use_json, bool show_progress) : - m_out(out), m_use_json(use_json), m_show_progress(show_progress) { + progress_message_stream(std::ostream & out, bool use_json, bool show_progress, log_tree::node const & lt) : + m_out(out), m_use_json(use_json), m_lt(lt), m_show_progress(show_progress) { #if defined(LEAN_MULTI_THREAD) if (show_progress) { m_timer.reset(new single_timer); @@ -255,7 +256,7 @@ public: } void on_event(std::vector const & events) { - log_tree::event const * cur_task = nullptr; + bool refresh_task = false; for (auto & e : events) { switch (e.m_kind) { case log_tree::event::EntryAdded: @@ -275,43 +276,52 @@ public: case log_tree::event::ProducerSet: taskq().submit(e.m_node.get_producer()); break; - case log_tree::event::Finished: - if (e.m_node.get_description().size()) - cur_task = &e; + case log_tree::event::StateChanged: + refresh_task = true; break; } } - if (m_show_progress && cur_task) { - std::ostringstream fmt; - fmt << cur_task->m_node.get_location().m_file_name << ": " << cur_task->m_node.get_description(); - auto fmt_str = fmt.str(); + if (m_show_progress && refresh_task) { #if defined(LEAN_MULTI_THREAD) - if (m_timer) { - m_timer->set(chrono::steady_clock::now() + chrono::milliseconds(100), - [=] { show_current_task(fmt_str); }, false); - } else { - unique_lock lock(m_mutex); - show_current_task_core(fmt_str); - } + lean_assert(m_timer); + m_timer->set(chrono::steady_clock::now() + chrono::milliseconds(100), + [=] { show_current_task(); }, false); #else - show_current_task_core(fmt_str); + show_current_task_core(); #endif } } - void show_current_task(std::string const & desc) { - unique_lock lock(m_mutex); - show_current_task_core(desc); + optional find_current_task() { + optional found_running; + m_lt.for_each([&] (log_tree::node const & lt) { + if (!found_running) { + if (lt.get_state() == log_tree::state::Running) { + std::ostringstream fmt; + fmt << lt.get_location().m_file_name << ": " << lt.get_description(); + found_running = fmt.str(); + } + } + return !found_running; + }); + return found_running; } - void show_current_task_core(std::string const & desc) { + + void show_current_task() { + unique_lock lock(m_mutex); + show_current_task_core(); + } + void show_current_task_core() { if (m_use_json) return; - clear_shown_task(); + if (auto desc = find_current_task()) { + clear_shown_task(); #if defined(LEAN_EMSCRIPTEN) - m_out << desc << std::endl; + m_out << *desc << std::endl; #else - m_out << desc << std::flush; - m_showing_task = true; + m_out << *desc << std::flush; + m_showing_task = true; #endif + } } }; @@ -510,10 +520,11 @@ int main(int argc, char ** argv) { } #endif - progress_message_stream msg_stream(std::cout, json_output, make_mode); + log_tree lt; + + progress_message_stream msg_stream(std::cout, json_output, make_mode, lt.get_root()); if (json_output) ios.set_regular_channel(ios.get_diagnostic_channel_ptr()); - log_tree lt; if (!test_suite) lt.add_listener([&] (std::vector const & evs) { msg_stream.on_event(evs); }); auto lt_root = lt.get_root(); diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 1e6d7fcbd4..efa91b9d8d 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -270,7 +270,7 @@ public: need_refresh = true; } break; - case log_tree::event::Finished: + case log_tree::event::StateChanged: if (!roi) roi = m_srv->get_roi(); if (roi->get_priority(e.m_node)) need_refresh = true; diff --git a/src/util/log_tree.cpp b/src/util/log_tree.cpp index 959425c2f1..d783629caa 100644 --- a/src/util/log_tree.cpp +++ b/src/util/log_tree.cpp @@ -60,7 +60,7 @@ void log_tree::node::detach_core(std::vector & events) const { m_ptr->m_detached = true; m_ptr->m_children.for_each([&] (name const &, node const & c) { c.detach_core(events); }); for (auto & e : m_ptr->m_entries) events.push_back({ event::EntryRemoved, m_ptr, e }); - if (m_ptr->m_producer) events.push_back({event::Finished, m_ptr, {}}); + if (m_ptr->m_producer) events.push_back({event::StateChanged, m_ptr, {}}); m_ptr->m_producer = nullptr; } @@ -133,6 +133,21 @@ log_tree::node log_tree::node::mk_child(name n, std::string const & description, return child; } +log_tree::state log_tree::node::get_state() const { + auto l = lock(); + return m_ptr->m_state; +} + +void log_tree::node::set_state(state s, bool ignore_illegal_trans) { + auto l = lock(); + if (s >= m_ptr->m_state) { + m_ptr->m_state = s; + notify({{event::StateChanged, *this, {}}}, l); + } else { + lean_always_assert(ignore_illegal_trans); + } +} + void log_tree::node::set_producer(gtask const & prod) { auto l = lock(); if (m_ptr->m_detached) return; @@ -142,8 +157,11 @@ void log_tree::node::set_producer(gtask const & prod) { void log_tree::node::finish() const { auto l = lock(); + lean_always_assert(m_ptr->m_state < state::Finished); + std::vector events; m_ptr->m_producer.reset(); + m_ptr->m_state = state::Finished; buffer> to_delete; m_ptr->m_children.for_each([&] (name const & n, node const & c) { @@ -156,7 +174,7 @@ void log_tree::node::finish() const { c.second.detach_core(events); } - events.push_back({event::Finished, *this, {}}); + events.push_back({event::StateChanged, *this, {}}); notify(events, l); } diff --git a/src/util/log_tree.h b/src/util/log_tree.h index 0dda9dd558..b1e511935a 100644 --- a/src/util/log_tree.h +++ b/src/util/log_tree.h @@ -32,6 +32,8 @@ public: struct event; using listener = std::function const &)>; + enum class state { Created, Running, Cancelled, Finished }; + using detail_level = unsigned; constexpr static detail_level DefaultLevel = 100, @@ -55,6 +57,7 @@ public: std::string m_description; gtask m_producer; detail_level m_detail_level = DefaultLevel; + state m_state = state::Created; node_cell() : m_rc(0) {} }; @@ -98,6 +101,8 @@ public: void finish() const; void set_producer(gtask const &); + void set_state(state, bool ignore_illegal_transition = false); + state get_state() const; detail_level get_detail_level() const { return m_ptr->m_detail_level; } location const & get_location() const { return m_ptr->m_location; } std::string const & get_description() const { return m_ptr->m_description; } @@ -119,7 +124,7 @@ public: }; struct event { - enum { ProducerSet, EntryAdded, EntryRemoved, Finished } m_kind; + enum { ProducerSet, EntryAdded, EntryRemoved, StateChanged } m_kind; node m_node; log_entry m_entry; };