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

feat(frontends/lean/elaborator): better error localization when running out of stack space and/or memory in begin-end tactic mode.

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-26 20:09:15 -07:00
parent c4ec89ae6d
commit 4d1b711247
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/elaborator.cpp
View file

@ -1847,6 +1847,15 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
} catch (tactic_exception & ex) { } catch (tactic_exception & ex) {
display_tactic_exception(ex, ps, ptac); display_tactic_exception(ex, ps, ptac);
return false; return false;
} catch (exception &) {
throw;
} catch (throwable & ex) {
auto out = regular(env(), ios());
flycheck_error err(out);
display_error_pos(out, pip(), ptac);
out << ex.what() << "\nproof state:\n";
out << ps.pp(env(), ios()) << "\n";
return false;
} }
} else { } else {
return false; return false;