From 14c33c4e012a22caa008d91a3be9149f6829bc4f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2015 11:59:49 -0700 Subject: [PATCH] feat(kernel/error_msgs): add workaround for issue #669 This issue should fix the new problem reported at #669. It only disables beta-reduction in the pretty printer for application type mismatch at (f n) when f is a lambda expression. --- src/kernel/error_msgs.cpp | 8 ++++++++ src/library/error_handling/error_handling.cpp | 7 +------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 8804c4afd..02e14a13e 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -75,6 +75,14 @@ format pp_app_type_mismatch(formatter const & _fmt, expr const & app, expr const opts = opts.update_if_undef(name{"pp", "implicit"}, true); fmt = fmt.update_options(opts); } + if (is_lambda(get_app_fn(app))) { + // Disable beta reduction in the pretty printer since it will make the error hard to understand. + // See issue https://github.com/leanprover/lean/issues/669 + options opts = fmt.get_options(); + // TODO(Leo): this is hackish, the option is defined in the folder library + opts = opts.update_if_undef(name{"pp", "beta"}, false); + fmt = fmt.update_options(opts); + } expr expected_type = binding_domain(fn_type); std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, expected_type, given_type); if (as_error) diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 903ee2930..66b55bc1a 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -145,12 +145,7 @@ static void display_error(io_state_stream const & ios, pos_info_provider const * } } -void display_error(io_state_stream const & _ios, pos_info_provider const * p, throwable const & ex) { - options opts = _ios.get_options(); - // Disable pp.beta to avoid cryptic error messages. - // See issue https://github.com/leanprover/lean/issues/669 - opts = opts.update_if_undef(get_pp_beta_name(), false); - io_state_stream ios = _ios.update_options(opts); +void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) { flycheck_error err(ios); if (auto k_ex = dynamic_cast(&ex)) { display_error(ios, p, *k_ex);