michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): suppress profiling information for declarations that take less than 0.01 secs to be processed

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 10:48:36 -08:00
parent 0acdcd487b
commit cbc3c0cf4f
2 changed files with 16 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/decl_cmds.cpp
View file

@ -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<expr>(), clear_pre_info);
} else {
return m_p.elaborate_type(e, list<expr>(), 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);

13
src/util/timeit.h
View file

@ -11,20 +11,23 @@ Author: Leonardo de Moura
#include <iomanip>
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<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC) << " secs\n";
double result = ((static_cast<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC);
if (result > m_threshold) {
m_out << m_msg << " " << std::fixed << std::setprecision(5) << result << " secs\n";
}
}
};
}