From 41a4eaacd3edd0e48c95f62505b2ee0ad5ea00ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Aug 2019 15:51:39 -0700
Subject: [PATCH] fix(runtime, library/init/lean/compiler/ir/emitc): missing
 export, ensure we can compile with C++ compiler

---
 library/init/lean/compiler/ir/emitc.lean | 21 ++++++++++++++++++---
 src/init/init.cpp                        |  6 +++++-
 src/runtime/init_module.cpp              |  5 ++++-
 3 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/library/init/lean/compiler/ir/emitc.lean b/library/init/lean/compiler/ir/emitc.lean
index 4df6e12cb7..a1b76a0484 100644
--- a/library/init/lean/compiler/ir/emitc.lean
+++ b/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
 
diff --git a/src/init/init.cpp b/src/init/init.cpp
index 064503c122..a98608ab54 100644
--- a/src/init/init.cpp
+++ b/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";
diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp
index 9f31641319..9caf4c4cf1 100644
--- a/src/runtime/init_module.cpp
+++ b/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();