From 08f3459ea3ccba2ff57c51ed8ec8f606c1d7556b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Mar 2019 14:53:33 -0700 Subject: [PATCH] fix(library/compiler/emit_cpp): stop initialization when error is reported --- src/library/compiler/emit_cpp.cpp | 1 + src/stage0/init/coe.cpp | 1 + src/stage0/init/control/alternative.cpp | 2 ++ src/stage0/init/control/applicative.cpp | 1 + src/stage0/init/control/combinators.cpp | 4 ++++ src/stage0/init/control/default.cpp | 11 +++++++++++ src/stage0/init/control/estate.cpp | 2 ++ src/stage0/init/control/except.cpp | 4 ++++ src/stage0/init/control/functor.cpp | 2 ++ src/stage0/init/control/id.cpp | 1 + src/stage0/init/control/lift.cpp | 3 +++ src/stage0/init/control/monad.cpp | 1 + src/stage0/init/control/monad_fail.cpp | 2 ++ src/stage0/init/control/option.cpp | 3 +++ src/stage0/init/control/reader.cpp | 4 ++++ src/stage0/init/control/state.cpp | 4 ++++ src/stage0/init/data/array/basic.cpp | 6 ++++++ src/stage0/init/data/array/default.cpp | 1 + src/stage0/init/data/basic.cpp | 10 ++++++++++ src/stage0/init/data/char/basic.cpp | 1 + src/stage0/init/data/char/default.cpp | 1 + src/stage0/init/data/default.cpp | 14 ++++++++++++++ src/stage0/init/data/dlist.cpp | 2 ++ src/stage0/init/data/fin/basic.cpp | 2 ++ src/stage0/init/data/fin/default.cpp | 1 + src/stage0/init/data/hashable.cpp | 2 ++ src/stage0/init/data/hashmap/basic.cpp | 4 ++++ src/stage0/init/data/int/basic.cpp | 5 +++++ src/stage0/init/data/int/default.cpp | 1 + src/stage0/init/data/list/basic.cpp | 2 ++ src/stage0/init/data/list/default.cpp | 2 ++ src/stage0/init/data/list/instances.cpp | 3 +++ src/stage0/init/data/nat/basic.cpp | 1 + src/stage0/init/data/nat/bitwise.cpp | 3 +++ src/stage0/init/data/nat/default.cpp | 3 +++ src/stage0/init/data/nat/div.cpp | 2 ++ src/stage0/init/data/option/basic.cpp | 4 ++++ src/stage0/init/data/option/instances.cpp | 1 + src/stage0/init/data/ordering/basic.cpp | 1 + src/stage0/init/data/ordering/default.cpp | 1 + src/stage0/init/data/rbmap/basic.cpp | 3 +++ src/stage0/init/data/rbmap/default.cpp | 2 ++ src/stage0/init/data/rbtree/basic.cpp | 1 + src/stage0/init/data/rbtree/default.cpp | 1 + src/stage0/init/data/repr.cpp | 3 +++ src/stage0/init/data/string/basic.cpp | 3 +++ src/stage0/init/data/string/default.cpp | 1 + src/stage0/init/data/to_string.cpp | 4 ++++ src/stage0/init/data/uint.cpp | 2 ++ src/stage0/init/default.cpp | 10 ++++++++++ src/stage0/init/fix.cpp | 1 + src/stage0/init/function.cpp | 1 + src/stage0/init/io.cpp | 3 +++ src/stage0/init/lean/compiler/const_folding.cpp | 3 +++ src/stage0/init/lean/compiler/default.cpp | 1 + src/stage0/init/lean/compiler/ir.cpp | 3 +++ src/stage0/init/lean/compiler/util.cpp | 1 + src/stage0/init/lean/config.cpp | 1 + src/stage0/init/lean/declaration.cpp | 1 + src/stage0/init/lean/default.cpp | 3 +++ src/stage0/init/lean/disjoint_set.cpp | 1 + src/stage0/init/lean/elaborator.cpp | 4 ++++ src/stage0/init/lean/expander.cpp | 2 ++ src/stage0/init/lean/expr.cpp | 2 ++ src/stage0/init/lean/extern.cpp | 2 ++ src/stage0/init/lean/format.cpp | 3 +++ src/stage0/init/lean/frontend.cpp | 6 ++++++ src/stage0/init/lean/kvmap.cpp | 2 ++ src/stage0/init/lean/level.cpp | 2 ++ src/stage0/init/lean/message.cpp | 2 ++ src/stage0/init/lean/name.cpp | 8 ++++++++ src/stage0/init/lean/name_mangling.cpp | 2 ++ src/stage0/init/lean/options.cpp | 1 + src/stage0/init/lean/parser/basic.cpp | 7 +++++++ src/stage0/init/lean/parser/combinators.cpp | 2 ++ src/stage0/init/lean/parser/command.cpp | 1 + src/stage0/init/lean/parser/declaration.cpp | 1 + src/stage0/init/lean/parser/identifier.cpp | 2 ++ src/stage0/init/lean/parser/level.cpp | 1 + src/stage0/init/lean/parser/module.cpp | 1 + src/stage0/init/lean/parser/notation.cpp | 1 + src/stage0/init/lean/parser/parsec.cpp | 9 +++++++++ src/stage0/init/lean/parser/pratt.cpp | 1 + src/stage0/init/lean/parser/rec.cpp | 2 ++ src/stage0/init/lean/parser/string_literal.cpp | 1 + src/stage0/init/lean/parser/syntax.cpp | 2 ++ src/stage0/init/lean/parser/term.cpp | 3 +++ src/stage0/init/lean/parser/token.cpp | 2 ++ src/stage0/init/lean/parser/trie.cpp | 2 ++ src/stage0/init/lean/position.cpp | 3 +++ src/stage0/init/lean/trace.cpp | 5 +++++ src/stage0/init/lean/util.cpp | 2 ++ src/stage0/init/platform.cpp | 1 + src/stage0/init/util.cpp | 1 + src/stage0/init/wf.cpp | 1 + 95 files changed, 255 insertions(+) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 3e496bac93..f8346d06d9 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -1070,6 +1070,7 @@ static void emit_initialize(std::ostream & out, environment const & env, module_ out << " if (_G_initialized) return w;\n"; out << " _G_initialized = true;\n"; for (module_name const & d : deps) { + out << "if (io_result_is_error(w)) return w;\n"; out << "w = initialize_" << mangle(d, false) << "(w);\n"; } comp_decls ds = get_llnf_code(env); diff --git a/src/stage0/init/coe.cpp b/src/stage0/init/coe.cpp index 994da2cf1e..2b0a096400 100644 --- a/src/stage0/init/coe.cpp +++ b/src/stage0/init/coe.cpp @@ -950,6 +950,7 @@ static bool _G_initialized = false; obj* initialize_init_coe(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); l_coe__bool__to__Prop = _init_l_coe__bool__to__Prop(); l_coe__sort__bool = _init_l_coe__sort__bool(); diff --git a/src/stage0/init/control/alternative.cpp b/src/stage0/init/control/alternative.cpp index a46dfe0995..f1790d15d2 100644 --- a/src/stage0/init/control/alternative.cpp +++ b/src/stage0/init/control/alternative.cpp @@ -364,7 +364,9 @@ static bool _G_initialized = false; obj* initialize_init_control_alternative(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_applicative(w); l_optional___rarg___closed__1 = _init_l_optional___rarg___closed__1(); lean::mark_persistent(l_optional___rarg___closed__1); diff --git a/src/stage0/init/control/applicative.cpp b/src/stage0/init/control/applicative.cpp index f860cd771c..ac0f1df1d8 100644 --- a/src/stage0/init/control/applicative.cpp +++ b/src/stage0/init/control/applicative.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_control_applicative(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_functor(w); return w; } diff --git a/src/stage0/init/control/combinators.cpp b/src/stage0/init/control/combinators.cpp index d0b468655e..2cc1c36944 100644 --- a/src/stage0/init/control/combinators.cpp +++ b/src/stage0/init/control/combinators.cpp @@ -1514,9 +1514,13 @@ static bool _G_initialized = false; obj* initialize_init_control_combinators(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_monad(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); l_mjoin___rarg___closed__1 = _init_l_mjoin___rarg___closed__1(); lean::mark_persistent(l_mjoin___rarg___closed__1); diff --git a/src/stage0/init/control/default.cpp b/src/stage0/init/control/default.cpp index 181a52a0c2..2e0fdbc3f6 100644 --- a/src/stage0/init/control/default.cpp +++ b/src/stage0/init/control/default.cpp @@ -29,16 +29,27 @@ static bool _G_initialized = false; obj* initialize_init_control_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_applicative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_functor(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_state(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_id(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_reader(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_option(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_combinators(w); return w; } diff --git a/src/stage0/init/control/estate.cpp b/src/stage0/init/control/estate.cpp index 6790f96460..3b57b36101 100644 --- a/src/stage0/init/control/estate.cpp +++ b/src/stage0/init/control/estate.cpp @@ -1575,7 +1575,9 @@ static bool _G_initialized = false; obj* initialize_init_control_estate(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_state(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); l_estate_result_to__string___main___rarg___closed__1 = _init_l_estate_result_to__string___main___rarg___closed__1(); lean::mark_persistent(l_estate_result_to__string___main___rarg___closed__1); diff --git a/src/stage0/init/control/except.cpp b/src/stage0/init/control/except.cpp index f3a5746385..5347ca8e52 100644 --- a/src/stage0/init/control/except.cpp +++ b/src/stage0/init/control/except.cpp @@ -3260,9 +3260,13 @@ static bool _G_initialized = false; obj* initialize_init_control_except(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad__fail(w); l_except_to__string___main___rarg___closed__1 = _init_l_except_to__string___main___rarg___closed__1(); lean::mark_persistent(l_except_to__string___main___rarg___closed__1); diff --git a/src/stage0/init/control/functor.cpp b/src/stage0/init/control/functor.cpp index 0fc1c98916..46a3aeb6ae 100644 --- a/src/stage0/init/control/functor.cpp +++ b/src/stage0/init/control/functor.cpp @@ -104,7 +104,9 @@ static bool _G_initialized = false; obj* initialize_init_control_functor(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); +if (io_result_is_error(w)) return w; w = initialize_init_function(w); return w; } diff --git a/src/stage0/init/control/id.cpp b/src/stage0/init/control/id.cpp index 899541da08..cc35849a55 100644 --- a/src/stage0/init/control/id.cpp +++ b/src/stage0/init/control/id.cpp @@ -184,6 +184,7 @@ static bool _G_initialized = false; obj* initialize_init_control_id(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); l_id_monad = _init_l_id_monad(); lean::mark_persistent(l_id_monad); diff --git a/src/stage0/init/control/lift.cpp b/src/stage0/init/control/lift.cpp index 92a00d378d..bcdf584c2b 100644 --- a/src/stage0/init/control/lift.cpp +++ b/src/stage0/init/control/lift.cpp @@ -234,8 +234,11 @@ static bool _G_initialized = false; obj* initialize_init_control_lift(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_function(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad(w); return w; } diff --git a/src/stage0/init/control/monad.cpp b/src/stage0/init/control/monad.cpp index f24f278140..1b9725ff11 100644 --- a/src/stage0/init/control/monad.cpp +++ b/src/stage0/init/control/monad.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_control_monad(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_applicative(w); return w; } diff --git a/src/stage0/init/control/monad_fail.cpp b/src/stage0/init/control/monad_fail.cpp index 4e516e297e..e4b71b789f 100644 --- a/src/stage0/init/control/monad_fail.cpp +++ b/src/stage0/init/control/monad_fail.cpp @@ -100,7 +100,9 @@ static bool _G_initialized = false; obj* initialize_init_control_monad__fail(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); l_match__failed___rarg___closed__1 = _init_l_match__failed___rarg___closed__1(); lean::mark_persistent(l_match__failed___rarg___closed__1); diff --git a/src/stage0/init/control/option.cpp b/src/stage0/init/control/option.cpp index 51e3b70e25..09d8fbe44b 100644 --- a/src/stage0/init/control/option.cpp +++ b/src/stage0/init/control/option.cpp @@ -2120,8 +2120,11 @@ static bool _G_initialized = false; obj* initialize_init_control_option(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); return w; } diff --git a/src/stage0/init/control/reader.cpp b/src/stage0/init/control/reader.cpp index f9be999351..00b50e00c2 100644 --- a/src/stage0/init/control/reader.cpp +++ b/src/stage0/init/control/reader.cpp @@ -1135,9 +1135,13 @@ static bool _G_initialized = false; obj* initialize_init_control_reader(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_id(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); return w; } diff --git a/src/stage0/init/control/state.cpp b/src/stage0/init/control/state.cpp index 775a67979f..eff1913a74 100644 --- a/src/stage0/init/control/state.cpp +++ b/src/stage0/init/control/state.cpp @@ -1604,9 +1604,13 @@ static bool _G_initialized = false; obj* initialize_init_control_state(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_lift(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_id(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); l_state__t_run_x_27___rarg___closed__1 = _init_l_state__t_run_x_27___rarg___closed__1(); lean::mark_persistent(l_state__t_run_x_27___rarg___closed__1); diff --git a/src/stage0/init/data/array/basic.cpp b/src/stage0/init/data/array/basic.cpp index ba3763aac3..40657af5f3 100644 --- a/src/stage0/init/data/array/basic.cpp +++ b/src/stage0/init/data/array/basic.cpp @@ -1433,11 +1433,17 @@ static bool _G_initialized = false; obj* initialize_init_data_array_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_fin_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); +if (io_result_is_error(w)) return w; w = initialize_init_function(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); l_array_nil___closed__1 = _init_l_array_nil___closed__1(); lean::mark_persistent(l_array_nil___closed__1); diff --git a/src/stage0/init/data/array/default.cpp b/src/stage0/init/data/array/default.cpp index d2d39789fa..05879efe16 100644 --- a/src/stage0/init/data/array/default.cpp +++ b/src/stage0/init/data/array/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_array_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_array_basic(w); return w; } diff --git a/src/stage0/init/data/basic.cpp b/src/stage0/init/data/basic.cpp index a5152f6172..0ba31c1054 100644 --- a/src/stage0/init/data/basic.cpp +++ b/src/stage0/init/data/basic.cpp @@ -28,15 +28,25 @@ static bool _G_initialized = false; obj* initialize_init_data_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_fin_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_char_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_ordering_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); return w; } diff --git a/src/stage0/init/data/char/basic.cpp b/src/stage0/init/data/char/basic.cpp index 1eca65ed67..c77de6faed 100644 --- a/src/stage0/init/data/char/basic.cpp +++ b/src/stage0/init/data/char/basic.cpp @@ -632,6 +632,7 @@ static bool _G_initialized = false; obj* initialize_init_data_char_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); l_char_has__lt = _init_l_char_has__lt(); lean::mark_persistent(l_char_has__lt); diff --git a/src/stage0/init/data/char/default.cpp b/src/stage0/init/data/char/default.cpp index 314c672947..6cc9561705 100644 --- a/src/stage0/init/data/char/default.cpp +++ b/src/stage0/init/data/char/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_char_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_char_basic(w); return w; } diff --git a/src/stage0/init/data/default.cpp b/src/stage0/init/data/default.cpp index 63bb0ba71d..e67e2fd040 100644 --- a/src/stage0/init/data/default.cpp +++ b/src/stage0/init/data/default.cpp @@ -32,19 +32,33 @@ static bool _G_initialized = false; obj* initialize_init_data_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_char_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_int_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_array_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_fin_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_ordering_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbtree_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_instances(w); return w; } diff --git a/src/stage0/init/data/dlist.cpp b/src/stage0/init/data/dlist.cpp index 7f24df8c05..5691a302bb 100644 --- a/src/stage0/init/data/dlist.cpp +++ b/src/stage0/init/data/dlist.cpp @@ -359,7 +359,9 @@ static bool _G_initialized = false; obj* initialize_init_data_dlist(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_function(w); return w; } diff --git a/src/stage0/init/data/fin/basic.cpp b/src/stage0/init/data/fin/basic.cpp index 84c4a0e026..88bf9d2050 100644 --- a/src/stage0/init/data/fin/basic.cpp +++ b/src/stage0/init/data/fin/basic.cpp @@ -730,7 +730,9 @@ static bool _G_initialized = false; obj* initialize_init_data_fin_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_div(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_bitwise(w); return w; } diff --git a/src/stage0/init/data/fin/default.cpp b/src/stage0/init/data/fin/default.cpp index bffffbefbe..cb7b20f672 100644 --- a/src/stage0/init/data/fin/default.cpp +++ b/src/stage0/init/data/fin/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_fin_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_fin_basic(w); return w; } diff --git a/src/stage0/init/data/hashable.cpp b/src/stage0/init/data/hashable.cpp index 9453c9addb..76c71e9163 100644 --- a/src/stage0/init/data/hashable.cpp +++ b/src/stage0/init/data/hashable.cpp @@ -102,7 +102,9 @@ static bool _G_initialized = false; obj* initialize_init_data_hashable(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_default(w); l_string_hashable = _init_l_string_hashable(); lean::mark_persistent(l_string_hashable); diff --git a/src/stage0/init/data/hashmap/basic.cpp b/src/stage0/init/data/hashmap/basic.cpp index fd3f0d0b92..dc2b5092f0 100644 --- a/src/stage0/init/data/hashmap/basic.cpp +++ b/src/stage0/init/data/hashmap/basic.cpp @@ -1584,9 +1584,13 @@ static bool _G_initialized = false; obj* initialize_init_data_hashmap_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_array_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_hashable(w); l_mk__hashmap__imp___rarg___closed__1 = _init_l_mk__hashmap__imp___rarg___closed__1(); lean::mark_persistent(l_mk__hashmap__imp___rarg___closed__1); diff --git a/src/stage0/init/data/int/basic.cpp b/src/stage0/init/data/int/basic.cpp index 4663252816..4e413420c6 100644 --- a/src/stage0/init/data/int/basic.cpp +++ b/src/stage0/init/data/int/basic.cpp @@ -658,10 +658,15 @@ static bool _G_initialized = false; obj* initialize_init_data_int_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); l_int_zero = _init_l_int_zero(); lean::mark_persistent(l_int_zero); diff --git a/src/stage0/init/data/int/default.cpp b/src/stage0/init/data/int/default.cpp index f699d1f6d1..f4af49c3a2 100644 --- a/src/stage0/init/data/int/default.cpp +++ b/src/stage0/init/data/int/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_int_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_int_basic(w); return w; } diff --git a/src/stage0/init/data/list/basic.cpp b/src/stage0/init/data/list/basic.cpp index 2435604630..6e865b09bc 100644 --- a/src/stage0/init/data/list/basic.cpp +++ b/src/stage0/init/data/list/basic.cpp @@ -5638,7 +5638,9 @@ static bool _G_initialized = false; obj* initialize_init_data_list_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); l_list_unzip___main___rarg___closed__1 = _init_l_list_unzip___main___rarg___closed__1(); lean::mark_persistent(l_list_unzip___main___rarg___closed__1); diff --git a/src/stage0/init/data/list/default.cpp b/src/stage0/init/data/list/default.cpp index 046ac12882..8670deb5e3 100644 --- a/src/stage0/init/data/list/default.cpp +++ b/src/stage0/init/data/list/default.cpp @@ -20,7 +20,9 @@ static bool _G_initialized = false; obj* initialize_init_data_list_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_instances(w); return w; } diff --git a/src/stage0/init/data/list/instances.cpp b/src/stage0/init/data/list/instances.cpp index c542774881..5fdd512db9 100644 --- a/src/stage0/init/data/list/instances.cpp +++ b/src/stage0/init/data/list/instances.cpp @@ -846,8 +846,11 @@ static bool _G_initialized = false; obj* initialize_init_data_list_instances(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad(w); l_list_monad = _init_l_list_monad(); lean::mark_persistent(l_list_monad); diff --git a/src/stage0/init/data/nat/basic.cpp b/src/stage0/init/data/nat/basic.cpp index 0a0d347471..a6b1441bc1 100644 --- a/src/stage0/init/data/nat/basic.cpp +++ b/src/stage0/init/data/nat/basic.cpp @@ -392,6 +392,7 @@ static bool _G_initialized = false; obj* initialize_init_data_nat_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); l_nat_decidable__eq = _init_l_nat_decidable__eq(); lean::mark_persistent(l_nat_decidable__eq); diff --git a/src/stage0/init/data/nat/bitwise.cpp b/src/stage0/init/data/nat/bitwise.cpp index 71f99d6ddc..55cba71318 100644 --- a/src/stage0/init/data/nat/bitwise.cpp +++ b/src/stage0/init/data/nat/bitwise.cpp @@ -354,8 +354,11 @@ static bool _G_initialized = false; obj* initialize_init_data_nat_bitwise(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_div(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); l_nat_land___closed__1 = _init_l_nat_land___closed__1(); lean::mark_persistent(l_nat_land___closed__1); diff --git a/src/stage0/init/data/nat/default.cpp b/src/stage0/init/data/nat/default.cpp index 80cb9a1f40..212691e6fa 100644 --- a/src/stage0/init/data/nat/default.cpp +++ b/src/stage0/init/data/nat/default.cpp @@ -21,8 +21,11 @@ static bool _G_initialized = false; obj* initialize_init_data_nat_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_div(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_bitwise(w); return w; } diff --git a/src/stage0/init/data/nat/div.cpp b/src/stage0/init/data/nat/div.cpp index 05dfab2faf..fca5136fa8 100644 --- a/src/stage0/init/data/nat/div.cpp +++ b/src/stage0/init/data/nat/div.cpp @@ -169,7 +169,9 @@ static bool _G_initialized = false; obj* initialize_init_data_nat_div(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_wf(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); l_nat_has__div = _init_l_nat_has__div(); lean::mark_persistent(l_nat_has__div); diff --git a/src/stage0/init/data/option/basic.cpp b/src/stage0/init/data/option/basic.cpp index 5283013531..c788b16ac8 100644 --- a/src/stage0/init/data/option/basic.cpp +++ b/src/stage0/init/data/option/basic.cpp @@ -1280,9 +1280,13 @@ static bool _G_initialized = false; obj* initialize_init_data_option_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_alternative(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); l_option_monad = _init_l_option_monad(); lean::mark_persistent(l_option_monad); diff --git a/src/stage0/init/data/option/instances.cpp b/src/stage0/init/data/option/instances.cpp index 9e205efb1f..60b6c19b5e 100644 --- a/src/stage0/init/data/option/instances.cpp +++ b/src/stage0/init/data/option/instances.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_option_instances(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); return w; } diff --git a/src/stage0/init/data/ordering/basic.cpp b/src/stage0/init/data/ordering/basic.cpp index 36e07bed63..43237330db 100644 --- a/src/stage0/init/data/ordering/basic.cpp +++ b/src/stage0/init/data/ordering/basic.cpp @@ -402,6 +402,7 @@ static bool _G_initialized = false; obj* initialize_init_data_ordering_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); l_ordering_has__repr___closed__1 = _init_l_ordering_has__repr___closed__1(); lean::mark_persistent(l_ordering_has__repr___closed__1); diff --git a/src/stage0/init/data/ordering/default.cpp b/src/stage0/init/data/ordering/default.cpp index 879440682e..3773b978a3 100644 --- a/src/stage0/init/data/ordering/default.cpp +++ b/src/stage0/init/data/ordering/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_ordering_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_ordering_basic(w); return w; } diff --git a/src/stage0/init/data/rbmap/basic.cpp b/src/stage0/init/data/rbmap/basic.cpp index 7af4675bdf..ed62ac31dc 100644 --- a/src/stage0/init/data/rbmap/basic.cpp +++ b/src/stage0/init/data/rbmap/basic.cpp @@ -8106,8 +8106,11 @@ static bool _G_initialized = false; obj* initialize_init_data_rbmap_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_ordering_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); l_rbmap_has__repr___rarg___closed__1 = _init_l_rbmap_has__repr___rarg___closed__1(); lean::mark_persistent(l_rbmap_has__repr___rarg___closed__1); diff --git a/src/stage0/init/data/rbmap/default.cpp b/src/stage0/init/data/rbmap/default.cpp index 88f1779bf2..70b70ab37a 100644 --- a/src/stage0/init/data/rbmap/default.cpp +++ b/src/stage0/init/data/rbmap/default.cpp @@ -20,7 +20,9 @@ static bool _G_initialized = false; obj* initialize_init_data_rbmap_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_rbtree_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_basic(w); return w; } diff --git a/src/stage0/init/data/rbtree/basic.cpp b/src/stage0/init/data/rbtree/basic.cpp index 8aed85ca80..d9dc938c70 100644 --- a/src/stage0/init/data/rbtree/basic.cpp +++ b/src/stage0/init/data/rbtree/basic.cpp @@ -5213,6 +5213,7 @@ static bool _G_initialized = false; obj* initialize_init_data_rbtree_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_basic(w); l_rbtree_has__repr___rarg___closed__1 = _init_l_rbtree_has__repr___rarg___closed__1(); lean::mark_persistent(l_rbtree_has__repr___rarg___closed__1); diff --git a/src/stage0/init/data/rbtree/default.cpp b/src/stage0/init/data/rbtree/default.cpp index 85e236c869..f1fbc74aa3 100644 --- a/src/stage0/init/data/rbtree/default.cpp +++ b/src/stage0/init/data/rbtree/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_rbtree_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_rbtree_basic(w); return w; } diff --git a/src/stage0/init/data/repr.cpp b/src/stage0/init/data/repr.cpp index f738157ab1..7135477082 100644 --- a/src/stage0/init/data/repr.cpp +++ b/src/stage0/init/data/repr.cpp @@ -1613,8 +1613,11 @@ static bool _G_initialized = false; obj* initialize_init_data_repr(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_div(w); l_bool_has__repr___closed__1 = _init_l_bool_has__repr___closed__1(); lean::mark_persistent(l_bool_has__repr___closed__1); diff --git a/src/stage0/init/data/string/basic.cpp b/src/stage0/init/data/string/basic.cpp index 2294994c88..91610f04a4 100644 --- a/src/stage0/init/data/string/basic.cpp +++ b/src/stage0/init/data/string/basic.cpp @@ -2287,8 +2287,11 @@ static bool _G_initialized = false; obj* initialize_init_data_string_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_char_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); l_string_decidable__eq = _init_l_string_decidable__eq(); lean::mark_persistent(l_string_decidable__eq); diff --git a/src/stage0/init/data/string/default.cpp b/src/stage0/init/data/string/default.cpp index 4b4d8a00cd..df83111511 100644 --- a/src/stage0/init/data/string/default.cpp +++ b/src/stage0/init/data/string/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_data_string_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); return w; } diff --git a/src/stage0/init/data/to_string.cpp b/src/stage0/init/data/to_string.cpp index 21fe60486e..800313a58e 100644 --- a/src/stage0/init/data/to_string.cpp +++ b/src/stage0/init/data/to_string.cpp @@ -834,9 +834,13 @@ static bool _G_initialized = false; obj* initialize_init_data_to__string(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_div(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); return w; } diff --git a/src/stage0/init/data/uint.cpp b/src/stage0/init/data/uint.cpp index e85c53860f..33f89d3708 100644 --- a/src/stage0/init/data/uint.cpp +++ b/src/stage0/init/data/uint.cpp @@ -1801,7 +1801,9 @@ static bool _G_initialized = false; obj* initialize_init_data_uint(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_fin_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_platform(w); l_uint8__sz = _init_l_uint8__sz(); lean::mark_persistent(l_uint8__sz); diff --git a/src/stage0/init/default.cpp b/src/stage0/init/default.cpp index ffe17e064b..b98d81bb65 100644 --- a/src/stage0/init/default.cpp +++ b/src/stage0/init/default.cpp @@ -28,15 +28,25 @@ static bool _G_initialized = false; obj* initialize_init_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_function(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); +if (io_result_is_error(w)) return w; w = initialize_init_wf(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_io(w); +if (io_result_is_error(w)) return w; w = initialize_init_util(w); +if (io_result_is_error(w)) return w; w = initialize_init_fix(w); return w; } diff --git a/src/stage0/init/fix.cpp b/src/stage0/init/fix.cpp index 8aa03d390f..d9a0f7bed3 100644 --- a/src/stage0/init/fix.cpp +++ b/src/stage0/init/fix.cpp @@ -1100,6 +1100,7 @@ static bool _G_initialized = false; obj* initialize_init_fix(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); return w; } diff --git a/src/stage0/init/function.cpp b/src/stage0/init/function.cpp index 0e5ca51662..ab3852e267 100644 --- a/src/stage0/init/function.cpp +++ b/src/stage0/init/function.cpp @@ -377,6 +377,7 @@ static bool _G_initialized = false; obj* initialize_init_function(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); return w; } diff --git a/src/stage0/init/io.cpp b/src/stage0/init/io.cpp index bfed79e23c..1da1274c8a 100644 --- a/src/stage0/init/io.cpp +++ b/src/stage0/init/io.cpp @@ -1852,8 +1852,11 @@ static bool _G_initialized = false; obj* initialize_init_io(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_estate(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_fix(w); l_io_error_has__to__string = _init_l_io_error_has__to__string(); lean::mark_persistent(l_io_error_has__to__string); diff --git a/src/stage0/init/lean/compiler/const_folding.cpp b/src/stage0/init/lean/compiler/const_folding.cpp index b781dc68b7..82b665cf87 100644 --- a/src/stage0/init/lean/compiler/const_folding.cpp +++ b/src/stage0/init/lean/compiler/const_folding.cpp @@ -2285,8 +2285,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_compiler_const__folding(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); +if (io_result_is_error(w)) return w; w = initialize_init_platform(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_util(w); l_lean_compiler_mk__uint__type__name___closed__1 = _init_l_lean_compiler_mk__uint__type__name___closed__1(); lean::mark_persistent(l_lean_compiler_mk__uint__type__name___closed__1); diff --git a/src/stage0/init/lean/compiler/default.cpp b/src/stage0/init/lean/compiler/default.cpp index 2622238dac..a2b0aa6e0d 100644 --- a/src/stage0/init/lean/compiler/default.cpp +++ b/src/stage0/init/lean/compiler/default.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_compiler_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_const__folding(w); return w; } diff --git a/src/stage0/init/lean/compiler/ir.cpp b/src/stage0/init/lean/compiler/ir.cpp index 5222189db8..5e3a841f71 100644 --- a/src/stage0/init/lean/compiler/ir.cpp +++ b/src/stage0/init/lean/compiler/ir.cpp @@ -4257,8 +4257,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_compiler_ir(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); l_lean_ir_type_has__beq = _init_l_lean_ir_type_has__beq(); lean::mark_persistent(l_lean_ir_type_has__beq); diff --git a/src/stage0/init/lean/compiler/util.cpp b/src/stage0/init/lean/compiler/util.cpp index eef6a3851b..2588b4babb 100644 --- a/src/stage0/init/lean/compiler/util.cpp +++ b/src/stage0/init/lean/compiler/util.cpp @@ -97,6 +97,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_compiler_util(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); l_lean_compiler_neutral__expr = _init_l_lean_compiler_neutral__expr(); lean::mark_persistent(l_lean_compiler_neutral__expr); diff --git a/src/stage0/init/lean/config.cpp b/src/stage0/init/lean/config.cpp index d7f0136e29..416349829a 100644 --- a/src/stage0/init/lean/config.cpp +++ b/src/stage0/init/lean/config.cpp @@ -28,6 +28,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_config(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); l_lean_closure__max__args = _init_l_lean_closure__max__args(); lean::mark_persistent(l_lean_closure__max__args); diff --git a/src/stage0/init/lean/declaration.cpp b/src/stage0/init/lean/declaration.cpp index bc237cc48c..d3240b9a2f 100644 --- a/src/stage0/init/lean/declaration.cpp +++ b/src/stage0/init/lean/declaration.cpp @@ -228,6 +228,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_declaration(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); return w; } diff --git a/src/stage0/init/lean/default.cpp b/src/stage0/init/lean/default.cpp index 2bc3315667..5e2c5846ec 100644 --- a/src/stage0/init/lean/default.cpp +++ b/src/stage0/init/lean/default.cpp @@ -21,8 +21,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_default(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_frontend(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_extern(w); return w; } diff --git a/src/stage0/init/lean/disjoint_set.cpp b/src/stage0/init/lean/disjoint_set.cpp index 7f76c34a59..4baf14df60 100644 --- a/src/stage0/init/lean/disjoint_set.cpp +++ b/src/stage0/init/lean/disjoint_set.cpp @@ -443,6 +443,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_disjoint__set(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_hashmap_basic(w); return w; } diff --git a/src/stage0/init/lean/elaborator.cpp b/src/stage0/init/lean/elaborator.cpp index 049ffff686..299040c6df 100644 --- a/src/stage0/init/lean/elaborator.cpp +++ b/src/stage0/init/lean/elaborator.cpp @@ -33598,9 +33598,13 @@ static bool _G_initialized = false; obj* initialize_init_lean_elaborator(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_module(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_expander(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_options(w); l_lean_elaborator_ordered__rbmap_empty___closed__1 = _init_l_lean_elaborator_ordered__rbmap_empty___closed__1(); lean::mark_persistent(l_lean_elaborator_ordered__rbmap_empty___closed__1); diff --git a/src/stage0/init/lean/expander.cpp b/src/stage0/init/lean/expander.cpp index a3bd6b9959..5640f3f0a5 100644 --- a/src/stage0/init/lean/expander.cpp +++ b/src/stage0/init/lean/expander.cpp @@ -12018,7 +12018,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_expander(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_module(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); l_lean_expander_transform__m_monad = _init_l_lean_expander_transform__m_monad(); lean::mark_persistent(l_lean_expander_transform__m_monad); diff --git a/src/stage0/init/lean/expr.cpp b/src/stage0/init/lean/expr.cpp index ffc29821f3..2aead83a4f 100644 --- a/src/stage0/init/lean/expr.cpp +++ b/src/stage0/init/lean/expr.cpp @@ -209,7 +209,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_expr(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_level(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); l_lean_expr__is__inhabited = _init_l_lean_expr__is__inhabited(); lean::mark_persistent(l_lean_expr__is__inhabited); diff --git a/src/stage0/init/lean/extern.cpp b/src/stage0/init/lean/extern.cpp index d595392800..951db93618 100644 --- a/src/stage0/init/lean/extern.cpp +++ b/src/stage0/init/lean/extern.cpp @@ -601,7 +601,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_extern(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); l_lean_get__extern__entry__for__aux___main___closed__1 = _init_l_lean_get__extern__entry__for__aux___main___closed__1(); lean::mark_persistent(l_lean_get__extern__entry__for__aux___main___closed__1); diff --git a/src/stage0/init/lean/format.cpp b/src/stage0/init/lean/format.cpp index 10109c86aa..538eb4076a 100644 --- a/src/stage0/init/lean/format.cpp +++ b/src/stage0/init/lean/format.cpp @@ -2224,8 +2224,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_format(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_reader(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_state(w); l_lean_format_join___closed__1 = _init_l_lean_format_join___closed__1(); lean::mark_persistent(l_lean_format_join___closed__1); diff --git a/src/stage0/init/lean/frontend.cpp b/src/stage0/init/lean/frontend.cpp index 8f8ed2b8a9..593e1f6d0d 100644 --- a/src/stage0/init/lean/frontend.cpp +++ b/src/stage0/init/lean/frontend.cpp @@ -2320,11 +2320,17 @@ static bool _G_initialized = false; obj* initialize_init_lean_frontend(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_module(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_expander(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_elaborator(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_util(w); +if (io_result_is_error(w)) return w; w = initialize_init_io(w); l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__1 = _init_l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__1(); lean::mark_persistent(l_io_prim_iterate___at_lean_run__frontend___spec__6___lambda__4___closed__1); diff --git a/src/stage0/init/lean/kvmap.cpp b/src/stage0/init/lean/kvmap.cpp index 0d4a0ccd03..0a3acfd430 100644 --- a/src/stage0/init/lean/kvmap.cpp +++ b/src/stage0/init/lean/kvmap.cpp @@ -847,7 +847,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_kvmap(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); l_lean_data__value_has__beq = _init_l_lean_data__value_has__beq(); lean::mark_persistent(l_lean_data__value_has__beq); diff --git a/src/stage0/init/lean/level.cpp b/src/stage0/init/lean/level.cpp index b8e0b90519..62ba6d77e4 100644 --- a/src/stage0/init/lean/level.cpp +++ b/src/stage0/init/lean/level.cpp @@ -1276,7 +1276,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_level(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); l_lean_level__is__inhabited = _init_l_lean_level__is__inhabited(); lean::mark_persistent(l_lean_level__is__inhabited); diff --git a/src/stage0/init/lean/message.cpp b/src/stage0/init/lean/message.cpp index 903e225b92..1ec2b7f4c6 100644 --- a/src/stage0/init/lean/message.cpp +++ b/src/stage0/init/lean/message.cpp @@ -314,7 +314,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_message(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_position(w); l_lean_message_to__string___closed__1 = _init_l_lean_message_to__string___closed__1(); lean::mark_persistent(l_lean_message_to__string___closed__1); diff --git a/src/stage0/init/lean/name.cpp b/src/stage0/init/lean/name.cpp index 4692e7c4f7..45cdf2f72d 100644 --- a/src/stage0/init/lean/name.cpp +++ b/src/stage0/init/lean/name.cpp @@ -2309,13 +2309,21 @@ static bool _G_initialized = false; obj* initialize_init_lean_name(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_coe(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_uint(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_format(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_hashable(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbtree_default(w); l_lean_inhabited = _init_l_lean_inhabited(); lean::mark_persistent(l_lean_inhabited); diff --git a/src/stage0/init/lean/name_mangling.cpp b/src/stage0/init/lean/name_mangling.cpp index fa1b9eed3c..876c941b03 100644 --- a/src/stage0/init/lean/name_mangling.cpp +++ b/src/stage0/init/lean/name_mangling.cpp @@ -3269,7 +3269,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_name__mangling(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_string__literal(w); l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__1 = _init_l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__1(); lean::mark_persistent(l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__1); diff --git a/src/stage0/init/lean/options.cpp b/src/stage0/init/lean/options.cpp index 433e5209f9..9fb62076e1 100644 --- a/src/stage0/init/lean/options.cpp +++ b/src/stage0/init/lean/options.cpp @@ -28,6 +28,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_options(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); l_lean_options_mk = _init_l_lean_options_mk(); lean::mark_persistent(l_lean_options_mk); diff --git a/src/stage0/init/lean/parser/basic.cpp b/src/stage0/init/lean/parser/basic.cpp index 0f8e427b58..c71f5d0a3a 100644 --- a/src/stage0/init/lean/parser/basic.cpp +++ b/src/stage0/init/lean/parser/basic.cpp @@ -3512,12 +3512,19 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_basic(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_parsec(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_syntax(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_rec(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_trie(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_identifier(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_message(w); l_lean_parser_max__prec = _init_l_lean_parser_max__prec(); lean::mark_persistent(l_lean_parser_max__prec); diff --git a/src/stage0/init/lean/parser/combinators.cpp b/src/stage0/init/lean/parser/combinators.cpp index 6976249e57..c0559f8bd5 100644 --- a/src/stage0/init/lean/parser/combinators.cpp +++ b/src/stage0/init/lean/parser/combinators.cpp @@ -3993,7 +3993,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_combinators(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_instances(w); l___private_init_lean_parser_combinators_1__many1__aux___main___rarg___closed__1 = _init_l___private_init_lean_parser_combinators_1__many1__aux___main___rarg___closed__1(); lean::mark_persistent(l___private_init_lean_parser_combinators_1__many1__aux___main___rarg___closed__1); diff --git a/src/stage0/init/lean/parser/command.cpp b/src/stage0/init/lean/parser/command.cpp index 0959565c11..dd50bff16b 100644 --- a/src/stage0/init/lean/parser/command.cpp +++ b/src/stage0/init/lean/parser/command.cpp @@ -14801,6 +14801,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_command(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_declaration(w); l_lean_parser_command_parser_lean_parser_has__view = _init_l_lean_parser_command_parser_lean_parser_has__view(); lean::mark_persistent(l_lean_parser_command_parser_lean_parser_has__view); diff --git a/src/stage0/init/lean/parser/declaration.cpp b/src/stage0/init/lean/parser/declaration.cpp index 4e5f8b5fe7..9bd52b6c6c 100644 --- a/src/stage0/init/lean/parser/declaration.cpp +++ b/src/stage0/init/lean/parser/declaration.cpp @@ -29992,6 +29992,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_declaration(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_term(w); l_lean_parser_command_doc__comment = _init_l_lean_parser_command_doc__comment(); lean::mark_persistent(l_lean_parser_command_doc__comment); diff --git a/src/stage0/init/lean/parser/identifier.cpp b/src/stage0/init/lean/parser/identifier.cpp index 46ba8c553c..96f7814c4a 100644 --- a/src/stage0/init/lean/parser/identifier.cpp +++ b/src/stage0/init/lean/parser/identifier.cpp @@ -2462,7 +2462,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_identifier(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_char_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_parsec(w); l_lean_id__begin__escape = _init_l_lean_id__begin__escape(); l_lean_id__begin__escape___boxed = _init_l_lean_id__begin__escape___boxed(); diff --git a/src/stage0/init/lean/parser/level.cpp b/src/stage0/init/lean/parser/level.cpp index 1b15f452b7..dd0605a4bc 100644 --- a/src/stage0/init/lean/parser/level.cpp +++ b/src/stage0/init/lean/parser/level.cpp @@ -6641,6 +6641,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_level(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_pratt(w); l_lean_parser_level__parser__m_monad = _init_l_lean_parser_level__parser__m_monad(); lean::mark_persistent(l_lean_parser_level__parser__m_monad); diff --git a/src/stage0/init/lean/parser/module.cpp b/src/stage0/init/lean/parser/module.cpp index bbb993d2b5..b6035bb831 100644 --- a/src/stage0/init/lean/parser/module.cpp +++ b/src/stage0/init/lean/parser/module.cpp @@ -6036,6 +6036,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_module(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_command(w); l_lean_parser_module__parser__m_monad = _init_l_lean_parser_module__parser__m_monad(); lean::mark_persistent(l_lean_parser_module__parser__m_monad); diff --git a/src/stage0/init/lean/parser/notation.cpp b/src/stage0/init/lean/parser/notation.cpp index f9a82a771a..a9eb43fea0 100644 --- a/src/stage0/init/lean/parser/notation.cpp +++ b/src/stage0/init/lean/parser/notation.cpp @@ -19878,6 +19878,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_notation(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_token(w); l_lean_parser_term_parser_lean_parser_has__tokens___closed__1 = _init_l_lean_parser_term_parser_lean_parser_has__tokens___closed__1(); lean::mark_persistent(l_lean_parser_term_parser_lean_parser_has__tokens___closed__1); diff --git a/src/stage0/init/lean/parser/parsec.cpp b/src/stage0/init/lean/parser/parsec.cpp index c1ccf59f9b..8a3b102101 100644 --- a/src/stage0/init/lean/parser/parsec.cpp +++ b/src/stage0/init/lean/parser/parsec.cpp @@ -10466,14 +10466,23 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_parsec(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_to__string(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_list_basic(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_except(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_repr(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_dlist(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_monad__fail(w); +if (io_result_is_error(w)) return w; w = initialize_init_control_combinators(w); l_lean_parser_parsec_expected_to__string___main___closed__1 = _init_l_lean_parser_parsec_expected_to__string___main___closed__1(); lean::mark_persistent(l_lean_parser_parsec_expected_to__string___main___closed__1); diff --git a/src/stage0/init/lean/parser/pratt.cpp b/src/stage0/init/lean/parser/pratt.cpp index 1a4d5623dc..246e1ed390 100644 --- a/src/stage0/init/lean/parser/pratt.cpp +++ b/src/stage0/init/lean/parser/pratt.cpp @@ -956,6 +956,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_pratt(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_token(w); l_lean_parser_curr__lbp___rarg___lambda__1___closed__1 = _init_l_lean_parser_curr__lbp___rarg___lambda__1___closed__1(); lean::mark_persistent(l_lean_parser_curr__lbp___rarg___lambda__1___closed__1); diff --git a/src/stage0/init/lean/parser/rec.cpp b/src/stage0/init/lean/parser/rec.cpp index 8cf44e06e1..0ed58fe13e 100644 --- a/src/stage0/init/lean/parser/rec.cpp +++ b/src/stage0/init/lean/parser/rec.cpp @@ -447,7 +447,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_rec(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_parsec(w); +if (io_result_is_error(w)) return w; w = initialize_init_fix(w); l_lean_parser_rec__t_run__parsec___rarg___lambda__1___closed__1 = _init_l_lean_parser_rec__t_run__parsec___rarg___lambda__1___closed__1(); lean::mark_persistent(l_lean_parser_rec__t_run__parsec___rarg___lambda__1___closed__1); diff --git a/src/stage0/init/lean/parser/string_literal.cpp b/src/stage0/init/lean/parser/string_literal.cpp index 36e3bd2d7f..d45962691d 100644 --- a/src/stage0/init/lean/parser/string_literal.cpp +++ b/src/stage0/init/lean/parser/string_literal.cpp @@ -1093,6 +1093,7 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_string__literal(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_parsec(w); l_lean_parser_parse__hex__digit___rarg___lambda__3___closed__1 = _init_l_lean_parser_parse__hex__digit___rarg___lambda__3___closed__1(); lean::mark_persistent(l_lean_parser_parse__hex__digit___rarg___lambda__3___closed__1); diff --git a/src/stage0/init/lean/parser/syntax.cpp b/src/stage0/init/lean/parser/syntax.cpp index c023264c1d..58795a00ec 100644 --- a/src/stage0/init/lean/parser/syntax.cpp +++ b/src/stage0/init/lean/parser/syntax.cpp @@ -2768,7 +2768,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_syntax(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_parsec(w); l_lean_parser_choice = _init_l_lean_parser_choice(); lean::mark_persistent(l_lean_parser_choice); diff --git a/src/stage0/init/lean/parser/term.cpp b/src/stage0/init/lean/parser/term.cpp index 624422752c..5c3ae71b18 100644 --- a/src/stage0/init/lean/parser/term.cpp +++ b/src/stage0/init/lean/parser/term.cpp @@ -48964,8 +48964,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_term(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_level(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_notation(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_expr(w); l_lean_parser_ident__univ__spec = _init_l_lean_parser_ident__univ__spec(); lean::mark_persistent(l_lean_parser_ident__univ__spec); diff --git a/src/stage0/init/lean/parser/token.cpp b/src/stage0/init/lean/parser/token.cpp index daa82f14d4..a3b46c3fa2 100644 --- a/src/stage0/init/lean/parser/token.cpp +++ b/src/stage0/init/lean/parser/token.cpp @@ -26887,7 +26887,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_token(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_combinators(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_parser_string__literal(w); l_lean_parser_match__token___closed__1 = _init_l_lean_parser_match__token___closed__1(); lean::mark_persistent(l_lean_parser_match__token___closed__1); diff --git a/src/stage0/init/lean/parser/trie.cpp b/src/stage0/init/lean/parser/trie.cpp index a63e51ab89..4b2325595c 100644 --- a/src/stage0/init/lean/parser/trie.cpp +++ b/src/stage0/init/lean/parser/trie.cpp @@ -1504,7 +1504,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_parser_trie(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_format(w); l_lean_parser_trie_mk___closed__1 = _init_l_lean_parser_trie_mk___closed__1(); lean::mark_persistent(l_lean_parser_trie_mk___closed__1); diff --git a/src/stage0/init/lean/position.cpp b/src/stage0/init/lean/position.cpp index 59a392ba60..2026cff724 100644 --- a/src/stage0/init/lean/position.cpp +++ b/src/stage0/init/lean/position.cpp @@ -804,8 +804,11 @@ static bool _G_initialized = false; obj* initialize_init_lean_position(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_format(w); l_lean_position_has__lt = _init_l_lean_position_has__lt(); lean::mark_persistent(l_lean_position_has__lt); diff --git a/src/stage0/init/lean/trace.cpp b/src/stage0/init/lean/trace.cpp index 01cd4dbb91..7b1d912e28 100644 --- a/src/stage0/init/lean/trace.cpp +++ b/src/stage0/init/lean/trace.cpp @@ -1289,10 +1289,15 @@ static bool _G_initialized = false; obj* initialize_init_lean_trace(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_format(w); +if (io_result_is_error(w)) return w; w = initialize_init_data_rbmap_default(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_position(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_options(w); return w; } diff --git a/src/stage0/init/lean/util.cpp b/src/stage0/init/lean/util.cpp index 9c6c614708..65589558d2 100644 --- a/src/stage0/init/lean/util.cpp +++ b/src/stage0/init/lean/util.cpp @@ -74,7 +74,9 @@ static bool _G_initialized = false; obj* initialize_init_lean_util(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_lean_position(w); +if (io_result_is_error(w)) return w; w = initialize_init_io(w); return w; } diff --git a/src/stage0/init/platform.cpp b/src/stage0/init/platform.cpp index 1bbece91d1..8fba5e6007 100644 --- a/src/stage0/init/platform.cpp +++ b/src/stage0/init/platform.cpp @@ -28,6 +28,7 @@ static bool _G_initialized = false; obj* initialize_init_platform(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_core(w); l_system_platform_nbits = _init_l_system_platform_nbits(); lean::mark_persistent(l_system_platform_nbits); diff --git a/src/stage0/init/util.cpp b/src/stage0/init/util.cpp index 60a7ba98c0..65d1ee7685 100644 --- a/src/stage0/init/util.cpp +++ b/src/stage0/init/util.cpp @@ -38,6 +38,7 @@ static bool _G_initialized = false; obj* initialize_init_util(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_string_basic(w); return w; } diff --git a/src/stage0/init/wf.cpp b/src/stage0/init/wf.cpp index 86a2fd87b0..e61d4d3a94 100644 --- a/src/stage0/init/wf.cpp +++ b/src/stage0/init/wf.cpp @@ -19,6 +19,7 @@ static bool _G_initialized = false; obj* initialize_init_wf(obj* w) { if (_G_initialized) return w; _G_initialized = true; +if (io_result_is_error(w)) return w; w = initialize_init_data_nat_basic(w); return w; }