diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 65cb0cca1..f148c0e01 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -238,6 +238,9 @@ server::server(environment const & env, io_state const & ios, unsigned num_threa m_env(env), m_ios(ios), m_out(ios.get_regular_channel().get_stream()), m_num_threads(num_threads), m_empty_snapshot(m_env, m_ios.get_options()), m_worker(env, ios, m_cache) { +#if !defined(LEAN_MULTI_THREAD) + lean_unreachable(); +#endif } server::~server() { diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 84fc68b72..4718d0a07 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -47,6 +47,7 @@ FOREACH(T ${LEANRUNTESTS}) COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) +if("${MULTI_THREAD}" MATCHES "ON") # LEAN INTERACTIVE TESTS file(GLOB LEANITTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.input") FOREACH(T ${LEANITTESTS}) @@ -55,6 +56,7 @@ FOREACH(T ${LEANITTESTS}) WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) +endif() # LEAN SLOW TESTS file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean") diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index f901214e7..a082bc636 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -78,8 +78,10 @@ static void display_help(std::ostream & out) { std::cout << " 0 means 'do not check'.\n"; std::cout << " --trust=num -t trust level (default: 0) \n"; std::cout << " --quiet -q do not print verbose messages\n"; +#if defined(LEAN_MULTI_THREAD) std::cout << " --server start Lean in 'server' mode\n"; std::cout << " --threads=num -j number of threads used to process lean files\n"; +#endif std::cout << " --deps just print dependencies of a Lean input\n"; std::cout << " --flycheck print structured error message for flycheck\n"; std::cout << " --cache=file -c load/save cached definitions from/to the given file\n"; @@ -113,9 +115,11 @@ static struct option g_long_options[] = { {"githash", no_argument, 0, 'g'}, {"output", required_argument, 0, 'o'}, {"trust", required_argument, 0, 't'}, +#if defined(LEAN_MULTI_THREAD) {"server", no_argument, 0, 'S'}, - {"quiet", no_argument, 0, 'q'}, {"threads", required_argument, 0, 'j'}, +#endif + {"quiet", no_argument, 0, 'q'}, {"cache", required_argument, 0, 'c'}, {"deps", no_argument, 0, 'D'}, {"flycheck", no_argument, 0, 'F'}, @@ -126,10 +130,14 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "FDSqlupgvhj:012k:012s:012t:012o:c:i:"; +#define BASIC_OPT_STR "FDqlupgvhk:012t:012o:c:i:" + +#if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD) +static char const * g_opt_str = BASIC_OPT_STR "Sj:012s:012"; +#elif !defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD) +static char const * g_opt_str = BASIC_OPT_STR "Sj:012"; #else -static char const * g_opt_str = "FDSqlupgvhj:012k:012t:012o:c:i:"; +static char const * g_opt_str = BASIC_OPT_STR; #endif class simple_pos_info_provider : public pos_info_provider { @@ -223,6 +231,11 @@ int main(int argc, char ** argv) { } } + #if !defined(LEAN_MULTI_THREAD) + lean_assert(!server); + lean_assert(num_threads == 1); + #endif + environment env = mk_environment(trust_lvl); io_state ios(lean::mk_pretty_formatter_factory()); if (quiet)