From 1cb34604cd963bfa108bb9644da5901376e3ed45 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 11 Jan 2021 11:51:41 +0100 Subject: [PATCH] chore: remove ios & message from tracing --- src/library/trace.cpp | 93 ++----------------------------------------- src/library/trace.h | 69 +------------------------------- 2 files changed, 5 insertions(+), 157 deletions(-) diff --git a/src/library/trace.cpp b/src/library/trace.cpp index 8bbcf9399e..5da82a13b6 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp @@ -11,14 +11,11 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/local_ctx.h" #include "library/abstract_type_context.h" -#include "library/io_state.h" #include "library/trace.h" -#include "library/messages.h" namespace lean { static name_set * g_trace_classes = nullptr; static name_map * g_trace_aliases = nullptr; -static name * g_trace_as_messages = nullptr; MK_THREAD_LOCAL_GET_DEF(std::vector, get_enabled_trace_classes); MK_THREAD_LOCAL_GET_DEF(std::vector, get_disabled_trace_classes); MK_THREAD_LOCAL_GET_DEF(environment, get_dummy_env); @@ -27,7 +24,6 @@ LEAN_THREAD_VALUE(bool, g_silent, false); LEAN_THREAD_PTR(environment, g_env); LEAN_THREAD_PTR(options, g_opts); LEAN_THREAD_PTR(abstract_type_context, g_ctx); -LEAN_THREAD_VALUE(unsigned, g_depth, 0); void register_trace_class(name const & n) { register_option(name("trace") + n, data_value_kind::Bool, "false", @@ -142,68 +138,11 @@ scope_trace_env::~scope_trace_env() { get_disabled_trace_classes().resize(m_disable_sz); } -void scope_trace_inc_depth::activate() { - lean_assert(!m_active); - m_active = true; - g_depth++; +std::ostream & tout() { + return std::cerr; } -scope_trace_inc_depth::~scope_trace_inc_depth() { - if (m_active) - g_depth--; -} - -void scope_trace_init_bool_option::init(name const & n, bool v) { - m_initialized = true; - m_old_opts = g_opts; - if (g_opts) - m_opts = *g_opts; - m_opts = m_opts.update_if_undef(n, v); - g_opts = &m_opts; -} - -scope_trace_init_bool_option::~scope_trace_init_bool_option() { - if (m_initialized) { - g_opts = m_old_opts; - } -} - -struct silent_ios_helper { - std::shared_ptr m_out; - io_state m_ios; - silent_ios_helper(): - m_out(new null_output_channel()), - m_ios(get_dummy_ios(), m_out, m_out) {} -}; - -MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper); -MK_THREAD_LOCAL_GET_DEF(abstract_type_context, get_dummy_tc); - -scope_trace_silent::scope_trace_silent(bool flag) { - m_old_value = g_silent; - g_silent = flag; -} - -scope_trace_silent::~scope_trace_silent() { - g_silent = m_old_value; -} - -io_state_stream tout() { - if (g_env && !g_silent) { - options opts = g_opts ? *g_opts : get_dummy_options(); - io_state ios(get_global_ios(), opts); - return diagnostic(*g_env, ios, *g_ctx); - } else { - return diagnostic(get_dummy_env(), get_silent_ios_helper().m_ios, get_dummy_tc()); - } -} - -io_state_stream const & operator<<(io_state_stream const & ios, tdepth const &) { - ios << g_depth << ". "; - return ios; -} - -io_state_stream const & operator<<(io_state_stream const & ios, tclass const & c) { +std::ostream & operator<<(std::ostream & ios, tclass const & c) { ios << "[" << c.m_cls << "] "; return ios; } @@ -211,8 +150,6 @@ io_state_stream const & operator<<(io_state_stream const & ios, tclass const & c void initialize_trace() { g_trace_classes = new name_set(); g_trace_aliases = new name_map(); - g_trace_as_messages = new name {"trace", "as_messages"}; - mark_persistent(g_trace_as_messages->raw()); register_trace_class(name{"debug"}); } @@ -220,30 +157,6 @@ void initialize_trace() { void finalize_trace() { delete g_trace_classes; delete g_trace_aliases; - delete g_trace_as_messages; -} - -scope_traces_as_messages::scope_traces_as_messages(std::string const & stream_name, pos_info const & pos) : - m_stream_name(stream_name), m_pos(pos) { - if (get_global_ios().get_options().get_bool(*g_trace_as_messages, false)) { - m_redirected_ios = std::unique_ptr(new io_state(get_global_ios())); - m_buffer = std::make_shared(); - m_redirected_ios->set_regular_channel(m_buffer); - m_redirected_ios->set_diagnostic_channel(m_buffer); - m_scoped_ios = std::unique_ptr(new scope_global_ios(*m_redirected_ios)); - } -} - -scope_traces_as_messages::~scope_traces_as_messages() { - if (enabled()) { - auto msg = m_buffer->str(); - if (!msg.empty()) { - auto redirected_output = m_buffer->str(); - if (!redirected_output.empty()) - report_message(message( - m_stream_name, m_pos, INFORMATION, "trace output", redirected_output)); - } - } } scope_traces_as_string::scope_traces_as_string() { diff --git a/src/library/trace.h b/src/library/trace.h index bd8394e52e..9ce2f2c069 100644 --- a/src/library/trace.h +++ b/src/library/trace.h @@ -31,19 +31,6 @@ public: ~scope_trace_env(); }; -class scope_traces_as_messages { - std::string m_stream_name; - pos_info m_pos; - std::unique_ptr m_redirected_ios; - std::unique_ptr m_scoped_ios; - std::shared_ptr m_buffer; - -public: - scope_traces_as_messages(std::string const & stream_name, pos_info const & pos); - ~scope_traces_as_messages(); - bool enabled() const { return static_cast(m_scoped_ios); } -}; - class scope_traces_as_string { std::unique_ptr m_redirected_ios; std::unique_ptr m_scoped_ios; @@ -54,68 +41,16 @@ public: std::string get_string() const { return m_buffer->str(); } }; -class scope_trace_inc_depth { - bool m_active{false}; -public: - ~scope_trace_inc_depth(); - void activate(); -}; - -#define LEAN_MERGE_(a, b) a##b -#define LEAN_LABEL_(a) LEAN_MERGE_(unique_name_, a) -#define LEAN_UNIQUE_NAME LEAN_LABEL_(__LINE__) - -#define lean_trace_inc_depth(CName) \ -scope_trace_inc_depth LEAN_UNIQUE_NAME; \ -if (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(name(CName))) \ - LEAN_UNIQUE_NAME.activate(); - -/* Temporarily set an option if it is not already set in the trace environment. */ -class scope_trace_init_bool_option { - bool m_initialized{false}; - options m_opts; - options * m_old_opts; -public: - ~scope_trace_init_bool_option(); - void init(name const & opt, bool val); -}; - -#define lean_trace_init_bool(CName, Opt, Val) \ - scope_trace_init_bool_option LEAN_UNIQUE_NAME; \ -if (lean_is_trace_enabled(CName)) { \ - LEAN_UNIQUE_NAME.init(Opt, Val); \ -} - -/* Helper object for temporarily silencing trace messages */ -class scope_trace_silent { - bool m_old_value; -public: - scope_trace_silent(bool flag); - ~scope_trace_silent(); -}; - -struct tdepth {}; struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} }; -io_state_stream tout(); -io_state_stream const & operator<<(io_state_stream const & ios, tdepth const &); -io_state_stream const & operator<<(io_state_stream const & ios, tclass const &); - -#define lean_trace_plain(CName, CODE) { \ -if (lean_is_trace_enabled(CName)) { \ - CODE \ -}} +std::ostream & tout(); +std::ostream & operator<<(std::ostream & ios, tclass const &); #define lean_trace(CName, CODE) { \ if (lean_is_trace_enabled(CName)) { \ tout() << tclass(CName); CODE \ }} -#define lean_trace_d(CName, CODE) { \ -if (lean_is_trace_enabled(CName)) { \ - tout() << tdepth() << tclass(CName); CODE \ -}} - void trace_expr(environment const & env, options const & opts, expr const & e); std::string trace_pp_expr(expr const & e);