diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp
index 36e2f87d4..c70b526ba 100644
--- a/src/library/blast/backward/backward_strategy.cpp
+++ b/src/library/blast/backward/backward_strategy.cpp
@@ -50,6 +50,8 @@ static backward_branch_extension & get_extension() {
 
 /** \brief Basic backwards chaining, inspired by Coq's [auto]. */
 class backward_strategy_fn : public strategy_fn {
+    virtual char const * get_name() const override { return "backward"; }
+
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(subst_action(hidx));
diff --git a/src/library/blast/grinder/grinder_strategy.h b/src/library/blast/grinder/grinder_strategy.h
index 933e91d9d..cb7d42383 100644
--- a/src/library/blast/grinder/grinder_strategy.h
+++ b/src/library/blast/grinder/grinder_strategy.h
@@ -13,6 +13,7 @@ namespace blast {
     The methods pre/post/next can be redefined to extend the set of actions
     applied by the grinder. This strategy applies the grinder intro/elim actions. */
 class grinder_strategy_core_fn : public strategy_fn {
+    virtual char const * get_name() const override { return "grinder"; }
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override;
     virtual action_result hypothesis_post_activation(hypothesis_idx hidx) override;
     virtual action_result next_action() override;
diff --git a/src/library/blast/simplifier/simplifier_strategies.cpp b/src/library/blast/simplifier/simplifier_strategies.cpp
index c8cd3416b..4b6caa0f6 100644
--- a/src/library/blast/simplifier/simplifier_strategies.cpp
+++ b/src/library/blast/simplifier/simplifier_strategies.cpp
@@ -19,6 +19,8 @@ class simplifier_strategy_fn : public strategy_fn {
     bool m_simp_hyps;
     bool m_use_hyps;
 
+    virtual char const * get_name() const override { return "simp"; }
+
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         if (m_simp_hyps) {
diff --git a/src/library/blast/strategies/debug_action_strategy.cpp b/src/library/blast/strategies/debug_action_strategy.cpp
index 46bdce69a..1d34bab5e 100644
--- a/src/library/blast/strategies/debug_action_strategy.cpp
+++ b/src/library/blast/strategies/debug_action_strategy.cpp
@@ -15,6 +15,8 @@ class debug_action_strategy_core_fn : public strategy_fn {
     virtual action_result post(hypothesis_idx) { return action_result::failed(); }
     virtual action_result next() { return action_result::failed(); }
 
+    virtual char const * get_name() const override { return "debug-action"; }
+
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(discard_action(hidx));
diff --git a/src/library/blast/strategies/preprocess_strategy.cpp b/src/library/blast/strategies/preprocess_strategy.cpp
index d3de6e5aa..6cd26d99c 100644
--- a/src/library/blast/strategies/preprocess_strategy.cpp
+++ b/src/library/blast/strategies/preprocess_strategy.cpp
@@ -27,6 +27,8 @@ class preprocess_strategy_fn : public strategy_fn {
 
     virtual bool show_failure() const override { return false; }
 
+    virtual char const * get_name() const override { return "preprocessor"; }
+
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(simplify_hypothesis_action(hidx));
@@ -58,7 +60,9 @@ class preprocess_strategy_fn : public strategy_fn {
         }
         if (get_num_choice_points() > get_initial_num_choice_points())
             throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points");
-        if (optional<expr> pf = m_main()) { return action_result::solved(*pf); }
+        if (optional<expr> pf = m_main()) {
+            return action_result::solved(*pf);
+        }
         return action_result::failed();
     }
 public:
diff --git a/src/library/blast/strategies/simple_strategy.cpp b/src/library/blast/strategies/simple_strategy.cpp
index ffdd9c8d8..8e377f900 100644
--- a/src/library/blast/strategies/simple_strategy.cpp
+++ b/src/library/blast/strategies/simple_strategy.cpp
@@ -29,6 +29,8 @@ namespace blast {
 /** \brief Implement a simple proof strategy for blast.
     We use it mainly for testing new actions and the whole blast infra-structure. */
 class simple_strategy_fn : public strategy_fn {
+    virtual char const * get_name() const override { return "simple"; }
+
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) override {
         Try(assumption_contradiction_actions(hidx));
         Try(simplify_hypothesis_action(hidx));
diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp
index ccc3c8493..3a27cd0d2 100644
--- a/src/library/blast/strategy.cpp
+++ b/src/library/blast/strategy.cpp
@@ -58,7 +58,7 @@ optional<expr> strategy_fn::search() {
     m_init_num_choices        = get_num_choice_points();
     unsigned init_proof_depth = curr_state().get_proof_depth();
     unsigned max_depth        = get_config().m_max_depth;
-    lean_trace_search(tout() << "search upto depth " << max_depth << "\n";);
+    lean_trace_search(tout() << "begin '" << get_name() << "' strategy (max-depth: " << max_depth << ")\n";);
     trace_curr_state();
     trace_target();
     action_result r = next_action();
@@ -75,7 +75,7 @@ optional<expr> strategy_fn::search() {
             r = next_choice_point(m_init_num_choices);
             if (failed(r)) {
                 // all choice points failed...
-                trace_search(">>> proof not found, no choice points left <<<");
+                lean_trace_search(tout() << "strategy '" << get_name() << "' failed, no proof found\n";);
                 if (show_failure())
                     display_curr_state();
                 return none_expr();
@@ -86,7 +86,7 @@ optional<expr> strategy_fn::search() {
             r = next_branch(r.get_proof());
             if (r.get_kind() == action_result::Solved) {
                 // all branches have been solved
-                trace_search("* found proof");
+                lean_trace_search(tout() << "strategy '" << get_name() << "' succeeded, proof found\n";);
                 return some_expr(unfold_hypotheses_ge(curr_state(), r.get_proof(), init_proof_depth));
             }
             trace_search("* next branch");
diff --git a/src/library/blast/strategy.h b/src/library/blast/strategy.h
index 3be08d0de..66cf0e0ba 100644
--- a/src/library/blast/strategy.h
+++ b/src/library/blast/strategy.h
@@ -27,6 +27,7 @@ protected:
     virtual action_result hypothesis_pre_activation(hypothesis_idx hidx) = 0;
     virtual action_result hypothesis_post_activation(hypothesis_idx hidx) = 0;
     virtual bool show_failure() const;
+    virtual char const * get_name() const = 0;
     action_result activate_hypothesis();
     unsigned get_initial_num_choice_points() const { return m_init_num_choices; }
     action_result next_branch(expr pr);