feat(library/tactic): produce better error message when a tactic fails

closes #348

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 elaborator::try_using(substitution & subst, expr const & mvar, proof_state const & ps,
-                           bool show_failure) {
+                           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) {
+        if (show_failure)
-            auto out = regular(env(), ios());
+            display_tactic_exception(ex, ps, pre_tac);
-            display_error_pos(out, pip(), ex.get_expr());
-            out << " tactic failed: " << ex.what() << "\n";
-        }
         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_tactic_exception(ex, ps, ptac);
-                display_error_pos(out, pip(), ex.get_expr());
-                out << " tactic failed: " << ex.what() << "\n";
                 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;
             }
         }

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 try_using(substitution & subst, expr const & mvar, proof_state const & ps,
-                   bool show_failure);
+                   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);

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;

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();
                 }

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)) {

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, char const * msg):exception(msg), m_expr(e) {}
-    expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {}
+    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 *)>

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();
                 }
 

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);

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;

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();
         }
     };

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);
         });
 }

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(char const * msg, optional<expr> const & m, pp_fn const & fn):
-tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
+    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) {

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 {
+class tactic_exception : public generic_exception {
-    expr m_expr;
+    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;

tests/lean/apply_fail.lean

@@ -0,0 +1,4 @@
+example (a b : Prop) : a ∧ b :=
+begin
+  apply or.inr
+end

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

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

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

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

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

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

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

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

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

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

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