From 6c934229f7c2f35cc6e53e405553a6db1e638786 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Aug 2015 18:37:17 -0700 Subject: [PATCH] feat(kernel,library/module): only module reader can add declarations without type-checking them --- src/kernel/environment.cpp | 2 +- src/kernel/environment.h | 18 ++++++++---------- src/library/kernel_bindings.cpp | 5 +---- src/library/module.cpp | 11 ++--------- src/library/module.h | 4 ---- src/library/shared_environment.h | 15 +++++++++------ tests/lua/env9.lua | 5 ----- 7 files changed, 21 insertions(+), 39 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 6af9082ff..4cb316b1d 100644 --- a/src/kernel/environment.cpp +++ b/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)) diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 032e6a686..a4d0899aa 100644 --- a/src/kernel/environment.h +++ b/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 t.get_declaration().get_name() with the theorem t.get_declaration(). This method throws an exception if: diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 69b533667..f5b1603ee 100644 --- a/src/library/kernel_bindings.cpp +++ b/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_declaration(L, 2))); - else - 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_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) { diff --git a/src/library/module.cpp b/src/library/module.cpp index 4ddba048e..ae0762da5 100644 --- a/src/library/module.cpp +++ b/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 diff --git a/src/library/module.h b/src/library/module.h index ad625c471..545728070 100644 --- a/src/library/module.h +++ b/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); diff --git a/src/library/shared_environment.h b/src/library/shared_environment.h index eb68e06ff..0a781de3a 100644 --- a/src/library/shared_environment.h +++ b/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 t.get_declaration().get_name() with the theorem t.get_declaration(). This is a constant time operation. diff --git a/tests/lua/env9.lua b/tests/lua/env9.lua index fd37b8280..7bcababb0 100644 --- a/tests/lua/env9.lua +++ b/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))