feat(library/blast): include strategies failure states in the tactic_exception

Reason: better flycheck error messages

src/library/blast/blast.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include <vector>
 #include "util/sstream.h"
 #include "kernel/for_each_fn.h"
@@ -76,6 +77,11 @@ class blastenv {
 
     environment                m_env;
     io_state                   m_ios;
+    /* blast may use different strategies.
+       We use m_buffer_ios to store messages describing failed attempts.
+       These messages are reported to the user only if none of the strategies have worked.
+       We dump the content of the diagnostic channel into an blast_exception. */
+    io_state                   m_buffer_ios;
     name_generator             m_ngen;
     unsigned                   m_next_uref_idx{0};
     unsigned                   m_next_mref_idx{0};
@@ -484,7 +490,8 @@ class blastenv {
 
 public:
     blastenv(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
-        m_env(env), m_ios(ios), m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
+        m_env(env), m_ios(ios), m_buffer_ios(ios),
+        m_ngen(*g_prefix), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
         m_not_reducible_pred(mk_not_reducible_pred(env)),
         m_class_pred(mk_class_pred(env)),
         m_instance_pred(mk_instance_pred(env)),
@@ -502,6 +509,7 @@ public:
         m_unfold_macro_pred([](expr const &) { return true; }),
         m_tctx(*this),
         m_normalizer(m_tctx) {
+        m_buffer_ios.set_diagnostic_channel(std::shared_ptr<output_channel>(new string_output_channel()));
         clear_choice_points();
     }
 
@@ -533,12 +541,18 @@ public:
         init_classical_flag();
     }
 
-    optional<expr> operator()(goal const & g) {
+    expr operator()(goal const & g) {
         init_state(g);
         if (auto r = apply_strategy()) {
-            return some_expr(to_tactic_proof(*r));
+            return to_tactic_proof(*r);
         } else {
-            return none_expr();
+            string_output_channel & channel = static_cast<string_output_channel &>(m_buffer_ios.get_diagnostic_channel());
+            std::string buffer = channel.str();
+            if (buffer.empty()) {
+                throw blast_exception(sstream() << " blast tactic failed");
+            } else {
+                throw blast_exception(sstream() << " blast tactic failed\n" << buffer << "-------");
+            }
         }
     }
 
@@ -546,6 +560,8 @@ public:
 
     io_state const & get_ios() const { return m_ios; }
 
+    io_state const & get_buffer_ios() const { return m_buffer_ios; }
+
     state & get_curr_state() { return m_curr_state; }
 
     bool is_reducible(name const & n) const {
@@ -1037,6 +1053,16 @@ void display(sstream const & msg) {
     ios().get_diagnostic_channel() << msg.str();
 }
 
+void display_at_buffer(sstream const & msg) {
+    lean_assert(g_blastenv);
+    g_blastenv->get_buffer_ios().get_diagnostic_channel() << msg.str();
+}
+
+void display_curr_state_at_buffer() {
+    lean_assert(g_blastenv);
+    curr_state().display(g_blastenv->get_env(), g_blastenv->get_buffer_ios());
+}
+
 scope_assignment::scope_assignment():m_keep(false) {
     lean_assert(g_blastenv);
     g_blastenv->m_tctx.push();
@@ -1162,7 +1188,7 @@ expr internalize(expr const & e) {
     return g_blastenv->internalize(e);
 }
 }
-optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
+expr blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
     scoped_expr_caching             scope1(true);
     blast::blastenv                 b(env, ios, ls, ds);

src/library/blast/blast.h

@@ -181,6 +181,12 @@ void display_expr(expr const & e);
 /** \brief Display message in the blast tactic diagnostic channel. */
 void display(char const * msg);
 void display(sstream const & msg);
+
+/** \brief Display curr state at buffered diagnostic channel used to craft an exception for user */
+void display_curr_state_at_buffer();
+/** \brief Display msng at buffered diagnostic channel used to craft an exception for user */
+void display_at_buffer(sstream const & msg);
+
 /** \brief Create a local scope for saving the assignment and
     metavariable declarations at curr_state() */
 class scope_assignment {
@@ -245,8 +251,8 @@ public:
     \remark This procedure should only be used for **debugging purposes**. */
 expr internalize(expr const & e);
 }
-optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
-                          goal const & g);
+expr blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
+                goal const & g);
 void initialize_blast();
 void finalize_blast();
 }

src/library/blast/blast_exception.h

@@ -11,10 +11,12 @@ Author: Leonardo de Moura
 
 namespace lean {
 class blast_exception : public exception {
-    expr m_expr;
+    optional<expr> m_expr;
 public:
     blast_exception(char const * msg, expr const & e):exception(msg), m_expr(e) {}
+    blast_exception(std::string const & msg, optional<expr> const & e):exception(msg), m_expr(e) {}
     blast_exception(std::string const & msg, expr const & e):exception(msg), m_expr(e) {}
+    blast_exception(sstream const & strm):exception(strm) {}
     virtual ~blast_exception() {}
     virtual throwable * clone() const { return new blast_exception(m_msg, m_expr); }
     virtual void rethrow() const { throw *this; }

src/library/blast/blast_tactic.cpp

@@ -19,15 +19,11 @@ tactic mk_blast_tactic(list<name> const & ls, list<name> const & ds) {
             }
             goal const & g = head(gs);
             try {
-                if (auto pr = blast_goal(env, ios, ls, ds, g)) {
-                    goals new_gs           = tail(gs);
-                    substitution new_subst = s.get_subst();
-                    assign(new_subst, g, *pr);
-                    return some_proof_state(proof_state(s, new_gs, new_subst));
-                } else {
-                    throw_tactic_exception_if_enabled(s, "blast tactic failed");
-                    return none_proof_state();
-                }
+                expr pr = blast_goal(env, ios, ls, ds, g);
+                goals new_gs           = tail(gs);
+                substitution new_subst = s.get_subst();
+                assign(new_subst, g, pr);
+                return some_proof_state(proof_state(s, new_gs, new_subst));
             } catch (blast_exception & ex) {
                 throw_tactic_exception_if_enabled(s, ex.what());
                 return none_proof_state();

src/library/blast/strategy.cpp

@@ -77,8 +77,10 @@ optional<expr> strategy_fn::search() {
             if (failed(r)) {
                 // all choice points failed...
                 lean_trace_search(tout() << "strategy '" << get_name() << "' failed, no proof found\n";);
-                if (show_failure())
-                    display_curr_state();
+                if (show_failure()) {
+                    display_at_buffer(sstream() << "strategy '" << get_name() << "' failed, no proof found, final state:\n");
+                    display_curr_state_at_buffer();
+                }
                 return none_expr();
             }
             break;