max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/compiler/ir/emitcpp): add missing lean::

Browse source 
@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.
This commit is contained in:
Leonardo de Moura 2019-08-21 09:51:01 -07:00
parent 166eff9525
commit 78d87cf4cd
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -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;

8
src/stage0/init/lean/compiler/ir/emitcpp.cpp generated
View file

@ -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;
}
}