From 150555e03f34f1d60ff2b6d4045c1f91cdc58dbf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 31 Jan 2019 18:18:42 -0800 Subject: [PATCH] chore(library/compiler/emit_cpp): temporarily comment line See new comment to understand motivation for the change. --- src/library/compiler/emit_cpp.cpp | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index b0360ff83a..371a19579e 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -547,8 +547,20 @@ struct emit_fn_fn { else m_out << cidx; } else if (is_enf_unreachable(val)) { - m_out << "lean_unreachable();\n"; - emit_lhs(x); emit_unit(); m_out << ";\n"; + /* We have commented `m_out << "lean_unreachable();\n` because it + may break initialization. The main issue is that `reduce_arity` + creates an auxiliary 0-ary definition for + ``` + def false.elim {C : Sort u} (h : false) : C := .. + ``` + and this auxiliary definition is executed at initialization time. + We should fix the problem by to preventing `reduce_arity` from + converting a n-ary function into a 0-ary one. + Another option is to use lazy initialization, but lazy initialization + would require thread local values. + */ + // m_out << "lean_unreachable();\n"; + emit_lhs(x); emit_unit(); } else { emit_lhs(x); emit_constant(val); }