feat(shell): provide the default environment when parsing Lua files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
7f818ecd92
commit
35bacf95fc
3 changed files with 8 additions and 2 deletions
|
@ -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());
|
set_global_options(L, s.get_options());
|
||||||
} else {
|
} else {
|
||||||
parse_lean_cmds_core(L, env, *io);
|
parse_lean_cmds_core(L, env, *io);
|
||||||
|
set_global_options(L, io->get_options());
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -227,7 +227,13 @@ int main(int argc, char ** argv) {
|
||||||
}
|
}
|
||||||
} else if (k == input_kind::Lua) {
|
} else if (k == input_kind::Lua) {
|
||||||
try {
|
try {
|
||||||
|
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]);
|
S.dofile(argv[i]);
|
||||||
|
});
|
||||||
|
});
|
||||||
} catch (lean::exception & ex) {
|
} catch (lean::exception & ex) {
|
||||||
std::cerr << ex.what() << std::endl;
|
std::cerr << ex.what() << std::endl;
|
||||||
ok = false;
|
ok = false;
|
||||||
|
|
|
@ -1,4 +1,3 @@
|
||||||
assert(not pcall(function() get_environment() end))
|
|
||||||
local env = environment()
|
local env = environment()
|
||||||
env:import("Int")
|
env:import("Int")
|
||||||
env:add_uvar_cnstr("M", level(level(), 1))
|
env:add_uvar_cnstr("M", level(level(), 1))
|
||||||
|
|
Loading…
Add table
Reference in a new issue