From 8a3522c8e50bc6e412e521827287792f3926163a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Aug 2019 19:26:03 -0700
Subject: [PATCH] chore(library/init/lean/compiler/ir/emitcpp): small hack for
 exporting functions as C functions instead of C++

---
 library/init/lean/compiler/ir/emitcpp.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index ef1d597b31..b202d7413d 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -125,10 +125,20 @@ do env ← getEnv;
 def emitCppInitName (n : Name) : M Unit :=
 toCppInitName n >>= emit
 
+def isSimpleExportName (n : Name) : M Bool :=
+do env ← getEnv;
+   match getExportNameFor env n with
+   | some (Name.mkString Name.anonymous s) => pure true
+   | _ => pure false
+
 def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit :=
 do
 let ps := decl.params;
-when (ps.isEmpty && addExternForConsts) (emit "extern ");
+if ps.isEmpty && addExternForConsts then
+  emit "extern "
+else
+  -- Temporary hack for transitioning to C
+  mwhen (isSimpleExportName decl.name) (emit "extern \"C\" ");
 emit (toCppType decl.resultType ++ " " ++ cppBaseName);
 unless (ps.isEmpty) $ do {
   emit "(";