From 936eb764664849ba4ed56c46718bb1ef3854b91c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Oct 2016 11:48:02 -0700 Subject: [PATCH] feat(CMakeFiles): add -DSERVER=OFF cmake option Motivation: we can disable lean-server and the json dependency when compiling lean.js. --- src/CMakeLists.txt | 8 ++++++++ src/shell/json.cpp | 2 ++ src/shell/json.h | 3 ++- src/shell/lean.cpp | 16 +++++++++++++++- src/shell/server.cpp | 2 ++ 5 files changed, 29 insertions(+), 2 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 53dd53fac1..69734f9df5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -20,6 +20,9 @@ option(SPLIT_STACK "SPLIT_STACK" OFF) option(READLINE "READLINE" OFF) option(TCMALLOC "TCMALLOC" ON) option(JEMALLOC "JEMALLOC" OFF) +# When ON we enable the lean-server support used for IDEs +option(SERVER "SERVER" ON) + # IGNORE_SORRY is a tempory option (hack). It allows us to build # a version of Lean that does not report when 'sorry' is used. # This is useful for suppressing warning messages in the nightly builds. @@ -75,6 +78,11 @@ if("${CYGWIN}" EQUAL "1") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_CYGWIN") endif() +if("${SERVER}" MATCHES "ON") + message(STATUS "Compile server enabled") + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_SERVER") +endif() + if(MINGW AND CMAKE_COMPILER_IS_GNUCXX) # See https://github.com/leanprover/lean/issues/930#issuecomment-172555475 message(STATUS "Set _GLIBCXX_USE_CXX11_ABI = 0 for a system using MSYS2 + g++") diff --git a/src/shell/json.cpp b/src/shell/json.cpp index 135629ced2..78e04fdc28 100644 --- a/src/shell/json.cpp +++ b/src/shell/json.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ +#if defined(SERVER) #include "shell/json.h" namespace lean { @@ -33,3 +34,4 @@ void json_message_stream::report(message const & msg) { } } +#endif diff --git a/src/shell/json.h b/src/shell/json.h index 92f91b2701..99ea6c11de 100644 --- a/src/shell/json.h +++ b/src/shell/json.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ #pragma once - +#if defined(SERVER) #include "library/messages.h" #include "util/json.hpp" @@ -26,3 +26,4 @@ public: }; } +#endif diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 8ec933e9f2..6a9bc9fb85 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -40,7 +40,9 @@ Author: Leonardo de Moura #include "shell/emscripten.h" #include "shell/simple_pos_info_provider.h" #include "shell/json.h" +#if defined(LEAN_SERVER) #include "shell/server.h" +#endif #include "version.h" #include "githash.h" // NOLINT @@ -96,8 +98,10 @@ static void display_help(std::ostream & out) { 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"; +#if defined(LEAN_SERVER) std::cout << " --json print JSON-formatted structured error messages\n"; std::cout << " --server start lean in server mode\n"; +#endif std::cout << " --cache=file -c load/save cached definitions from/to the given file\n"; std::cout << " --profile display elaboration/type checking time for each definition/theorem\n"; #if defined(LEAN_USE_BOOST) @@ -136,8 +140,10 @@ static struct option g_long_options[] = { #endif {"quiet", no_argument, 0, 'q'}, {"deps", no_argument, 0, 'd'}, +#if defined(LEAN_SERVER) {"json", no_argument, 0, 'J'}, {"server", no_argument, 0, 'S'}, +#endif #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -220,8 +226,10 @@ int main(int argc, char ** argv) { bool smt2 = false; bool only_deps = false; unsigned num_threads = 1; +#if defined(LEAN_SERVER) bool json_output = false; bool server = false; +#endif options opts; std::string output; std::string cache_name; @@ -284,6 +292,7 @@ int main(int argc, char ** argv) { return 1; } break; +#if defined(LEAN_SERVER) case 'J': opts = opts.update(lean::name{"trace", "as_messages"}, true); json_output = true; @@ -292,6 +301,7 @@ int main(int argc, char ** argv) { opts = opts.update(lean::name{"trace", "as_messages"}, true); server = true; break; +#endif case 'P': opts = opts.update("profile", true); break; @@ -313,7 +323,7 @@ int main(int argc, char ** argv) { case 'E': export_txt = std::string(optarg); break; -#ifdef LEAN_DEBUG +#if defined(LEAN_DEBUG) case 'B': lean::enable_debug(optarg); break; @@ -348,11 +358,13 @@ int main(int argc, char ** argv) { environment env = mk_environment(trust_lvl); io_state ios(opts, lean::mk_pretty_formatter_factory()); +#if defined(LEAN_SERVER) if (json_output) { ios.set_message_channel(std::make_shared(std::cout)); // Redirect uncaptured non-json messages to stdout ios.set_regular_channel(ios.get_diagnostic_channel_ptr()); } +#endif if (smt2) { // Note: the smt2 flag may override other flags @@ -372,6 +384,7 @@ int main(int argc, char ** argv) { return ok ? 0 : 1; } +#if defined(LEAN_SERVER) if (server) { /* Disable assertion violation dialog: (C)ontinue, (A)bort, (S)top, Invoke (G)DB */ @@ -379,6 +392,7 @@ int main(int argc, char ** argv) { lean::server(num_threads, env, ios).run(); return 0; } +#endif try { bool ok = true; diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 10287bacad..3950539134 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ +#if defined(LEAN_SERVER) #include #include "frontends/lean/parser.h" #include "library/module.h" @@ -147,3 +148,4 @@ json server::handle_check(json const &) { } } +#endif