michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/error_msgs): add workaround for issue #669

Browse source 
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.
This commit is contained in:
Leonardo de Moura 2015-06-17 11:59:49 -07:00
parent d12b5613c6
commit 14c33c4e01
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/error_msgs.cpp
View file

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

7
src/library/error_handling/error_handling.cpp
View file

@ -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<kernel_exception const *>(&ex)) {
display_error(ios, p, *k_ex);