From 28b9d17a14f9c5d5d3bcd9a98e7d5ca2479ede4b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 May 2014 10:04:42 -0700 Subject: [PATCH] perf(library/module): do not use multiple threads when skipping type checking, add flag to disable/enable type checking theorems asynchronously Signed-off-by: Leonardo de Moura --- src/library/module.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/library/module.cpp b/src/library/module.cpp index 8dfc086f5..7c7c4c48b 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -22,6 +22,10 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "version.h" +#ifndef LEAN_ASYNCH_IMPORT_THEOREM +#define LEAN_ASYNCH_IMPORT_THEOREM false +#endif + namespace lean { typedef std::pair> writer; @@ -110,7 +114,7 @@ static void declaration_reader(deserializer & d, module_idx midx, shared_environ environment env = senv.env(); if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { senv.add(decl); - } else if (decl.is_theorem()) { + } else if (LEAN_ASYNCH_IMPORT_THEOREM && decl.is_theorem()) { // First, we add the theorem as an axiom, and create an asychronous task for // checking the actual theorem, and replace the axiom with the actual theorem. certified_declaration tmp_c = check(env, mk_axiom(decl.get_name(), decl.get_params(), decl.get_type())); @@ -200,6 +204,10 @@ struct import_modules_fn { if (m_num_threads > 1) m_num_threads = 1; #endif + if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) { + // it doesn't payoff to use multiple threads if we will not type check anything + m_num_threads = 1; + } } module_info_ptr load_module_file(std::string const & mname) {