michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add parallel_import option

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-25 22:46:49 -07:00
parent 709b5ce90f
commit 3ec30bf537
1 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/parser.cpp
View file

@ -39,14 +39,21 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
#endif #endif
#ifndef LEAN_DEFAULT_PARSER_PARALLEL_IMPORT
#define LEAN_DEFAULT_PARSER_PARALLEL_IMPORT false
#endif
namespace lean { namespace lean {
// ========================================== // ==========================================
// Parser configuration options // Parser configuration options
static name g_parser_show_errors {"lean", "parser", "show_errors"}; static name g_parser_show_errors {"parser", "show_errors"};
static name g_parser_parallel_import {"parser", "parallel_import"};
RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel"); RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel");
RegisterBoolOption(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT, "(lean parser) import modules in parallel");
bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); } bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); }
bool get_parser_parallel_import(options const & opts) { return opts.get_bool(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT); }
// ========================================== // ==========================================
parser::local_scope::local_scope(parser & p): parser::local_scope::local_scope(parser & p):
@ -1020,7 +1027,10 @@ void parser::parse_imports() {
next(); next();
} }
} }
m_env = import_modules(m_env, olean_files.size(), olean_files.data(), m_num_threads, true, m_ios); unsigned num_threads = 0;
if (get_parser_parallel_import(m_ios.get_options()))
num_threads = m_num_threads;
m_env = import_modules(m_env, olean_files.size(), olean_files.data(), num_threads, true, m_ios);
for (auto const & f : lua_files) { for (auto const & f : lua_files) {
std::string rname = find_file(f, {".lua"}); std::string rname = find_file(f, {".lua"});
system_import(rname.c_str()); system_import(rname.c_str());