feat(library/blast/trace): improve trace depth

src/library/blast/strategy.cpp

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

src/library/blast/trace.cpp

@@ -56,6 +56,21 @@ void trace_curr_state() {
     }
 }
 
+typedef pair<unsigned, unsigned> unsigned_pair;
+MK_THREAD_LOCAL_GET(unsigned_pair, get_depth_num_choices, mk_pair(-1, -1));
+
+void trace_depth_nchoices() {
+    if (!lean_is_trace_enabled(name({"blast", "search"})))
+        return;
+    auto & p = get_depth_num_choices();
+    if (p.first == curr_state().get_proof_depth() &&
+        p.second == get_num_choice_points())
+        return;
+    p = mk_pair(curr_state().get_proof_depth(), get_num_choice_points());
+    lean_trace(name({"blast", "search"}),
+               tout() << "depth: " << p.first << ", #choice: " << p.second << "\n";);
+}
+
 void trace_search(char const * msg) {
     lean_trace(name({"blast", "search"}), tout() << msg << "\n";);
 }

src/library/blast/trace.h

@@ -13,6 +13,7 @@ namespace blast {
 void trace_curr_state();
 void trace_target();
 void trace_search(char const * msg);
+void trace_depth_nchoices();
 void trace_action(char const * a);
 void trace_curr_state_if(action_result r);