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

feat(library/compiler/emit_cpp): initialize task_manager at generated main function

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-17 09:21:17 -08:00
parent 170579c803
commit 75f4eb2f84
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/compiler/emit_cpp.cpp
View file

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