From f5811d6092e887b00889b60a952df1df7c595a97 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2015 12:42:57 -0700
Subject: [PATCH] feat(frontends/lean): hide subterms that do not contain
 metavariables when generating "unresolved metavariables" error message

closes #473
---
 src/frontends/lean/pp.cpp                   | 69 ++++++++++++++-------
 src/frontends/lean/pp.h                     | 13 ++--
 src/kernel/error_msgs.cpp                   | 14 +++--
 src/kernel/formatter.cpp                    | 17 ++++-
 src/kernel/formatter.h                      |  3 +
 tests/lean/438.lean.expected.out            |  5 +-
 tests/lean/apply_fail.lean.expected.out     |  1 +
 tests/lean/assert_fail.lean.expected.out    |  4 +-
 tests/lean/beginend_bug.lean.expected.out   |  3 +-
 tests/lean/ctx.lean.expected.out            |  3 +-
 tests/lean/gen_bug.lean.expected.out        |  1 +
 tests/lean/gen_fail.lean.expected.out       |  3 +-
 tests/lean/goals1.lean.expected.out         |  3 +-
 tests/lean/inv_del.lean.expected.out        |  3 +-
 tests/lean/open_tst.lean.expected.out       |  2 +
 tests/lean/place_eqn.lean.expected.out      |  4 +-
 tests/lean/pstate.lean.expected.out         |  3 +-
 tests/lean/quasireducible.lean.expected.out |  6 +-
 tests/lean/revert_fail.lean.expected.out    |  5 +-
 tests/lean/rewrite_fail.lean.expected.out   |  4 +-
 20 files changed, 117 insertions(+), 49 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 44eacffb9..a4ff85771 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/typed_expr.h"
 #include "library/num.h"
+#include "library/util.h"
 #include "library/let.h"
 #include "library/print.h"
 #include "library/abbreviation.h"
@@ -278,6 +279,7 @@ void pretty_fn::set_options_core(options const & o) {
     m_beta            = get_pp_beta(o);
     m_numerals        = get_pp_numerals(o);
     m_abbreviations   = get_pp_abbreviations(o);
+    m_hide_full_terms = get_formatter_hide_full_terms(o);
     m_num_nat_coe     = m_numerals && !m_coercion && has_coercion_num_nat(m_env);
 }
 
@@ -314,35 +316,35 @@ bool pretty_fn::is_prop(expr const & e) {
     }
 }
 
-auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result {
+auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
     if (sz == 1) {
-        return pp_child(app_arg(e), max_bp()-1);
+        return pp_child(app_arg(e), max_bp()-1, ignore_hide);
     } else if (is_app(e) && is_implicit(app_fn(e))) {
-        return pp_coercion_fn(app_fn(e), sz-1);
+        return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
     } else {
         expr const & fn = app_fn(e);
-        result res_fn   = pp_coercion_fn(fn, sz-1);
+        result res_fn   = pp_coercion_fn(fn, sz-1, ignore_hide);
         format fn_fmt   = res_fn.fmt();
         if (m_implict && sz == 2 && has_implicit_args(fn))
             fn_fmt = compose(*g_explicit_fmt, fn_fmt);
-        result res_arg  = pp_child(app_arg(e), max_bp());
+        result res_arg  = pp_child(app_arg(e), max_bp(), ignore_hide);
         return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
     }
 }
 
-auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
+auto pretty_fn::pp_coercion(expr const & e, unsigned bp, bool ignore_hide) -> result {
     buffer<expr> args;
     expr const & f = get_app_args(e, args);
     optional<pair<name, unsigned>> r = is_coercion(m_env, f);
     lean_assert(r);
     if (r->second >= args.size()) {
-        return pp_child_core(e, bp);
+        return pp_child_core(e, bp, ignore_hide);
     } else if (r->second == args.size() - 1) {
-        return pp_child(args.back(), bp);
+        return pp_child(args.back(), bp, ignore_hide);
     } else {
         unsigned sz = args.size() - r->second;
         lean_assert(sz >= 2);
-        auto r = pp_coercion_fn(e, sz);
+        auto r = pp_coercion_fn(e, sz, ignore_hide);
         if (r.rbp() < bp) {
             return result(paren(r.fmt()));
         } else {
@@ -351,8 +353,8 @@ auto pretty_fn::pp_coercion(expr const & e, unsigned bp) -> result {
     }
 }
 
-auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
-    result r = pp(e);
+auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> result {
+    result r = pp(e, ignore_hide);
     if (r.rbp() < bp) {
         return result(paren(r.fmt()));
     } else {
@@ -360,20 +362,20 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp) -> result {
     }
 }
 
-auto pretty_fn::pp_child(expr const & e, unsigned bp) -> result {
+auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
     if (auto it = is_abbreviated(e))
-        return pp_abbreviation(e, *it, false);
+        return pp_abbreviation(e, *it, false, ignore_hide);
     if (is_app(e)) {
         expr const & f = app_fn(e);
         if (auto it = is_abbreviated(f)) {
-            return pp_abbreviation(e, *it, true);
+            return pp_abbreviation(e, *it, true, ignore_hide);
         } else if (is_implicit(f)) {
-            return pp_child(f, bp);
+            return pp_child(f, bp, ignore_hide);
         } else if (!m_coercion && is_coercion(m_env, f)) {
-            return pp_coercion(e, bp);
+            return pp_coercion(e, bp, ignore_hide);
         }
     }
-    return pp_child_core(e, bp);
+    return pp_child_core(e, bp, ignore_hide);
 }
 
 auto pretty_fn::pp_var(expr const & e) -> result {
@@ -490,8 +492,13 @@ auto pretty_fn::pp_app(expr const & e) -> result {
     expr const & fn = app_fn(e);
     if (auto it = is_abbreviated(fn))
         return pp_abbreviation(e, *it, true);
-    result res_fn = pp_child(fn, max_bp()-1);
-    format fn_fmt = res_fn.fmt();
+    // If the application contains a metavariable, then we want to
+    // show the function, otherwise it would be hard to understand the
+    // context where the metavariable occurs. This is hack to implement
+    // formatter.hide_full_terms
+    bool ignore_hide = true;
+    result res_fn    = pp_child(fn, max_bp()-1, ignore_hide);
+    format fn_fmt    = res_fn.fmt();
     if (m_implict && !is_app(fn) && has_implicit_args(fn))
         fn_fmt = compose(*g_explicit_fmt, fn_fmt);
     result res_arg = pp_child(app_arg(e), max_bp());
@@ -1056,7 +1063,7 @@ auto pretty_fn::pp_notation(expr const & e) -> optional<result> {
     return optional<result>();
 }
 
-auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn) -> result {
+auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide) -> result {
     declaration const & d = m_env.get(abbrev);
     unsigned num_univs    = d.get_num_univ_params();
     buffer<level> ls;
@@ -1065,12 +1072,28 @@ auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn) ->
     buffer<expr> args;
     if (fn)
         get_app_args(e, args);
-    return pp(mk_app(mk_constant(abbrev, to_list(ls)), args));
+    return pp(mk_app(mk_constant(abbrev, to_list(ls)), args), ignore_hide);
 }
 
-auto pretty_fn::pp(expr const & e) -> result {
-    if (m_depth > m_max_depth || m_num_steps > m_max_steps)
+static bool is_pp_atomic(expr const & e) {
+    switch (e.kind()) {
+    case expr_kind::App:
+    case expr_kind::Lambda:
+    case expr_kind::Pi:
+    case expr_kind::Macro:
+        return false;
+    default:
+        return true;
+    }
+}
+
+auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
+    if ((m_depth >= m_max_depth ||
+         m_num_steps > m_max_steps ||
+         (m_hide_full_terms && !ignore_hide && !has_expr_metavar_relaxed(e))) &&
+        !is_pp_atomic(e)) {
         return result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt);
+    }
     flet<unsigned> let_d(m_depth, m_depth+1);
     m_num_steps++;
 
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index b581d411f..e10f5ba3e 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -67,6 +67,7 @@ private:
     bool                m_beta;
     bool                m_numerals;
     bool                m_abbreviations;
+    bool                m_hide_full_terms;
 
     name mk_metavar_name(name const & m);
     name mk_local_name(name const & n, name const & suggested);
@@ -88,10 +89,10 @@ private:
     optional<result> pp_notation(notation_entry const & entry, buffer<optional<expr>> & args);
     optional<result> pp_notation(expr const & e);
 
-    result pp_coercion_fn(expr const & e, unsigned sz);
-    result pp_coercion(expr const & e, unsigned bp);
-    result pp_child_core(expr const & e, unsigned bp);
-    result pp_child(expr const & e, unsigned bp);
+    result pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide = false);
+    result pp_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
+    result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);
+    result pp_child(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_var(expr const & e);
     result pp_sort(expr const & e);
     result pp_const(expr const & e);
@@ -107,12 +108,12 @@ private:
     result pp_let(expr e);
     result pp_num(mpz const & n);
     // If fn is true, then \c e is of the form (f a), and the abbreviation is \c f.
-    result pp_abbreviation(expr const & e, name const & abbrev, bool fn);
+    result pp_abbreviation(expr const & e, name const & abbrev, bool fn, bool ignore_hide = false);
     void set_options_core(options const & o);
 
 public:
     pretty_fn(environment const & env, options const & o);
-    result pp(expr const & e);
+    result pp(expr const & e, bool ignore_hide = false);
     void set_options(options const & o);
     options const & get_options() const { return m_options; }
     format operator()(expr const & e);
diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp
index 2abf4e64a..a50ce3a93 100644
--- a/src/kernel/error_msgs.cpp
+++ b/src/kernel/error_msgs.cpp
@@ -91,7 +91,9 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const &
 }
 
 static format pp_until_meta_visible(formatter const & fmt, expr const & e, list<options> extra) {
-    formatter fmt1 = fmt;
+    options o = fmt.get_options();
+    o = o.update_if_undef(get_formatter_hide_full_terms_name(), true);
+    formatter fmt1 = fmt.update_options(o);
     while (true) {
         format r = pp_indent_expr(fmt1, e);
         std::ostringstream out;
@@ -99,9 +101,10 @@ static format pp_until_meta_visible(formatter const & fmt, expr const & e, list<
         if (out.str().find("?M") != std::string::npos)
             return r;
         if (!extra)
-            return pp_indent_expr(fmt, e);
-        options o = join(head(extra), fmt.get_options());
-        fmt1  = fmt.update_options(o);
+            return pp_indent_expr(fmt.update_options(o), e);
+        options o2 = join(head(extra), fmt.get_options());
+        o2    = o2.update_if_undef(get_formatter_hide_full_terms_name(), true);
+        fmt1  = fmt.update_options(o2);
         extra = tail(extra);
     }
 }
@@ -119,6 +122,9 @@ format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const &
     else
         r += format("value");
     r += format(" has metavariables");
+    options const & o = fmt.get_options();
+    if (!o.contains(get_formatter_hide_full_terms_name()))
+        r += line() + format("remark: set 'formatter.hide_full_terms' to false to see the complete term");
     r += pp_until_meta_visible(fmt, e);
     return r;
 }
diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index a7a10df5a..04b14276c 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -5,9 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
+#include "util/sexpr/option_declarations.h"
 #include "kernel/formatter.h"
 
+#ifndef LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS
+#define LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS false
+#endif
+
 namespace lean {
+static name * g_formatter_hide_full = nullptr;
+
+name const & get_formatter_hide_full_terms_name() { return *g_formatter_hide_full; }
+bool get_formatter_hide_full_terms(options const & opts) { return opts.get_bool(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS); }
+
 static std::function<void(std::ostream &, expr const & e)> * g_print = nullptr;
 
 void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn) {
@@ -27,9 +37,14 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
 
 void print(lean::expr const & a) { std::cout << a << std::endl; }
 
-void initialize_formatter() {}
+void initialize_formatter() {
+    g_formatter_hide_full = new name{"formatter", "hide_full_terms"};
+    register_bool_option(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS,
+                         "(formatter) replace terms which do not contain metavariables with `...`");
+}
 
 void finalize_formatter() {
+    delete g_formatter_hide_full;
     if (g_print)
         delete g_print;
 }
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index f0fdba7c3..ec2f3939a 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -13,6 +13,9 @@ namespace lean {
 class expr;
 class environment;
 
+name const & get_formatter_hide_full_terms_name();
+bool get_formatter_hide_full_terms(options const & opts);
+
 class formatter {
     std::function<format(expr const &, options const &)> m_fn;
     options                             m_options;
diff --git a/tests/lean/438.lean.expected.out b/tests/lean/438.lean.expected.out
index 9028f72f5..a25800c7f 100644
--- a/tests/lean/438.lean.expected.out
+++ b/tests/lean/438.lean.expected.out
@@ -11,5 +11,6 @@ P₀ : Type,
 P : group P₀
 ⊢ ?M_1
 438.lean:10:2: error: failed to add declaration 'lambda_morphism.mk' to environment, type has metavariables
-  Π {P₀ : Type} {P : group P₀},
-    ?M_2 = ?M_3 → lambda_morphism P₀ P
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  Π {P₀ : Type} {P : …},
+    ?M_2 = ?M_3 → …
diff --git a/tests/lean/apply_fail.lean.expected.out b/tests/lean/apply_fail.lean.expected.out
index 63d9908ca..5ea45ee6d 100644
--- a/tests/lean/apply_fail.lean.expected.out
+++ b/tests/lean/apply_fail.lean.expected.out
@@ -9,5 +9,6 @@ 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
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : Prop),
     ?M_1
diff --git a/tests/lean/assert_fail.lean.expected.out b/tests/lean/assert_fail.lean.expected.out
index 00c4ad83b..0e0901e43 100644
--- a/tests/lean/assert_fail.lean.expected.out
+++ b/tests/lean/assert_fail.lean.expected.out
@@ -8,7 +8,8 @@ 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),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop) (H : …),
     ?M_1
 assert_fail.lean:9:2: error:invalid tactic, there are no goals to be solved
 proof state:
@@ -18,5 +19,6 @@ a : Prop,
 Ha : a
 ⊢ a
 assert_fail.lean:10:0: error: failed to add declaration '14.1' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (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 1dffbd4aa..dbe18db7d 100644
--- a/tests/lean/beginend_bug.lean.expected.out
+++ b/tests/lean/beginend_bug.lean.expected.out
@@ -21,5 +21,6 @@ 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),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
     ?M_1
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index 76c785599..626c414f0 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -6,5 +6,6 @@ h : A = B,
 p1 p2 : A × B
 ⊢ nat
 ctx.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
-  λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : A = B) (p1 p2 : A × B),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A B : Type) (a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat) (b1 b2 b3 : bool) (h : …) (p1 p2 : …),
     ?M_1
diff --git a/tests/lean/gen_bug.lean.expected.out b/tests/lean/gen_bug.lean.expected.out
index 12b338107..436f8c980 100644
--- a/tests/lean/gen_bug.lean.expected.out
+++ b/tests/lean/gen_bug.lean.expected.out
@@ -19,5 +19,6 @@ 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
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A B : Type) (a : A) (b : B),
     ?M_1
diff --git a/tests/lean/gen_fail.lean.expected.out b/tests/lean/gen_fail.lean.expected.out
index cd819f686..a02aeab25 100644
--- a/tests/lean/gen_fail.lean.expected.out
+++ b/tests/lean/gen_fail.lean.expected.out
@@ -16,5 +16,6 @@ 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),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (n : ℕ) (v : …),
     ?M_1
diff --git a/tests/lean/goals1.lean.expected.out b/tests/lean/goals1.lean.expected.out
index 9b2ff3931..1d1c65621 100644
--- a/tests/lean/goals1.lean.expected.out
+++ b/tests/lean/goals1.lean.expected.out
@@ -5,5 +5,6 @@ Hab : eq a b,
 Hbc : eq b c
 ⊢ eq b c
 goals1.lean:9:0: error: failed to add declaration 'foo' to environment, value has metavariables
-  λ (A : Type) (a b c : A) (Hab : eq a b) (Hbc : eq b c),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (a b c : A) (Hab : …) (Hbc : …),
     ?M_1
diff --git a/tests/lean/inv_del.lean.expected.out b/tests/lean/inv_del.lean.expected.out
index e2b6174d9..fe8d7736b 100644
--- a/tests/lean/inv_del.lean.expected.out
+++ b/tests/lean/inv_del.lean.expected.out
@@ -5,5 +5,6 @@ H : Π (a : A), P (vone a),
 a : A
 ⊢ P (vone a)
 inv_del.lean:15:2: error: failed to add declaration 'vec.eone' to environment, value has metavariables
-  λ (A : Type) (P : vec A 1 → Type) (H : Π (a : A), P (vone a)) (v : vec A 1),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (P : …) (H : …) (v : …),
     ?M_1
diff --git a/tests/lean/open_tst.lean.expected.out b/tests/lean/open_tst.lean.expected.out
index 9e9beb5c6..75dd74a81 100644
--- a/tests/lean/open_tst.lean.expected.out
+++ b/tests/lean/open_tst.lean.expected.out
@@ -17,6 +17,7 @@ open_tst.lean:22:2: error: don't know how to synthesize placeholder
 
 ⊢ inhabited ℕ
 open_tst.lean:22:2: error: failed to add declaration 'foo1' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
 a + a : ℕ
 open_tst.lean:29:8: error: unknown identifier 'add'
@@ -25,5 +26,6 @@ open_tst.lean:32:2: error: don't know how to synthesize placeholder
 
 ⊢ inhabited ℕ
 open_tst.lean:32:2: error: failed to add declaration 'foo2' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
 open_tst.lean:41:10: error: invalid expression
diff --git a/tests/lean/place_eqn.lean.expected.out b/tests/lean/place_eqn.lean.expected.out
index 8d45277e2..aebf76354 100644
--- a/tests/lean/place_eqn.lean.expected.out
+++ b/tests/lean/place_eqn.lean.expected.out
@@ -6,7 +6,7 @@ foo : ℕ → ℕ,
 a : ℕ
 ⊢ ℕ
 place_eqn.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : ℕ),
     nat.brec_on a
-      (λ (a_1 : ℕ) (b : nat.below a_1),
-         nat.cases_on a_1 (λ (b_1 : nat.below 0), ?M_1) (λ (a_2 : ℕ) (b_1 : nat.below (succ a_2)), ?M_2) b)
+      (λ (a_1 : ℕ) (b : …), nat.cases_on a_1 (λ (b_1 : …), ?M_1) (λ (a_2 : ℕ) (b_1 : …), ?M_2) b)
diff --git a/tests/lean/pstate.lean.expected.out b/tests/lean/pstate.lean.expected.out
index b902706f7..7253037ab 100644
--- a/tests/lean/pstate.lean.expected.out
+++ b/tests/lean/pstate.lean.expected.out
@@ -5,5 +5,6 @@ h₁ : a = b,
 h₂ : b = c
 ⊢ b = c
 pstate.lean:4:7: error: failed to add declaration 'foo' to environment, value has metavariables
-  λ (A : Type) (a b c : A) (h₁ : a = b) (h₂ : b = c),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (a b c : A) (h₁ : …) (h₂ : …),
     eq.trans h₁ ?M_1
diff --git a/tests/lean/quasireducible.lean.expected.out b/tests/lean/quasireducible.lean.expected.out
index a84991154..a624fd90e 100644
--- a/tests/lean/quasireducible.lean.expected.out
+++ b/tests/lean/quasireducible.lean.expected.out
@@ -10,7 +10,8 @@ a : nat,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:11:3: error: failed to add declaration '14.1' to environment, value has metavariables
-  λ (a : nat) (H : f a = a),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a : nat) (H : …),
     ?M_1
 quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern
   f a
@@ -24,5 +25,6 @@ a : nat,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:16:3: error: failed to add declaration '14.2' to environment, value has metavariables
-  λ (a : nat) (H : f a = a),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a : nat) (H : …),
     ?M_1
diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out
index 7a1d5a3b5..6ac2c7c0d 100644
--- a/tests/lean/revert_fail.lean.expected.out
+++ b/tests/lean/revert_fail.lean.expected.out
@@ -10,7 +10,8 @@ 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),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (n : nat) (v : …),
     ?M_1
 revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
 proof state:
@@ -19,6 +20,7 @@ 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
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),
     ?M_1
 revert_fail.lean:16:2: error:invalid 'revert' tactic, unknown hypothesis 'm'
@@ -29,5 +31,6 @@ 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
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),
     ?M_1
diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out
index 522a6790e..2ecd71ab4 100644
--- a/tests/lean/rewrite_fail.lean.expected.out
+++ b/tests/lean/rewrite_fail.lean.expected.out
@@ -12,7 +12,8 @@ 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),
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : ℕ) (Ha : …) (Hb : …),
     ?M_1
 rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
 proof state:
@@ -21,5 +22,6 @@ 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
+remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : ℕ),
     ?M_1