feat(library/tactic/rewrite_tactic): disable pp.beta at rewrite error msg

library/init/nat_lemmas.lean

@@ -36,8 +36,6 @@ namespace nat
   | n m 0        := rfl
   | n m (succ k) := by simp [add_succ, add_assoc n m k]
 
-  set_option trace.app_builder true
-
   protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
   | 0        m k := by ctx_simp [nat.zero_add]
   | (succ n) m k := λ h,

src/library/tactic/rewrite_tactic.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/app_builder.h"
 #include "library/constants.h"
 #include "library/trace.h"
+#include "library/pp_options.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
 #include "library/vm/vm_nat.h"
@@ -64,12 +65,13 @@ vm_obj rewrite(transparency_mode const & m, bool use_instances, occurrences cons
     expr pattern = target ? lhs : rhs;
     expr e_abst  = kabstract(ctx, e, pattern, occs);
     if (closed(e_abst)) {
+        auto new_s = update_option_if_undef(s, get_pp_beta_name(), false);
         auto thunk = [=]() {
             format msg = format("rewrite tactic failed, did not find instance of the pattern in the target expression");
-            msg += pp_indented_expr(s, pattern);
+            msg += pp_indented_expr(new_s, pattern);
             return msg;
         };
-        return mk_tactic_exception(thunk, s);
+        return mk_tactic_exception(thunk, new_s);
     }
     /* Synthesize type class instances */
     if (use_instances) {

src/library/tactic/tactic_state.h

@@ -96,6 +96,9 @@ tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
 
    \remark It returns s is is_eqp(s.mctx(), mctx) and is_decl_eqp(s.get_main_goal_decl()->get_context(), lctx) */
 tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx);
+template<typename T> tactic_state update_option_if_undef(tactic_state const & s, name const & n, T v) {
+    return set_options(s, s.get_options().update_if_undef(n, v));
+}
 
 bool is_tactic_state(vm_obj const & o);
 tactic_state const & to_tactic_state(vm_obj const & o);

tests/lean/bad_error2.lean

@@ -0,0 +1,11 @@
+open nat
+
+example {k n m : ℕ} (h : k + n ≤ k + m) : n ≤ m :=
+match le.elim h with
+| ⟨w, hw⟩ := @le.intro _ _ w
+    begin
+      -- in the following error pp.beta is automatically disabled
+      rw [nat.add_assoc] at hw,
+      apply nat.add_left_cancel hw
+    end
+end

tests/lean/bad_error2.lean.expected.out

@@ -0,0 +1,9 @@
+bad_error2.lean:8:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression
+  ?m_1 + ?m_2 + ?m_3
+state:
+k n m : ℕ,
+h : k + n ≤ k + m,
+_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
+w : ℕ,
+hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
+⊢ n + w = m