feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules

"Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip
type checking when importing these files.
TODO: add a check-sum.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/environment.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "util/realpath.h"
 #include "util/sstream.h"
 #include "util/lean_path.h"
+#include "util/flet.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
 #include "kernel/kernel_exception.h"
@@ -355,11 +356,13 @@ void environment_cell::check_no_cached_type(expr const & e) {
    v is not convertible to \c t.
 */
 void environment_cell::check_type(name const & n, expr const & t, expr const & v) {
+    if (m_type_check) {
         m_type_checker->check_type(t);
         expr v_t = m_type_checker->check(v);
         if (!m_type_checker->is_convertible(v_t, t))
             throw def_type_mismatch_exception(env(), n, t, v, v_t);
     }
+}
 
 /** \brief Throw exception if it is not a valid new definition */
 void environment_cell::check_new_definition(name const & n, expr const & t, expr const & v) {
@@ -407,7 +410,11 @@ void environment_cell::add_definition(name const & n, expr const & t, expr const
 void environment_cell::add_definition(name const & n, expr const & v, bool opaque) {
     check_no_cached_type(v);
     check_name(n);
-    expr v_t = m_type_checker->check(v);
+    expr v_t;
+    if (m_type_check)
+        v_t = m_type_checker->check(v);
+    else
+        v_t = m_type_checker->infer_type(v);
     unsigned w = get_max_weight(v) + 1;
     register_named_object(mk_definition(n, v_t, v, w));
     if (opaque)
@@ -434,6 +441,7 @@ void environment_cell::set_opaque(name const & n, bool opaque) {
 void environment_cell::add_axiom(name const & n, expr const & t) {
     check_no_cached_type(t);
     check_name(n);
+    if (m_type_check)
         m_type_checker->check_type(t);
     register_named_object(mk_axiom(n, t));
 }
@@ -442,6 +450,7 @@ void environment_cell::add_axiom(name const & n, expr const & t) {
 void environment_cell::add_var(name const & n, expr const & t) {
     check_no_cached_type(t);
     check_name(n);
+    if (m_type_check)
         m_type_checker->check_type(t);
     register_named_object(mk_var_decl(n, t));
 }
@@ -534,6 +543,10 @@ void environment_cell::import_builtin(char const * id, std::function<void()> fn)
     }
 }
 
+void environment_cell::set_trusted_imported(bool flag) {
+    m_trust_imported = flag;
+}
+
 static char const * g_olean_header   = "oleanfile";
 static char const * g_olean_end_file = "EndFile";
 void environment_cell::export_objects(std::string const & fname) {
@@ -598,6 +611,7 @@ bool environment_cell::load_core(std::string const & fname, io_state const & ios
 }
 
 bool environment_cell::import(std::string const & fname, io_state const & ios) {
+    flet<bool> set(m_type_check, !m_trust_imported);
     return load_core(realpath(find_file(fname, {".olean"}).c_str()), ios, optional<std::string>(fname));
 }
 
@@ -607,12 +621,16 @@ void environment_cell::load(std::string const & fname, io_state const & ios) {
 
 environment_cell::environment_cell():
     m_num_children(0) {
+    m_trust_imported = false;
+    m_type_check     = true;
     init_uvars();
 }
 
 environment_cell::environment_cell(std::shared_ptr<environment_cell> const & parent):
     m_num_children(0),
     m_parent(parent) {
+    m_trust_imported = false;
+    m_type_check     = true;
     parent->inc_children();
 }
 

src/kernel/environment.h

@@ -43,7 +43,8 @@ class environment_cell {
     object_dictionary                       m_object_dictionary;
     std::unique_ptr<type_checker>           m_type_checker;
     std::set<name>                          m_imported_modules;   // set of imported files and builtin modules
-
+    bool                                    m_trust_imported; // if true, then imported modules are not type checked.
+    bool                                    m_type_check;     // auxiliary flag used to implement m_trust_imported.
     std::vector<std::unique_ptr<environment_extension>> m_extensions;
     friend class environment_extension;
 
@@ -324,6 +325,12 @@ public:
 
     void load(std::string const & fname, io_state const & ios);
 
+    /**
+        \brief When trusted_imported flag is true, the environment will
+        not type check imported modules.
+    */
+    void set_trusted_imported(bool flag);
+
     /**
        \brief Execute function \c fn. Any object created by \c fn
        is not exported by the environment.

src/shell/lean.cpp

@@ -65,6 +65,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --luahook=num -c  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 -t        trust imported modules\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -95,6 +96,7 @@ static struct option g_long_options[] = {
     {"luahook",    required_argument, 0, 'c'},
     {"githash",    no_argument,       0, 'g'},
     {"output",     required_argument, 0, 'o'},
+    {"trust",      no_argument,       0, 't'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",     required_argument, 0, 's'},
 #endif
@@ -107,10 +109,11 @@ int main(int argc, char ** argv) {
         lean::register_modules();
         bool kernel_only    = false;
         bool export_objects = false;
+        bool trust_imported = false;
         std::string output;
         input_kind default_k = input_kind::Lean; // default
         while (true) {
-            int c = getopt_long(argc, argv, "klupgvhc:012s:012o:", g_long_options, NULL);
+            int c = getopt_long(argc, argv, "tklupgvhc:012s:012o:", g_long_options, NULL);
             if (c == -1)
                 break; // end of command line
             switch (c) {
@@ -148,6 +151,9 @@ int main(int argc, char ** argv) {
                 output = optarg;
                 export_objects = true;
                 break;
+            case 't':
+                trust_imported = true;
+                break;
             default:
                 std::cerr << "Unknown command line option\n";
                 display_help(std::cerr);
@@ -164,6 +170,7 @@ int main(int argc, char ** argv) {
                 std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl;
 #endif
                 environment env;
+                env->set_trusted_imported(trust_imported);
                 io_state ios;
                 init_frontend(env, ios, kernel_only);
                 script_state S;
@@ -179,6 +186,7 @@ int main(int argc, char ** argv) {
             }
         } else {
             environment env;
+            env->set_trusted_imported(trust_imported);
             io_state    ios;
             init_frontend(env, ios, kernel_only);
             script_state S;