feat(library/blast): improve tracing

src/library/blast/blast.cpp

@@ -1148,7 +1148,7 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
 void initialize_blast() {
     register_trace_class("blast");
     register_trace_class(name{"blast_detailed"});
-    register_trace_class(name({"blast", "event"}));
+    register_trace_class(name{"blast", "event"});
     register_trace_class(name{"blast", "state"});
     register_trace_class(name{"blast", "action"});
     register_trace_class(name{"blast", "search"});

src/library/blast/forward/ematch.cpp

@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "util/interrupt.h"
-#include "library/trace.h"
 #include "library/constants.h"
 #include "library/idx_metavar.h"
 #include "library/head_map.h"
@@ -305,7 +304,7 @@ struct ematch_fn {
         if (!m_new_instances) {
             trace_action("ematch");
         }
-        lean_trace(name({"blast", "ematch"}), tout() << "ematch_instance: " << ppb(new_inst) << "\n";);
+        lean_trace(name({"blast", "ematch"}), tout() << "instance: " << ppb(new_inst) << "\n";);
         m_new_instances = true;
         expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof);
         m_ext.m_instances.insert(new_inst);

src/library/blast/state.cpp

@@ -6,12 +6,14 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <algorithm>
+#include "library/trace.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "library/replace_visitor.h"
 #include "library/blast/util.h"
+#include "library/blast/trace.h"
 #include "library/blast/blast.h"
 #include "library/blast/state.h"
 
@@ -840,6 +842,9 @@ optional<unsigned> state::select_hypothesis_to_activate() {
 }
 
 void state::activate_hypothesis(hypothesis_idx hidx) {
+    lean_trace(name({"blast", "search"}),
+               hypothesis const & h = get_hypothesis_decl(hidx);
+               tout() << "activate: " << h.get_name() << " : " << ppb(h.get_type()) << "\n";);
     m_branch.m_active.insert(hidx);
     update_indices(hidx);
 }

src/library/blast/strategy.cpp

@@ -93,6 +93,9 @@ optional<expr> strategy_fn::search() {
             r = next_action();
             break;
         }
+        lean_trace(name({"blast", "search"}),
+                   tout() << "depth [" << curr_state().get_proof_depth() << "], #choice: "
+                   << get_num_choice_points() << "\n";);
         trace_curr_state_if(r);
     }
 }

src/library/blast/trace.cpp

@@ -14,9 +14,7 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 void trace_curr_state() {
-    lean_trace(name({"blast", "state"}),
-               tout() << "[" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n";
-               curr_state().display(tout()););
+    lean_trace(name({"blast", "state"}), tout() << "\n"; curr_state().display(tout()););
 }
 
 void trace_search(char const * msg) {