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

feat(shell): remove '--server' command line option when compiling with -DMULTI_THREAD=OFF

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 12:42:19 -07:00
parent 0bc9cf407e
commit b5b68613b1
3 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/server.cpp
View file

@ -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() {

2
src/shell/CMakeLists.txt
View file

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

21
src/shell/lean.cpp
View file

@ -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)