We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e434766 commit 7df9596Copy full SHA for 7df9596
src/library/ir_interpreter.cpp
@@ -902,6 +902,10 @@ class interpreter {
902
throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module");
903
}
904
push_frame(e.m_decl, m_arg_stack.size());
905
+ // `Unreachable` can be from `mkDummyExternDecl`, which may mean that we failed to run the
906
+ // initializer, suggesting some incorrect `meta` phase setup. Let's make sure we give a
907
+ // better signal than a segfault in that case.
908
+ lean_always_assert(fn_body_tag(decl_fun_body(e.m_decl)) != fn_body_kind::Unreachable);
909
value r = eval_body(decl_fun_body(e.m_decl));
910
pop_frame(r, decl_type(e.m_decl));
911
if (!type_is_scalar(t)) {
0 commit comments