From 7fc216183e6e42a61fb34da1178fd91ae2192c56 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Feb 2015 16:56:42 -0800
Subject: [PATCH] feat(library/tactic): produce better error message when a
 tactic fails

closes #348
---
 src/frontends/lean/elaborator.cpp         | 35 +++++++++++++++--------
 src/frontends/lean/elaborator.h           |  5 ++--
 src/library/tactic/apply_tactic.cpp       | 26 +++++++++++++----
 src/library/tactic/assert_tactic.cpp      |  6 +++-
 src/library/tactic/exact_tactic.cpp       |  4 ++-
 src/library/tactic/expr_to_tactic.h       |  8 ++++--
 src/library/tactic/generalize_tactic.cpp  | 15 ++++++++--
 src/library/tactic/intros_tactic.cpp      |  4 ++-
 src/library/tactic/rename_tactic.cpp      |  4 ++-
 src/library/tactic/revert_tactic.cpp      | 10 +++++--
 src/library/tactic/rewrite_tactic.cpp     |  9 +++++-
 src/library/tactic/tactic.cpp             | 20 +++++++++++--
 src/library/tactic/tactic.h               | 18 ++++++++++--
 tests/lean/apply_fail.lean                |  4 +++
 tests/lean/apply_fail.lean.expected.out   | 13 +++++++++
 tests/lean/assert_fail.lean               | 10 +++++++
 tests/lean/assert_fail.lean.expected.out  | 22 ++++++++++++++
 tests/lean/beginend_bug.lean.expected.out | 12 +++++++-
 tests/lean/gen_bug.lean.expected.out      | 16 ++++++++++-
 tests/lean/gen_fail.lean                  |  7 +++++
 tests/lean/gen_fail.lean.expected.out     | 20 +++++++++++++
 tests/lean/revert_fail.lean               | 17 +++++++++++
 tests/lean/revert_fail.lean.expected.out  | 33 +++++++++++++++++++++
 tests/lean/rewrite_fail.lean              | 12 ++++++++
 tests/lean/rewrite_fail.lean.expected.out | 23 +++++++++++++++
 25 files changed, 315 insertions(+), 38 deletions(-)
 create mode 100644 tests/lean/apply_fail.lean
 create mode 100644 tests/lean/apply_fail.lean.expected.out
 create mode 100644 tests/lean/assert_fail.lean
 create mode 100644 tests/lean/assert_fail.lean.expected.out
 create mode 100644 tests/lean/gen_fail.lean
 create mode 100644 tests/lean/gen_fail.lean.expected.out
 create mode 100644 tests/lean/revert_fail.lean
 create mode 100644 tests/lean/revert_fail.lean.expected.out
 create mode 100644 tests/lean/rewrite_fail.lean
 create mode 100644 tests/lean/rewrite_fail.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 41f5bc20d..eecc420c5 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1480,14 +1480,30 @@ optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
     }
 }
 
+void elaborator::display_tactic_exception(tactic_exception const & ex, proof_state const & ps, expr const & pre_tac) {
+    auto out = regular(env(), ios());
+    flycheck_error err(out);
+    if (optional<expr> const & e = ex.get_main_expr())
+        display_error_pos(out, pip(), *e);
+    else
+        display_error_pos(out, pip(), pre_tac);
+    out << ex.pp(out.get_formatter()) << "\nproof state:\n";
+    if (auto curr_ps = ex.get_proof_state())
+        out << curr_ps->pp(env(), ios()) << "\n";
+    else
+        out << ps.pp(env(), ios()) << "\n";
+}
+
 /** \brief Try to instantiate meta-variable \c mvar (modulo its state ps) using the given tactic.
     If it succeeds, then update subst with the solution.
     Return true iff the metavariable \c mvar has been assigned.
 
     If \c show_failure == true, then display reason for failure.
+
+    \remark the argument \c pre_tac is only used for error localization.
 */
-bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
-                           bool show_failure) {
+bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state const & ps,
+                           expr const & pre_tac, tactic const & tac, bool show_failure) {
     lean_assert(length(ps.get_goals()) == 1);
     // make sure ps is a really a proof state for mvar.
     lean_assert(mlocal_name(get_app_fn(head(ps.get_goals()).get_meta())) == mlocal_name(mvar));
@@ -1511,11 +1527,8 @@ bool elaborator::try_using(substitution & subst, expr const & mvar, proof_state
             return true;
         }
     } catch (tactic_exception & ex) {
-        if (show_failure) {
-            auto out = regular(env(), ios());
-            display_error_pos(out, pip(), ex.get_expr());
-            out << " tactic failed: " << ex.what() << "\n";
-        }
+        if (show_failure)
+            display_tactic_exception(ex, ps, pre_tac);
         return false;
     }
 }
@@ -1562,9 +1575,7 @@ void elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
                 }
                 ps = r->first;
             } catch (tactic_exception & ex) {
-                auto out = regular(env(), ios());
-                display_error_pos(out, pip(), ex.get_expr());
-                out << " tactic failed: " << ex.what() << "\n";
+                display_tactic_exception(ex, ps, ptac);
                 return;
             }
         } else {
@@ -1603,7 +1614,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
 
         if (auto tac = pre_tactic_to_tactic(subst.instantiate_all(*pre_tac))) {
             bool show_failure = true;
-            try_using(subst, mvar, ps, *tac, show_failure);
+            try_using(subst, mvar, ps, *pre_tac, *tac, show_failure);
             return;
         }
     }
@@ -1613,7 +1624,7 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set
         for (expr const & pre_tac : get_tactic_hints(env())) {
             if (auto tac = pre_tactic_to_tactic(pre_tac)) {
                 bool show_failure = false;
-                if (try_using(subst, mvar, ps, *tac, show_failure))
+                if (try_using(subst, mvar, ps, pre_tac, *tac, show_failure))
                     return;
             }
         }
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 2541eca60..13a55e0ec 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -145,10 +145,11 @@ class elaborator : public coercion_info_manager {
     unify_result_seq solve(constraint_seq const & cs);
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg, expr const & pos);
     void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg);
+    void display_tactic_exception(tactic_exception const & ex, proof_state const & ps, expr const & pre_tac);
     optional<expr> get_pre_tactic_for(expr const & mvar);
     optional<tactic> pre_tactic_to_tactic(expr const & pre_tac);
-    bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, tactic const & tac,
-                   bool show_failure);
+    bool try_using(substitution & subst, expr const & mvar, proof_state const & ps,
+                   expr const & pre_tac, tactic const & tac, bool show_failure);
     void try_using_begin_end(substitution & subst, expr const & mvar, proof_state ps, expr const & pre_tac);
     void solve_unassigned_mvar(substitution & subst, expr mvar, name_set & visited);
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited);
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index 3a8466dc3..8db063b53 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
+#include "kernel/error_msgs.h"
 #include "kernel/type_checker.h"
 #include "library/reducible.h"
 #include "library/kernel_bindings.h"
@@ -72,8 +73,10 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
                                          expr const & _e, buffer<constraint> & cs,
                                          bool add_meta, subgoals_action_kind subgoals_action) {
     goals const & gs = s.get_goals();
-    if (empty(gs))
+    if (empty(gs)) {
+        throw_no_goal_if_enabled(s);
         return proof_state_seq();
+    }
     bool class_inst   = get_apply_class_instance(ios.get_options());
     name_generator ngen = s.get_ngen();
     bool relax_opaque = s.relax_main_opaque();
@@ -124,8 +127,16 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     metavar_closure cls(t);
     cls.mk_constraints(s.get_subst(), justification(), relax_opaque);
     pair<bool, constraint_seq> dcs = tc->is_def_eq(t, e_t);
-    if (!dcs.first)
+    if (!dcs.first) {
+        throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
+                format r = format("invalid 'apply' tactic, failed to unify");
+                r       += pp_indent_expr(fmt, t);
+                r       += compose(line(), format("with"));
+                r       += pp_indent_expr(fmt, e_t);
+                return r;
+            });
         return proof_state_seq();
+    }
     dcs.second.linearize(cs);
     unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), s.get_subst(), cfg);
     list<expr> meta_lst   = to_list(metas.begin(), metas.end());
@@ -172,14 +183,17 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
 tactic eassumption_tactic() {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
-            if (empty(gs))
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
                 return proof_state_seq();
+            }
+            proof_state new_s = s.update_report_failure(false);
             proof_state_seq r;
             goal g = head(gs);
             buffer<expr> hs;
             get_app_args(g.get_meta(), hs);
             for (expr const & h : hs) {
-                r = append(r, apply_tactic_core(env, ios, s, h, false, IgnoreSubgoals));
+                r = append(r, apply_tactic_core(env, ios, new_s, h, false, IgnoreSubgoals));
             }
             return r;
         });
@@ -188,8 +202,10 @@ tactic eassumption_tactic() {
 tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, subgoals_action_kind k) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
-            if (empty(gs))
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
                 return proof_state_seq();
+            }
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
             expr       new_e;
diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp
index dffc19b68..8211733e6 100644
--- a/src/library/tactic/assert_tactic.cpp
+++ b/src/library/tactic/assert_tactic.cpp
@@ -15,13 +15,17 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e)
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
-            if (!gs)
+            if (!gs) {
+                throw_no_goal_if_enabled(s);
                 return none_proof_state();
+            }
             bool report_unassigned = true;
             if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) {
                 goals const & gs   = new_s.get_goals();
                 goal const & g     = head(gs);
                 if (g.find_hyp(id)) {
+                    throw_tactic_exception_if_enabled(s, sstream() << "invalid 'assert' tactic, goal already has a "
+                                                      "hypothesis named '" << id << "'");
                     // goal already has a hypothesis named id
                     return none_proof_state();
                 }
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index f7386c49e..9767d827e 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -15,8 +15,10 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
     return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
-            if (!gs)
+            if (!gs) {
+                throw_no_goal_if_enabled(s);
                 return none_proof_state();
+            }
             expr t            = head(gs).get_type();
             bool report_unassigned = true;
             if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) {
diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h
index 6c5b37cda..c36778c2c 100644
--- a/src/library/tactic/expr_to_tactic.h
+++ b/src/library/tactic/expr_to_tactic.h
@@ -65,10 +65,12 @@ expr const & get_repeat_tac_fn();
 expr const & get_determ_tac_fn();
 
 /** \brief Exception used to report a problem when an expression is being converted into a tactic. */
-class expr_to_tactic_exception : public tactic_exception {
+class expr_to_tactic_exception : public exception {
+    expr m_expr;
 public:
-    expr_to_tactic_exception(expr const & e, char const * msg):tactic_exception(e, msg) {}
-    expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {}
+    expr_to_tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
+    expr_to_tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
+    expr const & get_expr() const { return m_expr; }
 };
 
 typedef std::function<tactic(type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *)>
diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp
index ed4f685e0..cf6414ec6 100644
--- a/src/library/tactic/generalize_tactic.cpp
+++ b/src/library/tactic/generalize_tactic.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/constants.h"
 #include "kernel/abstract.h"
+#include "kernel/kernel_exception.h"
 #include "library/reducible.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
@@ -21,8 +22,11 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                 goal const & g      = head(gs);
                 auto tc     = mk_type_checker(env, ngen.mk_child());
                 auto e_t_cs = tc->infer(*new_e);
-                if (e_t_cs.second)
+                if (e_t_cs.second) {
+                    throw_tactic_exception_if_enabled(s, "invalid 'generalize' tactic, unification constraints "
+                                                      "have been generated when inferring type");
                     return none_proof_state(); // constraints were generated
+                }
                 expr e_t    = e_t_cs.first;
                 expr t      = subst.instantiate(g.get_type());
                 name n;
@@ -37,7 +41,14 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                 expr new_v = g.abstract(mk_app(new_m, *new_e));
                 try {
                     tc->check_ignore_levels(g.abstract(new_t));
-                } catch (exception &) {
+                } catch (kernel_exception const & ex) {
+                    std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
+                    throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {
+                            format r = format("invalid 'generalize' tactic, type error");
+                            r       += line();
+                            r       += ex_ptr->pp(fmt);
+                            return r;
+                        });
                     return none_proof_state();
                 }
 
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index c34dc449c..d5bf3ba45 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -15,8 +15,10 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
     auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
         list<name> ns    = _ns;
         goals const & gs = s.get_goals();
-        if (empty(gs))
+        if (empty(gs)) {
+            throw_no_goal_if_enabled(s);
             return optional<proof_state>();
+        }
         goal const & g      = head(gs);
         name_generator ngen = s.get_ngen();
         auto tc             = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp
index 1bd47b40b..ae3a8eb5d 100644
--- a/src/library/tactic/rename_tactic.cpp
+++ b/src/library/tactic/rename_tactic.cpp
@@ -13,8 +13,10 @@ namespace lean {
 tactic rename_tactic(name const & from, name const & to) {
     return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             goals const & gs = s.get_goals();
-            if (empty(gs))
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
                 return none_proof_state();
+            }
             goal const & g        = head(gs);
             goals const & rest_gs = tail(gs);
             buffer<expr> locals;
diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp
index 086c6031d..365d70295 100644
--- a/src/library/tactic/revert_tactic.cpp
+++ b/src/library/tactic/revert_tactic.cpp
@@ -14,8 +14,10 @@ namespace lean {
 tactic revert_tactic(name const & n) {
     auto fn = [=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
         goals const & gs = s.get_goals();
-        if (empty(gs))
+        if (empty(gs)) {
+            throw_no_goal_if_enabled(s);
             return none_proof_state();
+        }
         goal  g          = head(gs);
         goals tail_gs    = tail(gs);
         if (auto p = g.find_hyp(n)) {
@@ -24,8 +26,11 @@ tactic revert_tactic(name const & n) {
             buffer<expr> hyps;
             g.get_hyps(hyps);
             hyps.erase(hyps.size() - i - 1);
-            if (depends_on(i, hyps.end() - i, h))
+            if (optional<expr> other_h = depends_on(i, hyps.end() - i, h)) {
+                throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, hypothesis '" << local_pp_name(*other_h)
+                                                  << "' depends on '" << local_pp_name(h) << "'");
                 return none_proof_state(); // other hypotheses depend on h
+            }
             name_generator ngen = s.get_ngen();
             expr new_type = Pi(h, g.get_type());
             expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
@@ -36,6 +41,7 @@ tactic revert_tactic(name const & n) {
             proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
             return some_proof_state(new_s);
         } else {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid 'revert' tactic, unknown hypothesis '" << n << "'");
             return none_proof_state();
         }
     };
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 5be59c35a..27470cb4b 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1161,6 +1161,11 @@ public:
         for (expr const & elem : elems) {
             flet<expr> set1(m_expr_loc, elem);
             if (!process_step(elem)) {
+                if (m_ps.report_failure()) {
+                    proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen);
+                    throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
+                                           [](formatter const &) { return format("invalid 'rewrite' tactic, rewrite step failed"); });
+                }
                 return proof_state_seq();
             }
         }
@@ -1178,8 +1183,10 @@ public:
 tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer<expr> const & elems) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
-            if (empty(gs))
+            if (empty(gs)) {
+                throw_no_goal_if_enabled(s);
                 return proof_state_seq();
+            }
             return rewrite_fn(env, ios, elab, s)(elems);
         });
 }
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 1fbf4b4c7..e0cb733df 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -34,8 +34,24 @@ void check_has_no_local(expr const & v, expr const & e, char const * tac_name) {
     }
 }
 
-tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
-tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
+tactic_exception::tactic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn):
+    generic_exception(msg, m, fn) {}
+tactic_exception::tactic_exception(char const * msg, optional<expr> const & m, proof_state const & ps, pp_fn const & fn):
+    generic_exception(msg, m, fn), m_ps(ps) {}
+tactic_exception::tactic_exception(expr const & e, std::string const & msg):
+    generic_exception(msg.c_str(), some_expr(e), [=](formatter const &) { return format(msg); }) {}
+tactic_exception::tactic_exception(std::string const & msg):
+    generic_exception(msg.c_str(), none_expr(), [=](formatter const &) { return format(msg); }) {}
+tactic_exception::tactic_exception(char const * msg):tactic_exception(std::string(msg)) {}
+tactic_exception::tactic_exception(sstream const & strm):tactic_exception(strm.str()) {}
+tactic_exception::tactic_exception(expr const & e, char const * msg):tactic_exception(e, std::string(msg)) {}
+tactic_exception::tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm.str()) {}
+tactic_exception::tactic_exception(expr const & e, pp_fn const & fn):generic_exception("tactic exception", some_expr(e), fn) {}
+tactic_exception::tactic_exception(pp_fn const & fn):generic_exception("tactic exception", none_expr(), fn) {}
+
+void throw_no_goal_if_enabled(proof_state const & ps) {
+    throw_tactic_exception_if_enabled(ps, "invalid tactic, there are no goals to be solved");
+}
 
 tactic tactic01(std::function<optional<proof_state>(environment const &, io_state const & ios, proof_state const &)> f) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 5ab95c706..a6aebefa6 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -11,20 +11,32 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/lazy_list.h"
 #include "library/io_state.h"
+#include "library/generic_exception.h"
 #include "library/tactic/proof_state.h"
 
 namespace lean {
 /** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
 void check_has_no_local(expr const & v, expr const & e, char const * tac_name);
 
-class tactic_exception : public exception {
-    expr m_expr;
+class tactic_exception : public generic_exception {
+    optional<proof_state> m_ps;
 public:
+    tactic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn);
+    tactic_exception(char const * msg, optional<expr> const & m, proof_state const & ps, pp_fn const & fn);
+    tactic_exception(expr const & e, std::string const & msg);
     tactic_exception(expr const & e, char const * msg);
     tactic_exception(expr const & e, sstream const & strm);
-    expr const & get_expr() const { return m_expr; }
+    tactic_exception(expr const & e, pp_fn const & fn);
+    tactic_exception(std::string const & msg);
+    tactic_exception(char const * msg);
+    tactic_exception(sstream const & strm);
+    tactic_exception(pp_fn const & fn);
+    optional<proof_state> const & get_proof_state() const { return m_ps; }
 };
 
+#define throw_tactic_exception_if_enabled(ps, msg)  if (ps.report_failure()) throw tactic_exception(msg);
+void throw_no_goal_if_enabled(proof_state const & ps);
+
 typedef lazy_list<proof_state> proof_state_seq;
 
 typedef std::function<proof_state_seq(environment const &, io_state const &, proof_state const &)> tactic;
diff --git a/tests/lean/apply_fail.lean b/tests/lean/apply_fail.lean
new file mode 100644
index 000000000..d8e2ab4d7
--- /dev/null
+++ b/tests/lean/apply_fail.lean
@@ -0,0 +1,4 @@
+example (a b : Prop) : a ∧ b :=
+begin
+  apply or.inr
+end
diff --git a/tests/lean/apply_fail.lean.expected.out b/tests/lean/apply_fail.lean.expected.out
new file mode 100644
index 000000000..63d9908ca
--- /dev/null
+++ b/tests/lean/apply_fail.lean.expected.out
@@ -0,0 +1,13 @@
+apply_fail.lean:3:2: error:invalid 'apply' tactic, failed to unify
+  a ∧ b
+with
+  ?M_1 ∨ ?M_2
+proof state:
+a b : Prop
+⊢ a ∧ b
+apply_fail.lean:4:0: error: don't know how to synthesize placeholder
+a b : Prop
+⊢ a ∧ b
+apply_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+  λ (a b : Prop),
+    ?M_1
diff --git a/tests/lean/assert_fail.lean b/tests/lean/assert_fail.lean
new file mode 100644
index 000000000..04fe26782
--- /dev/null
+++ b/tests/lean/assert_fail.lean
@@ -0,0 +1,10 @@
+example (a b : Prop) (H : b ∧ a) : a ∧ b :=
+begin
+  assert (H : a)
+end
+
+example (a : Prop) (Ha : a) : a :=
+begin
+  exact Ha,
+  assert (H : a)
+end
diff --git a/tests/lean/assert_fail.lean.expected.out b/tests/lean/assert_fail.lean.expected.out
new file mode 100644
index 000000000..00c4ad83b
--- /dev/null
+++ b/tests/lean/assert_fail.lean.expected.out
@@ -0,0 +1,22 @@
+assert_fail.lean:3:2: error:invalid 'assert' tactic, goal already has a hypothesis named 'H'
+proof state:
+a b : Prop,
+H : b ∧ a
+⊢ a ∧ b
+assert_fail.lean:4:0: error: don't know how to synthesize placeholder
+a b : Prop,
+H : b ∧ a
+⊢ a ∧ b
+assert_fail.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+  λ (a b : Prop) (H : b ∧ a),
+    ?M_1
+assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved
+proof state:
+no goals
+assert_fail.lean:10:0: error: don't know how to synthesize placeholder
+a : Prop,
+Ha : a
+⊢ a
+assert_fail.lean:10:0: error: failed to add declaration '14.1' to environment, value has metavariables
+  λ (a : Prop) (Ha : a),
+    ?M_1
diff --git a/tests/lean/beginend_bug.lean.expected.out b/tests/lean/beginend_bug.lean.expected.out
index 665fc426a..1dffbd4aa 100644
--- a/tests/lean/beginend_bug.lean.expected.out
+++ b/tests/lean/beginend_bug.lean.expected.out
@@ -1,4 +1,8 @@
-beginend_bug.lean:7:2: error: tactic failed
+beginend_bug.lean:7:2: error:invalid 'apply' tactic, failed to unify
+  a = ?M_1
+with
+  b = c
+proof state:
 A : Type,
 a b c : A,
 Hab : a = b,
@@ -10,6 +14,12 @@ a b c : A,
 Hab : a = b,
 Hbc : b = c
 ⊢ ?M_1 = c
+beginend_bug.lean:9:0: error: don't know how to synthesize placeholder
+A : Type,
+a b c : A,
+Hab : a = b,
+Hbc : b = c
+⊢ a = c
 beginend_bug.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
   λ (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c),
     ?M_1
diff --git a/tests/lean/gen_bug.lean.expected.out b/tests/lean/gen_bug.lean.expected.out
index fac193206..12b338107 100644
--- a/tests/lean/gen_bug.lean.expected.out
+++ b/tests/lean/gen_bug.lean.expected.out
@@ -1,9 +1,23 @@
-gen_bug.lean:9:2: error: tactic failed
+gen_bug.lean:9:2: error:invalid 'generalize' tactic, type error
+type mismatch at application
+  @heq B b
+term
+  b
+has type
+  B_1
+but is expected to have type
+  B
+proof state:
 A B : Type,
 a : A,
 b : B,
 H : @heq A a B b
 ⊢ @heq B b A a
+gen_bug.lean:12:0: error: don't know how to synthesize placeholder
+A B : Type,
+a : A,
+b : B
+⊢ @heq A a B b → @heq B b A a
 gen_bug.lean:12:0: error: failed to add declaration 'tst' to environment, value has metavariables
   λ (A B : Type) (a : A) (b : B),
     ?M_1
diff --git a/tests/lean/gen_fail.lean b/tests/lean/gen_fail.lean
new file mode 100644
index 000000000..c0bb80a62
--- /dev/null
+++ b/tests/lean/gen_fail.lean
@@ -0,0 +1,7 @@
+import data.vector
+open nat
+
+theorem tst (n : nat) (v : vector nat n) : v = v :=
+begin
+  generalize n,
+end
diff --git a/tests/lean/gen_fail.lean.expected.out b/tests/lean/gen_fail.lean.expected.out
new file mode 100644
index 000000000..cd819f686
--- /dev/null
+++ b/tests/lean/gen_fail.lean.expected.out
@@ -0,0 +1,20 @@
+gen_fail.lean:6:2: error:invalid 'generalize' tactic, type error
+type mismatch at application
+  eq v
+term
+  v
+has type
+  vector ℕ n_1
+but is expected to have type
+  vector ℕ n
+proof state:
+n : ℕ,
+v : vector ℕ n
+⊢ v = v
+gen_fail.lean:7:0: error: don't know how to synthesize placeholder
+n : ℕ,
+v : vector ℕ n
+⊢ v = v
+gen_fail.lean:7:0: error: failed to add declaration 'tst' to environment, value has metavariables
+  λ (n : ℕ) (v : vector ℕ n),
+    ?M_1
diff --git a/tests/lean/revert_fail.lean b/tests/lean/revert_fail.lean
new file mode 100644
index 000000000..09905ee7e
--- /dev/null
+++ b/tests/lean/revert_fail.lean
@@ -0,0 +1,17 @@
+import data.vector
+
+example (A : Type) (n : nat) (v : vector A n) : v = v :=
+begin
+  revert n
+end
+
+example (n : nat) : n = n :=
+begin
+  esimp,
+  revert n
+end
+
+example (n : nat) : n = n :=
+begin
+  revert m
+end
diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out
new file mode 100644
index 000000000..7a1d5a3b5
--- /dev/null
+++ b/tests/lean/revert_fail.lean.expected.out
@@ -0,0 +1,33 @@
+revert_fail.lean:5:2: error:invalid 'revert' tactic, hypothesis 'v' depends on 'n'
+proof state:
+A : Type,
+n : nat,
+v : vector A n
+⊢ v = v
+revert_fail.lean:6:0: error: don't know how to synthesize placeholder
+A : Type,
+n : nat,
+v : vector A n
+⊢ v = v
+revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
+  λ (A : Type) (n : nat) (v : vector A n),
+    ?M_1
+revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+proof state:
+no goals
+revert_fail.lean:12:0: error: don't know how to synthesize placeholder
+n : nat
+⊢ n = n
+revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
+  λ (n : nat),
+    ?M_1
+revert_fail.lean:16:2: error:invalid 'revert' tactic, unknown hypothesis 'm'
+proof state:
+n : nat
+⊢ n = n
+revert_fail.lean:17:0: error: don't know how to synthesize placeholder
+n : nat
+⊢ n = n
+revert_fail.lean:17:0: error: failed to add declaration '14.2' to environment, value has metavariables
+  λ (n : nat),
+    ?M_1
diff --git a/tests/lean/rewrite_fail.lean b/tests/lean/rewrite_fail.lean
new file mode 100644
index 000000000..70476c14c
--- /dev/null
+++ b/tests/lean/rewrite_fail.lean
@@ -0,0 +1,12 @@
+open nat
+
+example (a b : nat) (Ha : a = 0) (Hb : b = 0) : a + b = 0 :=
+begin
+  rewrite [Ha, Ha]
+end
+
+example (a : nat) : a = a :=
+begin
+  esimp,
+  esimp
+end
diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out
new file mode 100644
index 000000000..1ce25ecd3
--- /dev/null
+++ b/tests/lean/rewrite_fail.lean.expected.out
@@ -0,0 +1,23 @@
+rewrite_fail.lean:5:15: error:invalid 'rewrite' tactic, rewrite step failed
+proof state:
+a b : ℕ,
+Ha : a = 0,
+Hb : b = 0
+⊢ 0 + b = 0
+rewrite_fail.lean:6:0: error: don't know how to synthesize placeholder
+a b : ℕ,
+Ha : a = 0,
+Hb : b = 0
+⊢ a + b = 0
+rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, value has metavariables
+  λ (a b : ℕ) (Ha : a = 0) (Hb : b = 0),
+    ?M_1
+rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+proof state:
+no goals
+rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
+a : ℕ
+⊢ a = a
+rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
+  λ (a : ℕ),
+    ?M_1