feat(shell): set default behavior to "trusted"

closes #402

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:
+    if args.trust:
-        args.lean_options.append("--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()

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
     )

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();

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; }
 }

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();
 }

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

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=num -t    trust level (default: max) 0 means do not trust any macro, "
-    std::cout << "  --Trust -T        short-cut for --trust=" << LEAN_BELIEVER_TRUST_LEVEL+1 << "\n";
+              << "                    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;

tests/lean/trust0/t1.lean

@@ -0,0 +1,2 @@
+import standard
+print trust

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