max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/parser): fix spurious "uses 'sorry'" messages

Browse source
This commit is contained in:
Sebastian Ullrich 2016-11-03 23:42:09 +01:00 • committed by Leonardo de Moura
parent 9465f25f09
commit eb599481b9
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/parser.cpp
View file

@ -2128,6 +2128,14 @@ void parser::parse_imports() {
m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
m_env = replay_export_decls_core(m_env, m_ios);
check_modules_up_to_date();
if (has_sorry(m_env)) {
#ifndef LEAN_IGNORE_SORRY
// TODO(Leo): remove the #ifdef.
// The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
// We use it to avoid a buch of warnings on cdash.
(mk_message(m_last_cmd_pos, WARNING) << "imported file uses 'sorry'").report();
#endif
}
m_imports_parsed = true;
if (olean_files.size())
save_snapshot();
@ -2156,14 +2164,6 @@ bool parser::parse_commands() {
// Only parse imports when we are at the beginning, i.e. not when starting from a snapshot.
if (!m_imports_parsed)
protected_call([&]() { parse_imports(); }, [&]() { sync_command(); });
if (has_sorry(m_env)) {
#ifndef LEAN_IGNORE_SORRY
// TODO(Leo): remove the #ifdef.
// The compilation option LEAN_IGNORE_SORRY is a temporary hack for the nightly builds
// We use it to avoid a buch of warnings on cdash.
(mk_message(WARNING) << "imported file uses 'sorry'").report();
#endif
}
while (!done) {
if (m_stop_at && pos().first > m_stop_at_line) {
throw interrupt_parser();