diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp
index d912b24b8..35b3d0aaf 100644
--- a/src/frontends/lean/register_module.cpp
+++ b/src/frontends/lean/register_module.cpp
@@ -94,6 +94,7 @@ static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & en
         set_global_options(L, s.get_options());
     } else {
         parse_lean_cmds_core(L, env, *io);
+        set_global_options(L, io->get_options());
     }
 }
 
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 28b8263a7..d416f1656 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -227,7 +227,13 @@ int main(int argc, char ** argv) {
                     }
                 } else if (k == input_kind::Lua) {
                     try {
-                        S.dofile(argv[i]);
+                        S.apply([&](lua_State * L) {
+                                lean::set_io_state    set1(L, ios);
+                                lean::set_environment set2(L, env);
+                                S.exec_unprotected([&]() {
+                                        S.dofile(argv[i]);
+                                    });
+                            });
                     } catch (lean::exception & ex) {
                         std::cerr << ex.what() << std::endl;
                         ok = false;
diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua
index 7ae5fe8ce..ba12b6823 100644
--- a/tests/lua/env4.lua
+++ b/tests/lua/env4.lua
@@ -1,4 +1,3 @@
-assert(not pcall(function() get_environment() end))
 local env = environment()
 env:import("Int")
 env:add_uvar_cnstr("M", level(level(), 1))