From f0c42defc8e7ec196ea8dca0f7050771ed111837 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Dec 2015 15:53:43 -0800
Subject: [PATCH] feat(library/blast/grinder): add tracing for suspicious event

---
 src/library/blast/grinder/intro_elim_lemmas.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp
index fec56f5ae..8573d836d 100644
--- a/src/library/blast/grinder/intro_elim_lemmas.cpp
+++ b/src/library/blast/grinder/intro_elim_lemmas.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/priority_queue.h"
 #include "kernel/instantiate.h"
+#include "library/trace.h"
 #include "library/scoped_ext.h"
 #include "library/user_recursors.h"
 #include "library/tmp_type_context.h"
@@ -134,7 +135,8 @@ head_map<gexpr> mk_intro_lemma_index() {
         ctx->clear();
         optional<name> target = get_intro_target(*ctx, lemmas[i]);
         if (!target) {
-            // TODO(Leo): generate event
+            lean_trace(name({"blast", "event"}),
+                       tout() << "discarding [intro] lemma '" << lemmas[i] << "', failed to find target type\n";);
         } else {
             r.insert(head_index(*target), gexpr(lemmas[i]));
         }
@@ -151,7 +153,8 @@ name_map<name> mk_elim_lemma_index() {
             recursor_info info = get_recursor_info(env(), lemma);
             r.insert(info.get_type_name(), lemma);
         } catch (exception &) {
-            // TODO(Leo): generate event
+            lean_trace(name({"blast", "event"}),
+                       tout() << "discarding [elim] lemma '" << lemma << "', failed to compute recursor information\n";);
         }
     }
     return r;