From 78d87cf4cdfcfcf0345bb72edf5c020391304c71 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Aug 2019 09:51:01 -0700
Subject: [PATCH] fix(library/init/lean/compiler/ir/emitcpp): add missing
 `lean::`

@kha It is unclear why the C++ compilers were accepting our generated
files without `lean::`. I found the issue by accident while working on
the new C backend.
---
 library/init/lean/compiler/ir/emitcpp.lean   | 16 ++++++++--------
 src/stage0/init/lean/compiler/ir/emitcpp.cpp |  8 ++++----
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 8da6bf8930..b2cf9fd918 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -205,7 +205,7 @@ match d with
   modName ← getModName;
   emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);");
   emitLns ["lean::io_mark_end_initialization();",
-           "if (io_result_is_ok(w)) {",
+           "if (lean::io_result_is_ok(w)) {",
            "lean::scoped_task_manager tmanager(lean::hardware_concurrency());"];
   if xs.size == 2 then do {
     emitLns ["obj* in = lean::box(0);",
@@ -220,8 +220,8 @@ match d with
     emitLn ("w = " ++ leanMainFn ++ "(w);")
   };
   emitLn "}";
-  emitLns ["if (io_result_is_ok(w)) {",
-           "  int ret = lean::unbox(io_result_get_value(w));",
+  emitLns ["if (lean::io_result_is_ok(w)) {",
+           "  int ret = lean::unbox(lean::io_result_get_value(w));",
            "  lean::dec_ref(w);",
            "  return ret;",
            "} else {",
@@ -711,13 +711,13 @@ env ← getEnv;
 let n := d.name;
 if isIOUnitInitFn env n then do {
   emit "w = "; emitCppName n; emitLn "(w);";
-  emitLn "if (io_result_is_error(w)) return w;"
+  emitLn "if (lean::io_result_is_error(w)) return w;"
 } else when (d.params.size == 0) $ do {
   match getInitFnNameFor env d.name with
   | some initFn => do {
     emit "w = "; emitCppName initFn; emitLn "(w);";
-    emitLn "if (io_result_is_error(w)) return w;";
-    emitCppName n; emitLn " = io_result_get_value(w);"
+    emitLn "if (lean::io_result_is_error(w)) return w;";
+    emitCppName n; emitLn " = lean::io_result_get_value(w);"
   }
   | _ => do {
     emitCppName n; emit " = "; emitCppInitName n; emitLn "();"
@@ -737,11 +737,11 @@ emitLns [
     "obj* initialize_" ++ modName.mangle "" ++ "(obj* w) {",
     "if (_G_initialized) return w;",
     "_G_initialized = true;",
-    "if (io_result_is_error(w)) return w;"
+    "if (lean::io_result_is_error(w)) return w;"
 ];
 env.imports.mfor $ fun m => emitLns [
   "w = initialize_" ++ m.mangle "" ++ "(w);",
-  "if (io_result_is_error(w)) return w;"
+  "if (lean::io_result_is_error(w)) return w;"
 ];
 let decls := getDecls env;
 decls.reverse.mfor emitDeclInit;
diff --git a/src/stage0/init/lean/compiler/ir/emitcpp.cpp b/src/stage0/init/lean/compiler/ir/emitcpp.cpp
index d50a191d1c..2ac76278a9 100644
--- a/src/stage0/init/lean/compiler/ir/emitcpp.cpp
+++ b/src/stage0/init/lean/compiler/ir/emitcpp.cpp
@@ -4979,7 +4979,7 @@ obj* _init_l_Lean_IR_EmitCpp_emitMainFn___closed__7() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string("if (io_result_is_ok(w)) {");
+x_1 = lean::mk_string("if (lean::io_result_is_ok(w)) {");
 return x_1;
 }
 }
@@ -5171,7 +5171,7 @@ obj* _init_l_Lean_IR_EmitCpp_emitMainFn___closed__26() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string("  int ret = lean::unbox(io_result_get_value(w));");
+x_1 = lean::mk_string("  int ret = lean::unbox(lean::io_result_get_value(w));");
 return x_1;
 }
 }
@@ -26213,7 +26213,7 @@ obj* _init_l_Lean_IR_EmitCpp_emitDeclInit___closed__3() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string("if (io_result_is_error(w)) return w;");
+x_1 = lean::mk_string("if (lean::io_result_is_error(w)) return w;");
 return x_1;
 }
 }
@@ -26221,7 +26221,7 @@ obj* _init_l_Lean_IR_EmitCpp_emitDeclInit___closed__4() {
 _start:
 {
 obj* x_1; 
-x_1 = lean::mk_string(" = io_result_get_value(w);");
+x_1 = lean::mk_string(" = lean::io_result_get_value(w);");
 return x_1;
 }
 }