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

chore(library/vm/interaction_state): do not profile calls into Lean other than tactic execution

Browse source 
Otherwise, we produce a message for e.g. every single interactive tactic parameter
This commit is contained in:
Sebastian Ullrich 2018-02-17 22:25:23 +01:00 • committed by Leonardo de Moura
parent 9c5df7875a
commit 782af7e5d6
4 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3704,7 +3704,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
try {
scoped_expr_caching scope(true);
vm_obj r = tactic_evaluator(m_ctx, m_opts, ref)(tactic, s);
vm_obj r = tactic_evaluator(m_ctx, m_opts, ref, /* allow_profiler */ true)(tactic, s);
expr val;
if (auto new_s = tactic::is_success(r)) {
metavar_context mctx = new_s->mctx();

4
src/library/tactic/tactic_evaluator.h
View file

@ -23,8 +23,8 @@ private:
protected:
virtual void process_failure(vm_state & S, vm_obj const & r) override;
public:
tactic_evaluator(type_context & ctx, options const & opts, expr const & ref):
tactic::evaluator(ctx, opts), m_ref(ref) {}
tactic_evaluator(type_context & ctx, options const & opts, expr const & ref, bool allow_profiler = false):
tactic::evaluator(ctx, opts, allow_profiler), m_ref(ref) {}
virtual vm_obj operator()(expr const & tactic, buffer<vm_obj> const & args, tactic_state const & s) override;
vm_obj operator()(expr const & tactic, tactic_state const & s) {
return tactic::evaluator::operator()(tactic, s);

4
src/library/vm/interaction_state.h
View file

@ -58,11 +58,11 @@ struct interaction_monad {
class evaluator {
type_context & m_ctx;
options const & m_opts;
options m_opts;
protected:
virtual void process_failure(vm_state & S, vm_obj const & r);
public:
evaluator(type_context & ctx, options const & opts);
evaluator(type_context & ctx, options const & opts, bool allow_profiler = false);
environment compile(name const & interaction_name, expr const & interaction);
vm_obj invoke(vm_state & S, name const & interaction_name,
std::initializer_list<vm_obj> const & args);

5
src/library/vm/interaction_state_imp.h
View file

@ -239,8 +239,11 @@ vm_obj interaction_monad<State>::evaluator::invoke(vm_state & S, name const & in
}
template<typename State>
interaction_monad<State>::evaluator::evaluator(type_context & ctx, options const & opts):
interaction_monad<State>::evaluator::evaluator(type_context & ctx, options const & opts, bool allow_profiler):
m_ctx(ctx), m_opts(opts) {
if (!allow_profiler)
// do not bother to invoke the profiler for most trivial calls into Lean
m_opts = m_opts.update("profiler", false);
}
template<typename State>