max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(util/timeit): add simpler type for threshold

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-20 12:04:08 -07:00
parent 0ff1f16bf0
commit 8d4f7bb8ec
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/compiler/preprocess.cpp
View file

@ -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);

2
src/util/timeit.h
View file

@ -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();