diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index 107494399..d912b24b8 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -125,8 +125,19 @@ static int parse_lean_cmds(lua_State * L) { } } +static bool g_default_trust_imported = false; + +void set_default_trust_imported_for_lua(bool f) { + g_default_trust_imported = f; +} + static int mk_environment(lua_State * L) { + int nargs = lua_gettop(L); environment env; + if (nargs == 0) + env->set_trusted_imported(g_default_trust_imported); + else + env->set_trusted_imported(lua_toboolean(L, 1)); io_state ios = init_frontend(env); return push_environment(L, env); } diff --git a/src/frontends/lean/register_module.h b/src/frontends/lean/register_module.h index be5436e1f..c1e6bea4a 100644 --- a/src/frontends/lean/register_module.h +++ b/src/frontends/lean/register_module.h @@ -9,4 +9,5 @@ Author: Leonardo de Moura namespace lean { void open_frontend_lean(lua_State * L); void register_frontend_lean_module(); +void set_default_trust_imported_for_lua(bool f); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 6c6045b28..28b8263a7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "frontends/lean/parser.h" #include "frontends/lean/shell.h" #include "frontends/lean/frontend.h" +#include "frontends/lean/register_module.h" #include "frontends/lua/register_modules.h" #include "version.h" #include "githash.h" // NOLINT @@ -157,6 +158,7 @@ int main(int argc, char ** argv) { break; case 't': trust_imported = true; + lean::set_default_trust_imported_for_lua(true); break; case 'q': quiet = true;