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

feat(util/log_tree): annotate nodes with detail levels

Browse source
This commit is contained in:
Gabriel Ebner 2017-03-17 16:08:44 +01:00
parent ef0e113b4b
commit c7ca21625c
12 changed files with 46 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/definition_cmds.cpp
View file

@ -760,7 +760,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
return elaborate_proof(decl_env, opts, header_pos, new_params_list,
new_fn, val, thm_finfo, is_rfl, type,
mctx, lctx, pos_provider, use_info_manager, file_name);
}));
}), log_tree::ElaborationLevel);
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, modifiers, attrs,
doc_string, header_pos);
} else if (kind == Example) {
@ -777,7 +777,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
check_example(env, opts, modifiers, lp_name_list, new_params_list, fn, val, mctx, lctx,
pos_provider, use_info_manager, file_name);
return unit();
});
}, log_tree::ElaborationLevel);
return p.env();
} else {
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);

2
src/frontends/lean/parser.cpp
View file

@ -2260,7 +2260,7 @@ void parser::process_imports() {
report_message(message(fn, pos, WARNING,
(sstream() << "imported file '" << mod_name << "' uses sorry").str()));
return unit {};
}));
}), log_tree::CrossModuleLintLevel);
return mod;
};

11
src/library/library_task_builder.h
View file

@ -26,8 +26,9 @@ struct exception_reporter {
};
template <class Res>
task<Res> add_library_task(task_builder<Res> && builder, std::string const & description, bool add_producer = true) {
auto lt = logtree().mk_child({}, description, logtree().get_location());
task<Res> add_library_task(task_builder<Res> && builder, std::string const & description,
bool add_producer = true, log_tree::detail_level lvl = log_tree::DefaultLevel) {
auto lt = logtree().mk_child({}, description, logtree().get_location(), lvl);
auto task = builder.wrap(library_scopes(lt)).build();
if (add_producer) lt.set_producer(task);
return task;
@ -39,8 +40,10 @@ task<Res> mk_library_task(task_builder<Res> && builder, std::string const & desc
}
template <class Res>
task<Res> add_library_task(task_builder<Res> && builder, bool add_producer = true) {
return add_library_task(std::forward<task_builder<Res>>(builder), {}, add_producer);
task<Res> add_library_task(task_builder<Res> && builder,
log_tree::detail_level lvl = log_tree::DefaultLevel,
bool add_producer = true) {
return add_library_task(std::forward<task_builder<Res>>(builder), {}, add_producer, lvl);
}
}

2
src/library/module_mgr.cpp
View file

@ -155,7 +155,7 @@ void module_mgr::build_module(module_id const & id, bool can_use_olean, name_set
if (!existing_mod->m_out_of_date) return;
scope_global_ios scope_ios(m_ios);
scope_log_tree lt(m_lt.mk_child(id, {}, { id, {{1, 0}, {static_cast<unsigned>(-1), 0}} }, true));
scope_log_tree lt(m_lt.mk_child(id, {}, { id, {{1, 0}, {static_cast<unsigned>(-1), 0}} }, log_tree::DefaultLevel, true));
scope_traces_as_messages scope_trace_msgs(id, {1, 0});
try {

2
src/library/mt_task_queue.h
View file

@ -74,7 +74,7 @@ public:
void wait_for_finish(gtask const & t) override;
void fail_and_dispose(gtask const &t) override;
void submit(gtask const & t, unsigned prio);
void submit(gtask const & t, unsigned prio) override;
void submit(gtask const & t) override;
void evacuate() override;

2
src/shell/lean_js.cpp
View file

@ -33,7 +33,7 @@ public:
int process_request(std::string msg) {
scope_global_ios scoped_ios(m_ios);
scope_log_tree lt(m_server.get_log_tree().get_root().mk_child("_server", {}, {}, true));
scope_log_tree lt(m_server.get_log_tree().get_root().mk_child("_server", {}, {}, log_tree::DefaultLevel, true));
try {
m_server.handle_request(json::parse(msg));
return 0;

11
src/shell/server.cpp
View file

@ -52,6 +52,7 @@ struct all_messages_msg {
bool region_of_interest::intersects(log_tree::node const & n) const {
if (!m_enabled) return true;
if (n.get_detail_level() > m_max_level) return false;
if (n.get_location().m_file_name.empty()) return true;
auto & l = n.get_location();
if (auto f = m_files.find(l.m_file_name)) {
@ -193,9 +194,8 @@ public:
}
void submit_core(log_tree::node const & n) {
// TODO(gabriel): priorities
if (auto prod = n.get_producer()) {
taskq().submit(prod);
taskq().submit(prod, n.get_detail_level());
}
}
@ -351,7 +351,14 @@ struct unrelated_error_msg {
}
};
server * g_server = nullptr;
void server_dump_log_tree() { g_server->dump_log_tree(); }
void server::dump_log_tree() { m_lt.print_to(std::cerr); }
void server::run() {
flet<server *> _(g_server, this);
scope_global_ios scoped_ios(m_ios);
/* Leo: we use std::setlocale to make sure decimal period is displayed as ".".

4
src/shell/server.h
View file

@ -32,6 +32,7 @@ struct string_cmp {
struct region_of_interest {
bool m_enabled = false;
log_tree::detail_level m_max_level = log_tree::CrossModuleLintLevel-1;
rb_map<std::string, line_range, string_cmp> m_files;
bool intersects(log_tree::node const & n) const;
@ -96,6 +97,9 @@ public:
log_tree & get_log_tree() { return m_lt; }
region_of_interest get_roi();
// debugging
void dump_log_tree();
};
void initialize_server();

6
src/util/log_tree.cpp
View file

@ -99,7 +99,7 @@ void log_tree::node::add(log_entry const & entry) const {
}
log_tree::node log_tree::node::mk_child(name n, std::string const & description, location const & loc,
bool overwrite) {
detail_level lvl, bool overwrite) {
auto l = lock();
std::vector<event> events;
@ -123,6 +123,7 @@ log_tree::node log_tree::node::mk_child(name n, std::string const & description,
child.m_ptr->m_tree = m_ptr->m_tree;
child.m_ptr->m_detached = m_ptr->m_detached;
}
child.m_ptr->m_detail_level = std::max(m_ptr->m_detail_level, lvl);
child.m_ptr->m_description = description;
child.m_ptr->m_location = loc;
m_ptr->m_children.insert(n, child);
@ -217,7 +218,8 @@ void log_tree::node::print_to(std::ostream & out, unsigned indent) const {
<< ": " << begin.first << ":" << begin.second << " -- " << end.first << ":" << end.second << ": "
<< m_ptr->m_description << " ("
<< m_ptr->m_entries.size()
<< " entries, producer = "
<< " entries, detail level = "
<< m_ptr->m_detail_level << ", producer = "
<< std::hex << reinterpret_cast<uintptr_t>(m_ptr->m_producer.get()) << std::dec
<< ")" << std::endl;

12
src/util/log_tree.h
View file

@ -31,6 +31,13 @@ public:
struct event;
using listener = std::function<void(std::vector<event> const &)>;
using detail_level = unsigned;
constexpr static detail_level
DefaultLevel = 100,
ElaborationLevel = 200,
CrossModuleLintLevel = 1000,
MaxLevel = std::numeric_limits<detail_level>::max();
struct node_cell {
MK_LEAN_RC()
void dealloc() { delete this; }
@ -46,6 +53,7 @@ public:
location m_location;
std::string m_description;
gtask m_producer;
detail_level m_detail_level = DefaultLevel;
node_cell() : m_rc(0) {}
};
@ -82,12 +90,14 @@ public:
name_map<node> get_used_children() const;
void remove_child(name const &) const;
node mk_child(name n, std::string const & description, location const & loc, bool overwrite = false);
node mk_child(name n, std::string const & description, location const & loc,
detail_level lvl = DefaultLevel, bool overwrite = false);
void reuse(name const & n) const;
void finish() const;
void set_producer(gtask const &);
detail_level get_detail_level() const { return m_ptr->m_detail_level; }
location const & get_location() const { return m_ptr->m_location; }
std::string const & get_description() const { return m_ptr->m_description; }
name_set get_used_names() const;

4
src/util/task.cpp
View file

@ -69,6 +69,10 @@ void task_queue::fail(gtask const & t, gtask const & failed) {
fail(t, failed->m_exception);
}
void task_queue::submit(gtask const & t, unsigned) {
return submit(t);
}
static task_queue * g_taskq = nullptr;
void set_task_queue(task_queue * q) {

1
src/util/task.h
View file

@ -145,6 +145,7 @@ public:
virtual void join() = 0;
virtual void submit(gtask const &) = 0;
virtual void submit(gtask const &, unsigned prio);
};
void set_task_queue(task_queue *); // NOLINT