From a339a53f5065fd5412e7dc4ebeb38dc394d47499 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jan 2014 15:31:58 -0800 Subject: [PATCH] feat(util/options): 'verbose' as a system option, add -q (quiet) option Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 2 +- src/frontends/lean/parser_imp.cpp | 9 +-------- src/shell/lean.cpp | 12 +++++++++++- src/util/sexpr/options.cpp | 8 ++++++++ src/util/sexpr/options.h | 1 + tests/lean/test.sh | 2 +- tests/lean/tst3.lean | 2 +- tests/lua/test.sh | 2 +- 8 files changed, 25 insertions(+), 13 deletions(-) diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index a8a486f47..29393fc3c 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -27,7 +27,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS) get_filename_component(BASENAME ${FILE} NAME_WE) set(FNAME "${BASENAME}.olean") add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} - COMMAND ${SHELL_DIR}/lean ${ARG} -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} + COMMAND ${SHELL_DIR}/lean ${ARG} -q -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${SHELL_DIR}/${FNAME} COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${CMAKE_CURRENT_SOURCE_DIR}/obj/${FNAME} DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${FILE} ${SHELL_DIR}/lean ${EXTRA_DEPS}) diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp index 63b0b6363..ebfa53dd4 100644 --- a/src/frontends/lean/parser_imp.cpp +++ b/src/frontends/lean/parser_imp.cpp @@ -16,20 +16,13 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true #endif -#ifndef LEAN_DEFAULT_PARSER_VERBOSE -#define LEAN_DEFAULT_PARSER_VERBOSE true -#endif - namespace lean { // ========================================== // Parser configuration options -static name g_parser_verbose {"lean", "parser", "verbose"}; static name g_parser_show_errors {"lean", "parser", "show_errors"}; -RegisterBoolOption(g_parser_verbose, LEAN_DEFAULT_PARSER_VERBOSE, "(lean parser) disable/enable parser verbose messages"); RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel"); -bool get_parser_verbose(options const & opts) { return opts.get_bool(g_parser_verbose, LEAN_DEFAULT_PARSER_VERBOSE); } bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); } // ========================================== @@ -108,7 +101,7 @@ double parser_imp::parse_double() { } void parser_imp::updt_options() { - m_verbose = get_parser_verbose(m_io_state.get_options()); + m_verbose = get_verbose(m_io_state.get_options()); m_show_errors = get_parser_show_errors(m_io_state.get_options()); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 1f96f9b25..6c6045b28 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -67,6 +67,7 @@ static void display_help(std::ostream & out) { std::cout << " it is useful for interrupting non-terminating user scripts,\n"; std::cout << " 0 means 'do not check'.\n"; std::cout << " --trust -t trust imported modules\n"; + std::cout << " --quiet -q do not print verbose messages\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -98,6 +99,7 @@ static struct option g_long_options[] = { {"githash", no_argument, 0, 'g'}, {"output", required_argument, 0, 'o'}, {"trust", no_argument, 0, 't'}, + {"quiet", no_argument, 0, 'q'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -111,10 +113,11 @@ int main(int argc, char ** argv) { bool no_kernel = false; bool export_objects = false; bool trust_imported = false; + bool quiet = false; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { - int c = getopt_long(argc, argv, "tnlupgvhc:012s:012o:", g_long_options, NULL); + int c = getopt_long(argc, argv, "qtnlupgvhc:012s:012o:", g_long_options, NULL); if (c == -1) break; // end of command line switch (c) { @@ -155,6 +158,9 @@ int main(int argc, char ** argv) { case 't': trust_imported = true; break; + case 'q': + quiet = true; + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -173,6 +179,8 @@ int main(int argc, char ** argv) { environment env; env->set_trusted_imported(trust_imported); io_state ios = init_frontend(env, no_kernel); + if (quiet) + ios.set_option("verbose", false); script_state S; shell sh(env, &S); int status = sh() ? 0 : 1; @@ -189,6 +197,8 @@ int main(int argc, char ** argv) { environment env; env->set_trusted_imported(trust_imported); io_state ios = init_frontend(env, no_kernel); + if (quiet) + ios.set_option("verbose", false); script_state S; bool ok = true; for (int i = optind; i < argc; i++) { diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index 5ae907210..9acac9f21 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -11,7 +11,15 @@ Author: Leonardo de Moura #include "util/sexpr/option_declarations.h" #include "util/sexpr/sexpr_fn.h" +#ifndef LEAN_DEFAULT_VERBOSE +#define LEAN_DEFAULT_VERBOSE true +#endif + namespace lean { +static name g_verbose("verbose"); +RegisterBoolOption(g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages"); +bool get_verbose(options const & opts) { return opts.get_bool(g_verbose, LEAN_DEFAULT_VERBOSE); } + std::ostream & operator<<(std::ostream & out, option_kind k) { switch (k) { case BoolOption: out << "Bool"; break; diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index 802706da8..285ede42a 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -70,6 +70,7 @@ public: friend bool operator==(options const & a, options const & b) { return a.m_value == b.m_value; } }; +bool get_verbose(options const & opts); inline options read_options(deserializer & d) { return options(read_sexpr(d)); } inline deserializer & operator>>(deserializer & d, options & o) { o = read_options(d); return d; } diff --git a/tests/lean/test.sh b/tests/lean/test.sh index 39b564e0a..d6c399da3 100755 --- a/tests/lean/test.sh +++ b/tests/lean/test.sh @@ -13,7 +13,7 @@ fi NUM_ERRORS=0 for f in `ls *.lean`; do echo "-- testing $f" - $LEAN config.lean $f &> $f.produced.out + $LEAN -t config.lean $f &> $f.produced.out if test -f $f.expected.out; then if diff -I "executing external script" $f.produced.out $f.expected.out; then echo "-- checked" diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index c60b7acc2..8b925381b 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,5 +1,5 @@ import if_then_else -set_option lean::parser::verbose false. +set_option verbose false. notation 10 if _ then _ : implies. print environment 1. print if true then false. diff --git a/tests/lua/test.sh b/tests/lua/test.sh index 625a8f616..dc77079bd 100755 --- a/tests/lua/test.sh +++ b/tests/lua/test.sh @@ -8,7 +8,7 @@ LEAN=$1 NUM_ERRORS=0 for f in `ls *.lua`; do echo "-- testing $f" - if $LEAN extra.lua $f > $f.produced.out; then + if $LEAN -t extra.lua $f > $f.produced.out; then echo "-- worked" else echo "ERROR executing $f, produced output is at $f.produced.out"