From 75f4eb2f84da04f51d41a455c3f4b5a9639fdcab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Feb 2019 09:21:17 -0800 Subject: [PATCH] feat(library/compiler/emit_cpp): initialize task_manager at generated `main` function --- src/library/compiler/emit_cpp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 62afa20d9a..0541495e9a 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -962,6 +962,7 @@ static void emit_main_fn(std::ostream & out, environment const & env, module_nam else out << "lean::initialize_runtime_module();\n"; out << "initialize_" << mangle(m, false) << "();\n"; + out << "lean::scoped_task_manager tmanager(lean::hardware_concurrency());\n"; if (arity == 2) { out << "obj* in = lean::box(0);\n"; out << "int i = argc;\n";