From 70a15898178cfe06219d2e7fcf4dadec41aedf5f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Jun 2019 08:59:55 -0700 Subject: [PATCH] refactor(library/init/lean): move `extern.lean` to `compiler` subdirectory --- library/init/lean/compiler/default.lean | 1 + .../{extern.lean => compiler/externattr.lean} | 0 library/init/lean/compiler/ir/basic.lean | 6 ++++-- library/init/lean/compiler/ir/boxing.lean | 2 +- library/init/lean/default.lean | 1 - src/shell/lean.cpp | 5 +++-- src/stage0/CMakeLists.txt | 2 +- src/stage0/init/lean/compiler/default.cpp | 5 ++++- .../lean/{extern.cpp => compiler/externattr.cpp} | 16 ++++++++-------- src/stage0/init/lean/compiler/ir/basic.cpp | 8 ++++---- src/stage0/init/lean/compiler/ir/boxing.cpp | 6 +++--- src/stage0/init/lean/default.cpp | 5 +---- 12 files changed, 30 insertions(+), 27 deletions(-) rename library/init/lean/{extern.lean => compiler/externattr.lean} (100%) rename src/stage0/init/lean/{extern.cpp => compiler/externattr.cpp} (96%) diff --git a/library/init/lean/compiler/default.lean b/library/init/lean/compiler/default.lean index e406d2cb57..39de8a9e8c 100644 --- a/library/init/lean/compiler/default.lean +++ b/library/init/lean/compiler/default.lean @@ -7,4 +7,5 @@ prelude import init.lean.compiler.inline import init.lean.compiler.constfolding import init.lean.compiler.closedtermcache +import init.lean.compiler.externattr import init.lean.compiler.ir diff --git a/library/init/lean/extern.lean b/library/init/lean/compiler/externattr.lean similarity index 100% rename from library/init/lean/extern.lean rename to library/init/lean/compiler/externattr.lean diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index 3c91b6832a..51c7d6f61f 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -5,8 +5,10 @@ Authors: Leonardo de Moura -/ prelude import init.data.array -import init.lean.name init.lean.extern -import init.lean.kvmap init.lean.format +import init.lean.name +import init.lean.kvmap +import init.lean.format +import init.lean.compiler.externattr /- Implements (extended) λPure and λRc proposed in the article "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura. diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean index 419cf8622a..c6f0b832f3 100644 --- a/library/init/lean/compiler/ir/boxing.lean +++ b/library/init/lean/compiler/ir/boxing.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import init.control.estate import init.control.reader -import init.lean.extern +import init.lean.compiler.externattr import init.lean.compiler.ir.basic import init.lean.compiler.ir.compilerm import init.lean.compiler.ir.freevars diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean index 20ea3047bc..4412d67c80 100644 --- a/library/init/lean/default.lean +++ b/library/init/lean/default.lean @@ -5,7 +5,6 @@ Authors: Leonardo de Moura -/ prelude import init.lean.compiler -import init.lean.extern import init.lean.environment import init.lean.modifiers import init.lean.runtime diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index bb52b6d533..cc7b4b3b10 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -449,7 +449,8 @@ int main(int argc, char ** argv) { scope_trace_env scope_trace(env, opts, trace_ctx); name main_module_name; - std::string mod_fn, contents; + std::string mod_fn = ""; + std::string contents; if (use_stdin) { if (argc - optind != 0) { std::cerr << "Expected exactly one of file name or --stdin\n"; @@ -578,7 +579,7 @@ int main(int argc, char ** argv) { return ok ? 0 : 1; } catch (lean::throwable & ex) { - std::cerr << lean::message_builder(env, ios, "", lean::pos_info(1, 1), lean::ERROR).set_exception( + std::cerr << lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR).set_exception( ex).build(); } catch (std::bad_alloc & ex) { std::cerr << "out of memory" << std::endl; diff --git a/src/stage0/CMakeLists.txt b/src/stage0/CMakeLists.txt index 0602cec603..c0e0ec1198 100644 --- a/src/stage0/CMakeLists.txt +++ b/src/stage0/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/extern.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) +add_library (stage0 OBJECT ./init/coe.cpp ./init/control/alternative.cpp ./init/control/applicative.cpp ./init/control/combinators.cpp ./init/control/conditional.cpp ./init/control/default.cpp ./init/control/estate.cpp ./init/control/except.cpp ./init/control/functor.cpp ./init/control/id.cpp ./init/control/lift.cpp ./init/control/monad.cpp ./init/control/monadfail.cpp ./init/control/option.cpp ./init/control/reader.cpp ./init/control/state.cpp ./init/core.cpp ./init/data/array/basic.cpp ./init/data/array/binsearch.cpp ./init/data/array/default.cpp ./init/data/array/qsort.cpp ./init/data/assoclist.cpp ./init/data/basic.cpp ./init/data/bytearray/basic.cpp ./init/data/bytearray/default.cpp ./init/data/char/basic.cpp ./init/data/char/default.cpp ./init/data/default.cpp ./init/data/dlist.cpp ./init/data/fin/basic.cpp ./init/data/fin/default.cpp ./init/data/hashable.cpp ./init/data/hashmap/basic.cpp ./init/data/hashmap/default.cpp ./init/data/int/basic.cpp ./init/data/int/default.cpp ./init/data/list/basic.cpp ./init/data/list/default.cpp ./init/data/list/instances.cpp ./init/data/nat/basic.cpp ./init/data/nat/bitwise.cpp ./init/data/nat/default.cpp ./init/data/nat/div.cpp ./init/data/option/basic.cpp ./init/data/option/instances.cpp ./init/data/ordering/basic.cpp ./init/data/ordering/default.cpp ./init/data/persistentarray/basic.cpp ./init/data/persistentarray/default.cpp ./init/data/random.cpp ./init/data/rbmap/basic.cpp ./init/data/rbmap/default.cpp ./init/data/rbtree/basic.cpp ./init/data/rbtree/default.cpp ./init/data/repr.cpp ./init/data/string/basic.cpp ./init/data/string/default.cpp ./init/data/tostring.cpp ./init/data/uint.cpp ./init/default.cpp ./init/env_ext.cpp ./init/fix.cpp ./init/io.cpp ./init/lean/attributes.cpp ./init/lean/compiler/closedtermcache.cpp ./init/lean/compiler/constfolding.cpp ./init/lean/compiler/default.cpp ./init/lean/compiler/exportattr.cpp ./init/lean/compiler/externattr.cpp ./init/lean/compiler/initattr.cpp ./init/lean/compiler/inline.cpp ./init/lean/compiler/ir/basic.cpp ./init/lean/compiler/ir/borrow.cpp ./init/lean/compiler/ir/boxing.cpp ./init/lean/compiler/ir/checker.cpp ./init/lean/compiler/ir/compilerm.cpp ./init/lean/compiler/ir/default.cpp ./init/lean/compiler/ir/elimdead.cpp ./init/lean/compiler/ir/emitcpp.cpp ./init/lean/compiler/ir/emitutil.cpp ./init/lean/compiler/ir/expandresetreuse.cpp ./init/lean/compiler/ir/format.cpp ./init/lean/compiler/ir/freevars.cpp ./init/lean/compiler/ir/livevars.cpp ./init/lean/compiler/ir/normids.cpp ./init/lean/compiler/ir/pushproj.cpp ./init/lean/compiler/ir/rc.cpp ./init/lean/compiler/ir/resetreuse.cpp ./init/lean/compiler/ir/simpcase.cpp ./init/lean/compiler/util.cpp ./init/lean/declaration.cpp ./init/lean/default.cpp ./init/lean/disjoint_set.cpp ./init/lean/elaborator/default.cpp ./init/lean/elaborator/elabstrategyattrs.cpp ./init/lean/environment.cpp ./init/lean/evalconst.cpp ./init/lean/expr.cpp ./init/lean/format.cpp ./init/lean/kvmap.cpp ./init/lean/level.cpp ./init/lean/message.cpp ./init/lean/modifiers.cpp ./init/lean/name.cpp ./init/lean/name_mangling.cpp ./init/lean/options.cpp ./init/lean/parser/default.cpp ./init/lean/parser/identifier.cpp ./init/lean/parser/level.cpp ./init/lean/parser/parser.cpp ./init/lean/parser/trie.cpp ./init/lean/position.cpp ./init/lean/reducibilityattrs.cpp ./init/lean/runtime.cpp ./init/lean/smap.cpp ./init/lean/syntax.cpp ./init/lean/toexpr.cpp ./init/lean/trace.cpp ./init/lean/util.cpp ./init/platform.cpp ./init/util.cpp ./init/wf.cpp) diff --git a/src/stage0/init/lean/compiler/default.cpp b/src/stage0/init/lean/compiler/default.cpp index 57c8520588..ac8091e9f7 100644 --- a/src/stage0/init/lean/compiler/default.cpp +++ b/src/stage0/init/lean/compiler/default.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.compiler.default -// Imports: init.lean.compiler.inline init.lean.compiler.constfolding init.lean.compiler.closedtermcache init.lean.compiler.ir.default +// Imports: init.lean.compiler.inline init.lean.compiler.constfolding init.lean.compiler.closedtermcache init.lean.compiler.externattr init.lean.compiler.ir.default #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -17,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; obj* initialize_init_lean_compiler_inline(obj*); obj* initialize_init_lean_compiler_constfolding(obj*); obj* initialize_init_lean_compiler_closedtermcache(obj*); +obj* initialize_init_lean_compiler_externattr(obj*); obj* initialize_init_lean_compiler_ir_default(obj*); static bool _G_initialized = false; obj* initialize_init_lean_compiler_default(obj* w) { @@ -29,6 +30,8 @@ w = initialize_init_lean_compiler_constfolding(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_closedtermcache(w); if (io_result_is_error(w)) return w; +w = initialize_init_lean_compiler_externattr(w); +if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_default(w); if (io_result_is_error(w)) return w; return w; diff --git a/src/stage0/init/lean/extern.cpp b/src/stage0/init/lean/compiler/externattr.cpp similarity index 96% rename from src/stage0/init/lean/extern.cpp rename to src/stage0/init/lean/compiler/externattr.cpp index 04c1ecc81a..172633098a 100644 --- a/src/stage0/init/lean/extern.cpp +++ b/src/stage0/init/lean/compiler/externattr.cpp @@ -1,5 +1,5 @@ // Lean compiler output -// Module: init.lean.extern +// Module: init.lean.compiler.externattr // Imports: init.lean.expr init.data.option.basic init.lean.environment #include "runtime/object.h" #include "runtime/apply.h" @@ -45,6 +45,7 @@ obj* mk_extern_call_core(obj*, obj*, obj*); } obj* l_String_Iterator_remainingBytes___main(obj*); obj* l_Lean_isExtern___boxed(obj*, obj*); +obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj*, obj*, obj*); obj* l_List_foldl___main___at_Lean_mkSimpleFnCall___spec__1(obj*, obj*); namespace lean { obj* string_push(obj*, uint32); @@ -78,11 +79,10 @@ uint8 l_UInt32_decEq(uint32, uint32); namespace lean { obj* mk_inline_ext_entry_core(obj*, obj*); } -obj* l___private_init_lean_extern_1__parseOptNum(obj*, obj*, obj*); obj* l_Lean_getExternAttrData___boxed(obj*, obj*); obj* l_Lean_getExternEntryForAux(obj*, obj*); +obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj*, obj*, obj*); obj* l_Lean_getExternEntryForAux___main___boxed(obj*, obj*); -obj* l___private_init_lean_extern_1__parseOptNum___main(obj*, obj*, obj*); uint8 l_String_Iterator_hasNext___main(obj*); obj* l_Lean_getExternEntryForAux___main(obj*, obj*); namespace lean { @@ -163,7 +163,7 @@ return x_3; } } } -obj* l___private_init_lean_extern_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) { +obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) { _start: { obj* x_4; uint8 x_5; @@ -247,11 +247,11 @@ return x_25; } } } -obj* l___private_init_lean_extern_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) { +obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) { _start: { obj* x_4; -x_4 = l___private_init_lean_extern_1__parseOptNum___main(x_1, x_2, x_3); +x_4 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_1, x_2, x_3); return x_4; } } @@ -295,7 +295,7 @@ else obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; x_16 = l_String_Iterator_next___main(x_3); x_17 = l_String_Iterator_remainingBytes___main(x_16); -x_18 = l___private_init_lean_extern_1__parseOptNum___main(x_17, x_16, x_5); +x_18 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_17, x_16, x_5); x_19 = lean::cnstr_get(x_18, 0); lean::inc(x_19); x_20 = lean::cnstr_get(x_18, 1); @@ -874,7 +874,7 @@ obj* initialize_init_lean_expr(obj*); obj* initialize_init_data_option_basic(obj*); obj* initialize_init_lean_environment(obj*); static bool _G_initialized = false; -obj* initialize_init_lean_extern(obj* w) { +obj* initialize_init_lean_compiler_externattr(obj* w) { if (_G_initialized) return w; _G_initialized = true; if (io_result_is_error(w)) return w; diff --git a/src/stage0/init/lean/compiler/ir/basic.cpp b/src/stage0/init/lean/compiler/ir/basic.cpp index cc725c523e..d5d1e3e95e 100644 --- a/src/stage0/init/lean/compiler/ir/basic.cpp +++ b/src/stage0/init/lean/compiler/ir/basic.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.compiler.ir.basic -// Imports: init.data.array.default init.lean.name init.lean.extern init.lean.kvmap init.lean.format +// Imports: init.data.array.default init.lean.name init.lean.kvmap init.lean.format init.lean.compiler.externattr #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -11061,9 +11061,9 @@ return x_12; } obj* initialize_init_data_array_default(obj*); obj* initialize_init_lean_name(obj*); -obj* initialize_init_lean_extern(obj*); obj* initialize_init_lean_kvmap(obj*); obj* initialize_init_lean_format(obj*); +obj* initialize_init_lean_compiler_externattr(obj*); static bool _G_initialized = false; obj* initialize_init_lean_compiler_ir_basic(obj* w) { if (_G_initialized) return w; @@ -11073,12 +11073,12 @@ w = initialize_init_data_array_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_extern(w); -if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(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_lean_compiler_externattr(w); +if (io_result_is_error(w)) return w; REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "Index"), "lt"), 2, l_Lean_IR_Index_lt___boxed); REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "VarId"), "HasBeq"), 2, l_Lean_IR_VarId_HasBeq___boxed); l_Lean_IR_VarId_HasToString___closed__1 = _init_l_Lean_IR_VarId_HasToString___closed__1(); diff --git a/src/stage0/init/lean/compiler/ir/boxing.cpp b/src/stage0/init/lean/compiler/ir/boxing.cpp index 536a41b0c6..cc13b90680 100644 --- a/src/stage0/init/lean/compiler/ir/boxing.cpp +++ b/src/stage0/init/lean/compiler/ir/boxing.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.compiler.ir.boxing -// Imports: init.control.estate init.control.reader init.lean.extern init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars +// Imports: init.control.estate init.control.reader init.lean.compiler.externattr init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -6334,7 +6334,7 @@ return x_4; } obj* initialize_init_control_estate(obj*); obj* initialize_init_control_reader(obj*); -obj* initialize_init_lean_extern(obj*); +obj* initialize_init_lean_compiler_externattr(obj*); obj* initialize_init_lean_compiler_ir_basic(obj*); obj* initialize_init_lean_compiler_ir_compilerm(obj*); obj* initialize_init_lean_compiler_ir_freevars(obj*); @@ -6347,7 +6347,7 @@ w = initialize_init_control_estate(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_lean_extern(w); +w = initialize_init_lean_compiler_externattr(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_basic(w); if (io_result_is_error(w)) return w; diff --git a/src/stage0/init/lean/default.cpp b/src/stage0/init/lean/default.cpp index 789e14f5c2..da2a12f997 100644 --- a/src/stage0/init/lean/default.cpp +++ b/src/stage0/init/lean/default.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.default -// Imports: init.lean.compiler.default init.lean.extern init.lean.environment init.lean.modifiers init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default +// Imports: init.lean.compiler.default init.lean.environment init.lean.modifiers init.lean.runtime init.lean.attributes init.lean.evalconst init.lean.parser.default init.lean.reducibilityattrs init.lean.elaborator.default #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -15,7 +15,6 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif obj* initialize_init_lean_compiler_default(obj*); -obj* initialize_init_lean_extern(obj*); obj* initialize_init_lean_environment(obj*); obj* initialize_init_lean_modifiers(obj*); obj* initialize_init_lean_runtime(obj*); @@ -31,8 +30,6 @@ _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_extern(w); -if (io_result_is_error(w)) return w; w = initialize_init_lean_environment(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_modifiers(w);