From 8d4f7bb8eceab4c40c42e4c24ed90dace2873c35 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 20 Sep 2018 12:04:08 -0700 Subject: [PATCH] feat(util/timeit): add simpler type for threshold --- src/library/compiler/preprocess.cpp | 3 ++- src/util/timeit.h | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index ff1f79edec..34a1f64787 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/timeit.h" #include "kernel/declaration.h" #include "kernel/replace_fn.h" #include "kernel/instantiate.h" @@ -235,9 +236,9 @@ class preprocess_fn { void exec_new_compiler(constant_info const & d) { name n = get_real_name(d.get_name()); + // timeit timer(std::cout, (sstream() << "compiling " << n).str().c_str(), 0.05); expr v = unfold_aux_match(m_env, d.get_value()); expr v1 = to_lcnf(m_env, local_ctx(), v); - // std::cout << "compiling " << n << "\n"; lean_trace(name({"compiler", "lcnf"}), tout() << n << "\n" << v1 << "\n";); lean_cond_assert("compiler", check(d, v1)); expr v2 = csimp(m_env, local_ctx(), v1); diff --git a/src/util/timeit.h b/src/util/timeit.h index 5b73cf0aa1..584a026e02 100644 --- a/src/util/timeit.h +++ b/src/util/timeit.h @@ -30,6 +30,8 @@ public: m_threshold(threshold), m_out(out), m_msg(msg) { m_start = std::chrono::steady_clock::now(); } + timeit(std::ostream & out, char const * msg, double threshold): + timeit(out, msg, second_duration(threshold)) {} timeit(std::ostream & out, char const * msg) : timeit(out, msg, second_duration(0)) {} ~timeit() { auto end = std::chrono::steady_clock::now();