From 782af7e5d6aa3f62959eafa35ed0e7bd8d5a2668 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 17 Feb 2018 22:25:23 +0100
Subject: [PATCH] chore(library/vm/interaction_state): do not profile calls
 into Lean other than tactic execution

Otherwise, we produce a message for e.g. every single interactive tactic parameter
---
 src/frontends/lean/elaborator.cpp      | 2 +-
 src/library/tactic/tactic_evaluator.h  | 4 ++--
 src/library/vm/interaction_state.h     | 4 ++--
 src/library/vm/interaction_state_imp.h | 5 ++++-
 4 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index dd1ca25241..d3f2203d1c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -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();
diff --git a/src/library/tactic/tactic_evaluator.h b/src/library/tactic/tactic_evaluator.h
index f147fe82cc..a3f57da370 100644
--- a/src/library/tactic/tactic_evaluator.h
+++ b/src/library/tactic/tactic_evaluator.h
@@ -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);
diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h
index 4c8122a461..31d88eae3f 100644
--- a/src/library/vm/interaction_state.h
+++ b/src/library/vm/interaction_state.h
@@ -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);
diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h
index e515c0b76c..4f7047220d 100644
--- a/src/library/vm/interaction_state_imp.h
+++ b/src/library/vm/interaction_state_imp.h
@@ -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>