From f5aa8ea4f51af23aa851be9366649d3bcac14dae Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 20 Sep 2021 11:27:49 +0200
Subject: [PATCH] chore: update stage0

---
 stage0/src/CMakeLists.txt              |   2 +-
 stage0/src/Lean/Compiler/IR/EmitC.lean |  17 +-
 stage0/src/include/lean/lean.h         |  13 +
 stage0/stdlib/Lean/Compiler/IR/EmitC.c | 394 +++++++++++++------------
 4 files changed, 236 insertions(+), 190 deletions(-)

diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt
index 9eaf425dc6..e7378608a5 100644
--- a/stage0/src/CMakeLists.txt
+++ b/stage0/src/CMakeLists.txt
@@ -181,7 +181,7 @@ endif()
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
-set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"")
+set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
 set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
diff --git a/stage0/src/Lean/Compiler/IR/EmitC.lean b/stage0/src/Lean/Compiler/IR/EmitC.lean
index 307e462098..796c29e61f 100644
--- a/stage0/src/Lean/Compiler/IR/EmitC.lean
+++ b/stage0/src/Lean/Compiler/IR/EmitC.lean
@@ -90,12 +90,15 @@ def toCInitName (n : Name) : M String := do
 def emitCInitName (n : Name) : M Unit :=
   toCInitName n >>= emit
 
-def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit := do
+def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
   let ps := decl.params
   let env ← getEnv
   if ps.isEmpty then
     if isClosedTermName env decl.name then emit "static "
-    else if addExternForConsts then emit "extern "
+    else if isExternal then emit "extern "
+    else emit "LEAN_EXPORT "
+  else
+    if !isExternal then emit "LEAN_EXPORT "
   emit (toCType decl.resultType ++ " " ++ cppBaseName)
   unless ps.isEmpty do
     emit "("
@@ -110,15 +113,15 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Boo
     emit ")"
   emitLn ";"
 
-def emitFnDecl (decl : Decl) (addExternForConsts : Bool) : M Unit := do
+def emitFnDecl (decl : Decl) (isExternal : Bool) : M Unit := do
   let cppBaseName ← toCName decl.name
-  emitFnDeclAux decl cppBaseName addExternForConsts
+  emitFnDeclAux decl cppBaseName isExternal
 
 def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := do
   let cName := Name.mkSimple cNameStr
   let env ← getEnv
   let extC := isExternC env decl.name
-  emitFnDeclAux decl cNameStr (!extC)
+  emitFnDeclAux decl cNameStr extC
 
 def emitFnDecls : M Unit := do
   let env ← getEnv
@@ -643,6 +646,8 @@ def emitDeclAux (d : Decl) : M Unit := do
       let baseName ← toCName f;
       if xs.size == 0 then
         emit "static "
+      else
+        emit "LEAN_EXPORT "  -- make symbol visible to the interpreter
       emit (toCType t); emit " ";
       if xs.size > 0 then
         emit baseName;
@@ -709,7 +714,7 @@ def emitInitFn : M Unit := do
   env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(lean_object*);")
   emitLns [
     "static bool _G_initialized = false;",
-    "lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(lean_object* w) {",
+    "LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(lean_object* w) {",
     "lean_object * res;",
     "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
     "_G_initialized = true;"
diff --git a/stage0/src/include/lean/lean.h b/stage0/src/include/lean/lean.h
index bd2989d6d3..5bb09ac4f5 100644
--- a/stage0/src/include/lean/lean.h
+++ b/stage0/src/include/lean/lean.h
@@ -46,6 +46,19 @@ extern "C" {
 #define LEAN_ALWAYS_INLINE
 #endif
 
+#ifdef _WIN32
+#define LEAN_EXPORT __declspec(dllexport)
+#else
+#define LEAN_EXPORT
+#endif
+
+// We set `LEAN_EXPORTING` when compiling objects of libleanshared, but not when including this header in any other context.
+#if defined LEAN_EXPORTING
+#define LEAN_SHARED LEAN_EXPORT
+#else
+#define LEAN_SHARED
+#endif
+
 #ifdef LEAN_RUNTIME_STATS
 #define LEAN_RUNTIME_STAT_CODE(c) c
 #else
diff --git a/stage0/stdlib/Lean/Compiler/IR/EmitC.c b/stage0/stdlib/Lean/Compiler/IR/EmitC.c
index c1a25c78ec..28d24c98ff 100644
--- a/stage0/stdlib/Lean/Compiler/IR/EmitC.c
+++ b/stage0/stdlib/Lean/Compiler/IR/EmitC.c
@@ -470,6 +470,7 @@ lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1___lambda__1__
 lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitTag(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__11;
 lean_object* l_Lean_IR_EmitC_emitDecl(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_throwUnknownVar(lean_object*);
 lean_object* l_Lean_IR_EmitC_isIf(lean_object*);
@@ -528,6 +529,7 @@ lean_object* l_Lean_IR_EmitC_emitFullApp(lean_object*, lean_object*, lean_object
 uint8_t l_Lean_IR_usesModuleFrom(lean_object*, lean_object*);
 static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__30;
 static lean_object* l_Lean_IR_EmitC_declareVar___closed__1;
+static lean_object* l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
 lean_object* l_Lean_IR_EmitC_declareVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_emitSSet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_mod(lean_object*, lean_object*);
@@ -2123,7 +2125,7 @@ static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("extern ");
+x_1 = lean_mk_string("LEAN_EXPORT ");
 return x_1;
 }
 }
@@ -2131,6 +2133,14 @@ static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__2() {
 _start:
 {
 lean_object* x_1; 
+x_1 = lean_mk_string("extern ");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__3() {
+_start:
+{
+lean_object* x_1; 
 x_1 = lean_mk_string("static ");
 return x_1;
 }
@@ -2149,44 +2159,58 @@ lean_dec(x_7);
 x_10 = l_Array_isEmpty___rarg(x_6);
 if (x_10 == 0)
 {
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_box(0);
-x_12 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_11, x_4, x_9);
-return x_12;
+if (x_3 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_11 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
+x_12 = lean_string_append(x_9, x_11);
+x_13 = lean_box(0);
+x_14 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_13, x_4, x_12);
+return x_14;
 }
 else
 {
-lean_object* x_13; uint8_t x_14; 
-x_13 = l_Lean_IR_Decl_name(x_1);
-x_14 = l_Lean_isClosedTermName(x_8, x_13);
-lean_dec(x_13);
-if (x_14 == 0)
-{
-if (x_3 == 0)
-{
 lean_object* x_15; lean_object* x_16; 
 x_15 = lean_box(0);
 x_16 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_15, x_4, x_9);
 return x_16;
 }
+}
 else
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
-x_17 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
-x_18 = lean_string_append(x_9, x_17);
-x_19 = lean_box(0);
-x_20 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_19, x_4, x_18);
-return x_20;
+lean_object* x_17; uint8_t x_18; 
+x_17 = l_Lean_IR_Decl_name(x_1);
+x_18 = l_Lean_isClosedTermName(x_8, x_17);
+lean_dec(x_17);
+if (x_18 == 0)
+{
+if (x_3 == 0)
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_19 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
+x_20 = lean_string_append(x_9, x_19);
+x_21 = lean_box(0);
+x_22 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_21, x_4, x_20);
+return x_22;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_23 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
+x_24 = lean_string_append(x_9, x_23);
+x_25 = lean_box(0);
+x_26 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_25, x_4, x_24);
+return x_26;
 }
 }
 else
 {
-lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
-x_21 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
-x_22 = lean_string_append(x_9, x_21);
-x_23 = lean_box(0);
-x_24 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_23, x_4, x_22);
-return x_24;
+lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
+x_27 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
+x_28 = lean_string_append(x_9, x_27);
+x_29 = lean_box(0);
+x_30 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_29, x_4, x_28);
+return x_30;
 }
 }
 }
@@ -2332,7 +2356,7 @@ return x_6;
 lean_object* l_Lean_IR_EmitC_emitExternDeclAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; 
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; 
 x_5 = l_Lean_IR_EmitC_getEnv(x_3, x_4);
 x_6 = lean_ctor_get(x_5, 0);
 lean_inc(x_6);
@@ -2341,20 +2365,8 @@ lean_inc(x_7);
 lean_dec(x_5);
 x_8 = l_Lean_IR_Decl_name(x_1);
 x_9 = l_Lean_isExternC(x_6, x_8);
-if (x_9 == 0)
-{
-uint8_t x_10; lean_object* x_11; 
-x_10 = 1;
-x_11 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_10, x_3, x_7);
-return x_11;
-}
-else
-{
-uint8_t x_12; lean_object* x_13; 
-x_12 = 0;
-x_13 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_12, x_3, x_7);
-return x_13;
-}
+x_10 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_9, x_3, x_7);
+return x_10;
 }
 }
 lean_object* l_List_foldl___at_Lean_IR_EmitC_emitFnDecls___spec__1(lean_object* x_1, lean_object* x_2) {
@@ -11629,19 +11641,19 @@ lean_inc(x_10);
 x_11 = l_Lean_hasInitAttr(x_5, x_10);
 if (x_11 == 0)
 {
-uint8_t x_61; 
-x_61 = 0;
-x_12 = x_61;
-goto block_60;
+uint8_t x_65; 
+x_65 = 0;
+x_12 = x_65;
+goto block_64;
 }
 else
 {
-uint8_t x_62; 
-x_62 = 1;
-x_12 = x_62;
-goto block_60;
+uint8_t x_66; 
+x_66 = 1;
+x_12 = x_66;
+goto block_64;
 }
-block_60:
+block_64:
 {
 if (x_12 == 0)
 {
@@ -11681,168 +11693,172 @@ x_24 = lean_nat_dec_eq(x_22, x_23);
 lean_dec(x_22);
 if (x_24 == 0)
 {
-lean_object* x_25; lean_object* x_26; 
-x_25 = lean_box(0);
-x_26 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_25, x_2, x_21);
-return x_26;
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_25 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
+x_26 = lean_string_append(x_21, x_25);
+x_27 = lean_box(0);
+x_28 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_27, x_2, x_26);
+return x_28;
 }
 else
 {
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-x_27 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
-x_28 = lean_string_append(x_21, x_27);
-x_29 = lean_box(0);
-x_30 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_29, x_2, x_28);
-return x_30;
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_29 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
+x_30 = lean_string_append(x_21, x_29);
+x_31 = lean_box(0);
+x_32 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_31, x_2, x_30);
+return x_32;
 }
 }
 else
 {
-uint8_t x_31; 
+uint8_t x_33; 
 lean_dec(x_2);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
 lean_dec(x_13);
 lean_dec(x_10);
-x_31 = !lean_is_exclusive(x_19);
-if (x_31 == 0)
+x_33 = !lean_is_exclusive(x_19);
+if (x_33 == 0)
 {
 return x_19;
 }
 else
 {
-lean_object* x_32; lean_object* x_33; lean_object* x_34; 
-x_32 = lean_ctor_get(x_19, 0);
-x_33 = lean_ctor_get(x_19, 1);
-lean_inc(x_33);
-lean_inc(x_32);
+lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_34 = lean_ctor_get(x_19, 0);
+x_35 = lean_ctor_get(x_19, 1);
+lean_inc(x_35);
+lean_inc(x_34);
 lean_dec(x_19);
-x_34 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_34, 0, x_32);
-lean_ctor_set(x_34, 1, x_33);
-return x_34;
+x_36 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_36, 0, x_34);
+lean_ctor_set(x_36, 1, x_35);
+return x_36;
 }
 }
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
-x_35 = lean_ctor_get(x_2, 0);
-x_36 = lean_ctor_get(x_2, 1);
-x_37 = lean_ctor_get(x_2, 3);
-x_38 = lean_ctor_get(x_2, 4);
+lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+x_37 = lean_ctor_get(x_2, 0);
+x_38 = lean_ctor_get(x_2, 1);
+x_39 = lean_ctor_get(x_2, 3);
+x_40 = lean_ctor_get(x_2, 4);
+lean_inc(x_40);
+lean_inc(x_39);
 lean_inc(x_38);
 lean_inc(x_37);
-lean_inc(x_36);
-lean_inc(x_35);
 lean_dec(x_2);
-x_39 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_39, 0, x_35);
-lean_ctor_set(x_39, 1, x_36);
-lean_ctor_set(x_39, 2, x_9);
-lean_ctor_set(x_39, 3, x_37);
-lean_ctor_set(x_39, 4, x_38);
+x_41 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_41, 0, x_37);
+lean_ctor_set(x_41, 1, x_38);
+lean_ctor_set(x_41, 2, x_9);
+lean_ctor_set(x_41, 3, x_39);
+lean_ctor_set(x_41, 4, x_40);
 lean_inc(x_13);
-x_40 = l_Lean_IR_EmitC_toCName(x_13, x_39, x_6);
-if (lean_obj_tag(x_40) == 0)
+x_42 = l_Lean_IR_EmitC_toCName(x_13, x_41, x_6);
+if (lean_obj_tag(x_42) == 0)
 {
-lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; 
-x_41 = lean_ctor_get(x_40, 0);
-lean_inc(x_41);
-x_42 = lean_ctor_get(x_40, 1);
-lean_inc(x_42);
-lean_dec(x_40);
-x_43 = lean_array_get_size(x_14);
-x_44 = lean_unsigned_to_nat(0u);
-x_45 = lean_nat_dec_eq(x_43, x_44);
-lean_dec(x_43);
-if (x_45 == 0)
-{
-lean_object* x_46; lean_object* x_47; 
-x_46 = lean_box(0);
-x_47 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_41, x_46, x_39, x_42);
-return x_47;
-}
-else
+lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; 
+x_43 = lean_ctor_get(x_42, 0);
+lean_inc(x_43);
+x_44 = lean_ctor_get(x_42, 1);
+lean_inc(x_44);
+lean_dec(x_42);
+x_45 = lean_array_get_size(x_14);
+x_46 = lean_unsigned_to_nat(0u);
+x_47 = lean_nat_dec_eq(x_45, x_46);
+lean_dec(x_45);
+if (x_47 == 0)
 {
 lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; 
-x_48 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
-x_49 = lean_string_append(x_42, x_48);
+x_48 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
+x_49 = lean_string_append(x_44, x_48);
 x_50 = lean_box(0);
-x_51 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_41, x_50, x_39, x_49);
+x_51 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_43, x_50, x_41, x_49);
 return x_51;
 }
-}
 else
 {
 lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; 
-lean_dec(x_39);
+x_52 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
+x_53 = lean_string_append(x_44, x_52);
+x_54 = lean_box(0);
+x_55 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_43, x_54, x_41, x_53);
+return x_55;
+}
+}
+else
+{
+lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; 
+lean_dec(x_41);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_14);
 lean_dec(x_13);
 lean_dec(x_10);
-x_52 = lean_ctor_get(x_40, 0);
-lean_inc(x_52);
-x_53 = lean_ctor_get(x_40, 1);
-lean_inc(x_53);
-if (lean_is_exclusive(x_40)) {
- lean_ctor_release(x_40, 0);
- lean_ctor_release(x_40, 1);
- x_54 = x_40;
+x_56 = lean_ctor_get(x_42, 0);
+lean_inc(x_56);
+x_57 = lean_ctor_get(x_42, 1);
+lean_inc(x_57);
+if (lean_is_exclusive(x_42)) {
+ lean_ctor_release(x_42, 0);
+ lean_ctor_release(x_42, 1);
+ x_58 = x_42;
 } else {
- lean_dec_ref(x_40);
- x_54 = lean_box(0);
+ lean_dec_ref(x_42);
+ x_58 = lean_box(0);
 }
-if (lean_is_scalar(x_54)) {
- x_55 = lean_alloc_ctor(1, 2, 0);
+if (lean_is_scalar(x_58)) {
+ x_59 = lean_alloc_ctor(1, 2, 0);
 } else {
- x_55 = x_54;
+ x_59 = x_58;
 }
-lean_ctor_set(x_55, 0, x_52);
-lean_ctor_set(x_55, 1, x_53);
-return x_55;
-}
-}
-}
-else
-{
-lean_object* x_56; lean_object* x_57; 
-lean_dec(x_10);
-lean_dec(x_9);
-lean_dec(x_2);
-lean_dec(x_1);
-x_56 = lean_box(0);
-if (lean_is_scalar(x_7)) {
- x_57 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_57 = x_7;
-}
-lean_ctor_set(x_57, 0, x_56);
-lean_ctor_set(x_57, 1, x_6);
-return x_57;
-}
-}
-else
-{
-lean_object* x_58; lean_object* x_59; 
-lean_dec(x_10);
-lean_dec(x_9);
-lean_dec(x_2);
-lean_dec(x_1);
-x_58 = lean_box(0);
-if (lean_is_scalar(x_7)) {
- x_59 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_59 = x_7;
-}
-lean_ctor_set(x_59, 0, x_58);
-lean_ctor_set(x_59, 1, x_6);
+lean_ctor_set(x_59, 0, x_56);
+lean_ctor_set(x_59, 1, x_57);
 return x_59;
 }
 }
 }
+else
+{
+lean_object* x_60; lean_object* x_61; 
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+x_60 = lean_box(0);
+if (lean_is_scalar(x_7)) {
+ x_61 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_61 = x_7;
+}
+lean_ctor_set(x_61, 0, x_60);
+lean_ctor_set(x_61, 1, x_6);
+return x_61;
+}
+}
+else
+{
+lean_object* x_62; lean_object* x_63; 
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+x_62 = lean_box(0);
+if (lean_is_scalar(x_7)) {
+ x_63 = lean_alloc_ctor(0, 2, 0);
+} else {
+ x_63 = x_7;
+}
+lean_ctor_set(x_63, 0, x_62);
+lean_ctor_set(x_63, 1, x_6);
+return x_63;
+}
+}
+}
 }
 lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
@@ -12999,7 +13015,7 @@ static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("(lean_object* w) {");
+x_1 = lean_mk_string("LEAN_EXPORT lean_object* ");
 return x_1;
 }
 }
@@ -13007,23 +13023,31 @@ static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__2() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("_G_initialized = true;");
+x_1 = lean_mk_string("(lean_object* w) {");
 return x_1;
 }
 }
 static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__3() {
 _start:
 {
+lean_object* x_1; 
+x_1 = lean_mk_string("_G_initialized = true;");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__4() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_IR_EmitC_emitInitFn___closed__2;
+x_2 = l_Lean_IR_EmitC_emitInitFn___closed__3;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__4() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__5() {
 _start:
 {
 lean_object* x_1; 
@@ -13031,19 +13055,19 @@ x_1 = lean_mk_string("if (_G_initialized) return lean_io_result_mk_ok(lean_box(0
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__5() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_IR_EmitC_emitInitFn___closed__4;
-x_2 = l_Lean_IR_EmitC_emitInitFn___closed__3;
+x_1 = l_Lean_IR_EmitC_emitInitFn___closed__5;
+x_2 = l_Lean_IR_EmitC_emitInitFn___closed__4;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__6() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__7() {
 _start:
 {
 lean_object* x_1; 
@@ -13051,19 +13075,19 @@ x_1 = lean_mk_string("lean_object * res;");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__7() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_IR_EmitC_emitInitFn___closed__6;
-x_2 = l_Lean_IR_EmitC_emitInitFn___closed__5;
+x_1 = l_Lean_IR_EmitC_emitInitFn___closed__7;
+x_2 = l_Lean_IR_EmitC_emitInitFn___closed__6;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__8() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__9() {
 _start:
 {
 lean_object* x_1; 
@@ -13071,7 +13095,7 @@ x_1 = lean_mk_string("static bool _G_initialized = false;");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__9() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__10() {
 _start:
 {
 lean_object* x_1; 
@@ -13079,11 +13103,11 @@ x_1 = lean_mk_string("return lean_io_result_mk_ok(lean_box(0));");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__10() {
+static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_IR_EmitC_emitInitFn___closed__9;
+x_1 = l_Lean_IR_EmitC_emitInitFn___closed__10;
 x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__14;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
@@ -13143,17 +13167,17 @@ block_65:
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; 
 x_12 = lean_mk_module_initialization_function_name(x_7);
-x_13 = l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___closed__1;
+x_13 = l_Lean_IR_EmitC_emitInitFn___closed__1;
 x_14 = lean_string_append(x_13, x_12);
 lean_dec(x_12);
-x_15 = l_Lean_IR_EmitC_emitInitFn___closed__1;
+x_15 = l_Lean_IR_EmitC_emitInitFn___closed__2;
 x_16 = lean_string_append(x_14, x_15);
 x_17 = lean_box(0);
-x_18 = l_Lean_IR_EmitC_emitInitFn___closed__7;
+x_18 = l_Lean_IR_EmitC_emitInitFn___closed__8;
 x_19 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_19, 0, x_16);
 lean_ctor_set(x_19, 1, x_18);
-x_20 = l_Lean_IR_EmitC_emitInitFn___closed__8;
+x_20 = l_Lean_IR_EmitC_emitInitFn___closed__9;
 x_21 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_21, 0, x_20);
 lean_ctor_set(x_21, 1, x_19);
@@ -13181,7 +13205,7 @@ lean_object* x_30; lean_object* x_31; lean_object* x_32;
 x_30 = lean_ctor_get(x_29, 1);
 lean_inc(x_30);
 lean_dec(x_29);
-x_31 = l_Lean_IR_EmitC_emitInitFn___closed__10;
+x_31 = l_Lean_IR_EmitC_emitInitFn___closed__11;
 x_32 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_31, x_1, x_30);
 return x_32;
 }
@@ -13229,7 +13253,7 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44;
 x_42 = lean_ctor_get(x_41, 1);
 lean_inc(x_42);
 lean_dec(x_41);
-x_43 = l_Lean_IR_EmitC_emitInitFn___closed__10;
+x_43 = l_Lean_IR_EmitC_emitInitFn___closed__11;
 x_44 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_43, x_1, x_42);
 return x_44;
 }
@@ -13280,7 +13304,7 @@ lean_object* x_58; lean_object* x_59; lean_object* x_60;
 x_58 = lean_ctor_get(x_57, 1);
 lean_inc(x_58);
 lean_dec(x_57);
-x_59 = l_Lean_IR_EmitC_emitInitFn___closed__10;
+x_59 = l_Lean_IR_EmitC_emitInitFn___closed__11;
 x_60 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_59, x_1, x_58);
 return x_60;
 }
@@ -13656,6 +13680,8 @@ l_Lean_IR_EmitC_emitFnDeclAux___closed__1 = _init_l_Lean_IR_EmitC_emitFnDeclAux_
 lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__1);
 l_Lean_IR_EmitC_emitFnDeclAux___closed__2 = _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__2();
 lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__2);
+l_Lean_IR_EmitC_emitFnDeclAux___closed__3 = _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__3();
+lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__3);
 l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1 = _init_l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1();
 lean_mark_persistent(l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1);
 l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__2 = _init_l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__2();
@@ -14068,6 +14094,8 @@ l_Lean_IR_EmitC_emitInitFn___closed__9 = _init_l_Lean_IR_EmitC_emitInitFn___clos
 lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__9);
 l_Lean_IR_EmitC_emitInitFn___closed__10 = _init_l_Lean_IR_EmitC_emitInitFn___closed__10();
 lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__10);
+l_Lean_IR_EmitC_emitInitFn___closed__11 = _init_l_Lean_IR_EmitC_emitInitFn___closed__11();
+lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__11);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus