feat(kernel,library/module): only module reader can add declarations without type-checking them

src/kernel/environment.cpp

@@ -102,7 +102,7 @@ declaration environment::get(name const & n) const {
 }
 
 environment environment::add(declaration const & d) const {
-    if (trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL)
+    if (trust_lvl() == 0)
         throw_kernel_exception(*this, "environment trust level does not allow users to add declarations that were not type checked");
     name const & n = d.get_name();
     if (find(n))

src/kernel/environment.h

@@ -115,6 +115,14 @@ class environment {
 
     environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext);
 
+    friend class shared_environment;
+    /**
+       \brief Adds a declaration that was not type checked.
+
+       \remark This method throws an excetion if trust_lvl() == 0
+       It is mainly when importing pre-compiled .olean files, and trust_lvl() > 0.
+    */
+    environment add(declaration const & d) const;
 public:
     environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true);
     environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
@@ -169,16 +177,6 @@ public:
     */
     environment add(certified_declaration const & d) const;
 
-    /**
-       \brief Adds a declaration that was not type checked. This method throws an excetion if
-       trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL.
-       It is mainly when importing pre-compiled .olean files, and trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL.
-
-       \remark If trust_lvl() == 0, then this method will always throw an exception. No matter what is
-       the value of LEAN_BELIEVER_TRUST_LEVEL used to compile Lean.
-    */
-    environment add(declaration const & d) const;
-
     /**
        \brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
        This method throws an exception if:

src/library/kernel_bindings.cpp

@@ -1022,10 +1022,7 @@ static int environment_is_universe(lua_State * L) { return push_boolean(L, to_en
 static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
 static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
 static int environment_add(lua_State * L) {
-    if (is_declaration(L, 2))
+    return push_environment(L, module::add(to_environment(L, 1), to_certified_declaration(L, 2)));
-        return push_environment(L, module::add(to_environment(L, 1), to_declaration(L, 2)));
-    else
-        return push_environment(L, module::add(to_environment(L, 1), to_certified_declaration(L, 2)));
 }
 static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_declaration(L, 2))); }
 static int mk_bare_environment(lua_State * L) {

src/library/module.cpp

@@ -225,13 +225,6 @@ environment add(environment const & env, certified_declaration const & d) {
     return export_decl(update_module_defs(new_env, _d), _d);
 }
 
-environment add(environment const & env, declaration const & d) {
-    environment new_env = env.add(d);
-    if (!check_computable(new_env, d.get_name()))
-        new_env = mark_noncomputable(new_env, d.get_name());
-    return export_decl(update_module_defs(new_env, d), d);
-}
-
 bool is_definition(environment const & env, name const & n) {
     module_ext const & ext = get_extension(env);
     return ext.m_module_defs.contains(n);
@@ -330,7 +323,7 @@ struct import_modules_fn {
         if (m_num_threads > 1)
             m_num_threads = 1;
 #endif
-        if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
+        if (env.trust_lvl() > 0) {
             // it doesn't payoff to use multiple threads if we will not type check anything
             m_num_threads = 1;
         }
@@ -424,7 +417,7 @@ struct import_modules_fn {
         decl = unfold_untrusted_macros(env, decl);
         if (decl.get_name() == get_sorry_name() && has_sorry(env))
             return;
-        if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
+        if (env.trust_lvl() > 0) {
             if (!m_keep_proofs && decl.is_theorem())
                 m_senv.add(theorem2axiom(decl));
             else

src/library/module.h

@@ -99,10 +99,6 @@ environment add_universe(environment const & env, name const & l);
 
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
-/** \brief Add the given declaration to the environment, and mark it to be exported.
-    This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
-*/
-environment add(environment const & env, declaration const & d);
 
 /** \brief Return true iff \c n is a definition added to the current module using #module::add */
 bool is_definition(environment const & env, name const & n);

src/library/shared_environment.h

@@ -12,8 +12,17 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Auxiliary object used when multiple threads are trying to populate the same environment. */
 class shared_environment {
+    friend class import_modules_fn;
     environment          m_env;
     mutable mutex        m_mutex;
+    /**
+        \brief Add declaration that was not type checked.
+        The method throws an exception if trust_level() == 0
+        It blocks this object for a small amount of time.
+
+        Only module
+    */
+    void add(declaration const & d);
 public:
     shared_environment();
     shared_environment(environment const & env);
@@ -26,12 +35,6 @@ public:
         It blocks this object for a small amount of time.
     */
     void add(certified_declaration const & d);
-    /**
-        \brief Add declaration that was not type checked.
-        The method throws an exception if trust_level() <= LEAN_BELIEVER_TRUST_LEVEL
-        It blocks this object for a small amount of time.
-    */
-    void add(declaration const & d);
     /**
         \brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
         This is a constant time operation.

tests/lua/env9.lua

@@ -4,8 +4,3 @@ local env = bare_environment()
 assert(not pcall(function() env:add(mk_constant_assumption("A", Prop)) end))
 -- The function check produces a "certified declaration".
 env:add(check(env, mk_constant_assumption("A", Prop)))
-
-local env = bare_environment({trust_level = 10000000})
--- Now, env has trust_level > LEAN_BELIEVER_TRUST_LEVEL, then we can
--- add declarations without type checking them.
-env:add(mk_constant_assumption("A", Prop))