From cbc3c0cf4f55370975423e99695abcaea6ed0394 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Dec 2015 10:48:36 -0800 Subject: [PATCH] feat(frontends/lean): suppress profiling information for declarations that take less than 0.01 secs to be processed --- src/frontends/lean/decl_cmds.cpp | 11 ++++++++--- src/util/timeit.h | 13 ++++++++----- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 67815078a..656c7e043 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -30,6 +30,11 @@ Author: Leonardo de Moura #include "frontends/lean/update_environment_exception.h" #include "frontends/lean/nested_declaration.h" +// We don't display profiling information for declarations that take less than 0.01 secs +#ifndef LEAN_PROFILE_THRESHOLD +#define LEAN_PROFILE_THRESHOLD 0.01 +#endif + namespace lean { static environment declare_universe(parser & p, environment env, name const & n, bool local) { if (local) { @@ -799,7 +804,7 @@ class definition_cmd_fn { std::ostringstream msg; display_pos(msg); msg << " type checking time for " << m_name; - timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str()); + timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD); return ::lean::check(m_env, d); } else { return ::lean::check(m_env, d); @@ -955,7 +960,7 @@ class definition_cmd_fn { std::ostringstream msg; display_pos(msg); msg << " type elaboration time for " << m_name; - timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str()); + timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD); return m_p.elaborate_type(e, list(), clear_pre_info); } else { return m_p.elaborate_type(e, list(), clear_pre_info); @@ -968,7 +973,7 @@ class definition_cmd_fn { std::ostringstream msg; display_pos(msg); msg << " elaboration time for " << m_name; - timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str()); + timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD); return m_p.elaborate_definition(def_name, type, value); } else { return m_p.elaborate_definition(def_name, type, value); diff --git a/src/util/timeit.h b/src/util/timeit.h index 2cb88fd6f..8829a0a5c 100644 --- a/src/util/timeit.h +++ b/src/util/timeit.h @@ -11,20 +11,23 @@ Author: Leonardo de Moura #include namespace lean { -/** - \brief Low tech timer for used for testing. -*/ +/** \brief Low tech timer for used for testing. */ class timeit { std::ostream & m_out; std::string m_msg; + double m_threshold; // we only display the result if time > m_threshold clock_t m_start; public: - timeit(std::ostream & out, char const * msg):m_out(out), m_msg(msg) { + timeit(std::ostream & out, char const * msg, double threshold):m_out(out), m_msg(msg), m_threshold(threshold) { m_start = clock(); } + timeit(std::ostream & out, char const * msg):timeit(out, msg, -0.1) {} ~timeit() { clock_t end = clock(); - m_out << m_msg << " " << std::fixed << std::setprecision(5) << ((static_cast(end) - static_cast(m_start)) / CLOCKS_PER_SEC) << " secs\n"; + double result = ((static_cast(end) - static_cast(m_start)) / CLOCKS_PER_SEC); + if (result > m_threshold) { + m_out << m_msg << " " << std::fixed << std::setprecision(5) << result << " secs\n"; + } } }; }