fix(runtime, library/init/lean/compiler/ir/emitc): missing export, ensure we can compile with C++ compiler

library/init/lean/compiler/ir/emitc.lean

@@ -187,7 +187,10 @@ match d with
   unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
   env ← getEnv;
   let usesLeanAPI := usesLeanNamespace env d;
-  when usesLeanAPI (emitLn "void lean_initialize();");
+  if usesLeanAPI then
+    emitLn "void lean_initialize();"
+  else
+    emitLn "void lean_initialize_runtime_module();";
   emitLn "int main(int argc, char ** argv) {\nlean_object* w; lean_object* in;";
   if usesLeanAPI then
     emitLn "lean_initialize();"
@@ -251,7 +254,18 @@ emitLns [
  "#pragma GCC diagnostic ignored \"-Wunused-parameter\"",
  "#pragma GCC diagnostic ignored \"-Wunused-label\"",
  "#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"",
- "#endif"]
+ "#endif",
+ "#ifdef __cplusplus",
+ "extern \"C\" {",
+ "#endif"
+]
+
+def emitFileFooter : M Unit :=
+emitLns [
+ "#ifdef __cplusplus",
+ "}",
+ "#endif"
+]
 
 def throwUnknownVar {α : Type} (x : VarId) : M α :=
 throw ("unknown variable '" ++ toString x ++ "'")
@@ -746,7 +760,8 @@ emitFileHeader;
 emitFnDecls;
 emitFns;
 emitInitFn;
-emitMainFnIfNeeded
+emitMainFnIfNeeded;
+emitFileFooter
 
 end EmitC
 

src/init/init.cpp

@@ -24,7 +24,7 @@ lean::object* initialize_init_lean_default(lean::object* w);
 namespace lean {
 object* sort_const_table_core(object * w);
 
-void initialize() {
+extern "C" void lean_initialize() {
     save_stack_info();
     initialize_util_module();
     object * w = initialize_init_default(io_mk_world());
@@ -48,6 +48,10 @@ void initialize() {
     initialize_frontend_lean_module();
 }
 
+void initialize() {
+    lean_initialize();
+}
+
 void finalize() {
 #ifdef LEAN_TRACK_CUSTOM_ALLOCATORS
     std::cerr << "memory deallocated by memory_pool (before finalization): " << get_memory_deallocated() << "\n";

src/runtime/init_module.cpp

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "runtime/io.h"
 
 namespace lean {
-void initialize_runtime_module() {
+extern "C" void lean_initialize_runtime_module() {
     initialize_alloc();
     initialize_debug();
     initialize_object();
@@ -20,6 +20,9 @@ void initialize_runtime_module() {
     initialize_serializer();
     initialize_thread();
 }
+void initialize_runtime_module() {
+    lean_initialize_runtime_module();
+}
 void finalize_runtime_module() {
     finalize_thread();
     finalize_serializer();