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

chore(frontends/lean/elaborator,library/compiler/compiler): avoid error recovery errors

Browse source
This commit is contained in:
Sebastian Ullrich 2018-11-12 15:33:28 +01:00
parent 2271d4bccc
commit 2f8e6cc975
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2647,6 +2647,9 @@ expr elaborator::visit_equations(expr const & e) {
}
new_e = instantiate_mvars(new_e);
ensure_no_unassigned_metavars(new_e);
if (has_sorry(new_e))
// aborting here prevents many additional errors
throw elaborator_exception(e, "[abort visit_equation]").ignore_if(true);
metavar_context mctx = m_ctx.mctx();
expr r = compile_equations(m_env, *this, mctx, m_ctx.lctx(), new_e);
m_ctx.set_env(m_env);

3
src/library/compiler/compiler.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "library/max_sharing.h"
#include "library/trace.h"
#include "library/sorry.h"
#include "library/vm/vm.h"
#include "library/compiler/util.h"
#include "library/compiler/lcnf.h"
@ -92,7 +93,7 @@ environment compile(environment const & env, options const & opts, names const &
return env;
for (name const & c : cs) {
if (!env.get(c).is_definition() || is_vm_builtin_function(c))
if (!env.get(c).is_definition() || is_vm_builtin_function(c) || has_sorry(env.get(c).get_value()))
return env;
}