From 12674114a4dacbf7a68922d91715074cdd6b7fc1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Jan 2015 16:19:46 -0800 Subject: [PATCH] feat(shell): set default behavior to "trusted" closes #402 --- bin/linja | 6 +++--- src/CMakeLists.txt | 4 ++-- src/frontends/lean/builtin_cmds.cpp | 3 +++ src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/shell/CMakeLists.txt | 25 +++++++++++++++++-------- src/shell/lean.cpp | 14 +++++--------- tests/lean/trust0/t1.lean | 2 ++ tests/lean/trust0/test_single.sh | 16 ++++++++++++++++ 9 files changed, 53 insertions(+), 22 deletions(-) create mode 100644 tests/lean/trust0/t1.lean create mode 100755 tests/lean/trust0/test_single.sh diff --git a/bin/linja b/bin/linja index b087827cf..273c700bd 100755 --- a/bin/linja +++ b/bin/linja @@ -342,8 +342,8 @@ def get_lean_options(args): args.lean_options.append("--discard") if args.memory: args.lean_options += ["-M", args.memory] - if args.Trust: - args.lean_options.append("--Trust") + if args.trust: + args.lean_options += ["-t", args.trust] if args.to_axiom: args.lean_options.append("--to_axiom") if args.cache: @@ -365,7 +365,7 @@ def parse_arg(argv): parser.add_argument('--keep-going', '-k', action='store', default=None, const=1, nargs='?', help="keep going until N jobs fail [default=1]") parser.add_argument('--discard', '-r', action='store_true', default=False, help="discard the proof of imported theorems after checking") parser.add_argument('--to_axiom', '-X', action='store_true', default=False, help="discard proofs of all theorems after checking them, i.e., theorems become axioms after checking") - parser.add_argument('--Trust', '-T', action='store_true', default=False, help="short-cut for maximum trust level (e.g., Lean will not type check imported files)") + parser.add_argument('--trust', '-t', action='store_true', default=False, help="trust level [default: max]") parser.add_argument('targets', nargs='*') args = parser.parse_args(argv) check_requirements() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 37a1987e1..aa020bf26 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -372,13 +372,13 @@ if("${CROSS_COMPILE}" MATCHES "ON" OR "${CMAKE_C_COMPILER}" MATCHES "emcc") else() add_custom_target( standard_lib ALL - COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja --Trust all tags + COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja all tags DEPENDS ${CMAKE_BINARY_DIR}/shell/lean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library ) add_custom_target( hott_lib ALL - COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja --Trust all tags + COMMAND ${PYTHON_EXECUTABLE} ${LEAN_SOURCE_DIR}/../bin/linja all tags DEPENDS ${CMAKE_BINARY_DIR}/shell/lean WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../hott ) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 61b7761b1..342c15cc4 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -175,6 +175,9 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token_or_id(get_options_tk())) { p.next(); p.regular_stream() << p.ios().get_options() << endl; + } else if (p.curr_is_token_or_id(get_trust_tk())) { + p.next(); + p.regular_stream() << "trust level: " << p.env().trust_lvl() << endl; } else if (p.curr_is_token_or_id(get_definition_tk())) { p.next(); auto pos = p.pos(); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 19c907e8c..48b824c9c 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -101,6 +101,7 @@ static name * g_persistent = nullptr; static name * g_local = nullptr; static name * g_root = nullptr; static name * g_fields = nullptr; +static name * g_trust = nullptr; void initialize_tokens() { g_period = new name("."); @@ -197,6 +198,7 @@ void initialize_tokens() { g_local = new name("[local]"); g_root = new name("_root_"); g_fields = new name("fields"); + g_trust = new name("trust"); } void finalize_tokens() { @@ -204,6 +206,7 @@ void finalize_tokens() { delete g_local; delete g_root; delete g_fields; + delete g_trust; delete g_prev; delete g_scoped; delete g_foldr; @@ -390,4 +393,5 @@ name const & get_persistent_tk() { return *g_persistent; } name const & get_local_tk() { return *g_local; } name const & get_root_tk() { return *g_root; } name const & get_fields_tk() { return *g_fields; } +name const & get_trust_tk() { return *g_trust; } } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index d2000e60a..ba5efe968 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -103,4 +103,5 @@ name const & get_persistent_tk(); name const & get_local_tk(); name const & get_root_tk(); name const & get_fields_tk(); +name const & get_trust_tk(); } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index a76018e04..f2fdcd574 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -38,7 +38,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN RUN TESTS @@ -47,7 +47,16 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) +ENDFOREACH(T) + +# LEAN TESTS using --trust=0 +file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean") +FOREACH(T ${LEANT0TESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leant0test_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 0" ${T_NAME}) ENDFOREACH(T) # LEAN RUN HoTT TESTS @@ -56,7 +65,7 @@ FOREACH(T ${LEANRUNHTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanhotttest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/hott" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) if("${MULTI_THREAD}" MATCHES "ON") @@ -66,7 +75,7 @@ FOREACH(T ${LEANITTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanittest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) endif() @@ -76,7 +85,7 @@ FOREACH(T ${LEANSLOWTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanslowtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive") ENDFOREACH(T) @@ -86,7 +95,7 @@ FOREACH(T ${LEANLUATESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanluatest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) # LEAN LUA SLOW TESTS @@ -95,7 +104,7 @@ FOREACH(T ${LEANLUASLOWTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanluaslowtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/slow" - COMMAND bash "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME}) + COMMAND bash "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) set_tests_properties("leanluaslowtest_${T_NAME}" PROPERTIES LABELS "expensive") ENDFOREACH(T) @@ -114,7 +123,7 @@ FOREACH(T ${LEANLUADOCS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanluadoc_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua" - COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T}) + COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) ENDFOREACH(T) # # Create the script lean.sh diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 7617a05a4..cb2f04a3f 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -98,8 +98,8 @@ static void display_help(std::ostream & out) { std::cout << " --luahook=num -k how often the Lua interpreter checks the interrupted flag,\n"; std::cout << " it is useful for interrupting non-terminating user scripts,\n"; std::cout << " 0 means 'do not check'.\n"; - std::cout << " --trust=num -t trust level (default: 0) \n"; - std::cout << " --Trust -T short-cut for --trust=" << LEAN_BELIEVER_TRUST_LEVEL+1 << "\n"; + std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro, " + << " and type check all imported modules\n"; std::cout << " --discard -r discard the proof of imported theorems after checking\n"; std::cout << " --to_axiom -X discard proofs of all theorems after checking them, i.e.,\n"; std::cout << " theorems become axioms after checking\n"; @@ -150,7 +150,6 @@ static struct option g_long_options[] = { {"cpp", required_argument, 0, 'C'}, {"memory", required_argument, 0, 'M'}, {"trust", required_argument, 0, 't'}, - {"Trust", no_argument, 0, 'T'}, {"discard", no_argument, 0, 'r'}, {"to_axiom", no_argument, 0, 'X'}, #if defined(LEAN_MULTI_THREAD) @@ -168,7 +167,7 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#define OPT_STR "HRXTFC:dD:qrlupgvhk:012t:012o:c:i:" +#define OPT_STR "HRXFC:dD:qrlupgvhk:012t:012o:c:i:" #if defined(LEAN_TRACK_MEMORY) #define OPT_STR2 OPT_STR "M:012" @@ -270,7 +269,7 @@ private: set_io_state set2; public: - emscripten_shell() : trust_lvl(10000), num_threads(1), opts("flycheck", true), + emscripten_shell() : trust_lvl(LEAN_BELIEVER_TRUST_LEVEL+1), num_threads(1), opts("flycheck", true), env(mk_environment(trust_lvl)), ios(opts, lean::mk_pretty_formatter_factory()), S(lean::get_thread_script_state()), set1(S, env), set2(S, ios) { } @@ -333,7 +332,7 @@ int main() { int main(int argc, char ** argv) { lean::initializer init; bool export_objects = false; - unsigned trust_lvl = 0; + unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1; bool server = false; bool only_deps = false; unsigned num_threads = 1; @@ -409,9 +408,6 @@ int main(int argc, char ** argv) { case 't': trust_lvl = atoi(optarg); break; - case 'T': - trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1; - break; case 'r': tmode = keep_theorem_mode::DiscardImported; break; diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean new file mode 100644 index 000000000..f99dc4ae7 --- /dev/null +++ b/tests/lean/trust0/t1.lean @@ -0,0 +1,2 @@ +import standard +print trust diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh new file mode 100755 index 000000000..1339f11d6 --- /dev/null +++ b/tests/lean/trust0/test_single.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +if [ $# -ne 2 ]; then + echo "Usage: test_single.sh [lean-executable-path] [file]" + exit 1 +fi +ulimit -s 8192 +LEAN=$1 +export LEAN_PATH=../../../library:. +f=$2 +echo "-- testing $f" +if $LEAN $f; then + echo "-- checked" +else + echo "failed $f" + exit 1 +fi