diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index c8184eeb3..fa4e5adc2 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); } namespace lean { +static void open_patch(lua_State * L); static void open_state(lua_State * L); static void open_thread(lua_State * L); environment & to_environment(lua_State * L, int idx); @@ -85,6 +86,7 @@ struct leanlua_state::imp { if (m_state == nullptr) throw exception("fail to create Lua interpreter"); luaL_openlibs(m_state); + open_patch(m_state); open_name(m_state); open_mpz(m_state); open_mpq(m_state); @@ -140,6 +142,39 @@ void leanlua_state::dostring(char const * str, environment & env) { m_ptr->dostring(str, env); } +static std::mutex g_print_mutex; + +/** \brief Thread safe version of print function */ +static int print(lua_State * L) { + // TODO(Leo): use output channels (if available) instead of std::cout + int n = lua_gettop(L); + int i; + lua_getglobal(L, "tostring"); + std::lock_guard lock(g_print_mutex); + for (i = 1; i <= n; i++) { + char const * s; + size_t l; + lua_pushvalue(L, -1); + lua_pushvalue(L, i); + lua_call(L, 1, 1); + s = lua_tolstring(L, -1, &l); + if (s == NULL) + return luaL_error(L, "'to_string' must return a string to 'print'"); + if (i > 1) { + std::cout << "\t"; + } + std::cout << s; + lua_pop(L, 1); + } + std::cout << std::endl; + return 0; +} + +/** \brief Redefine some functions from the Lua library */ +static void open_patch(lua_State * L) { + set_global_function(L, "print"); +} + constexpr char const * state_mt = "state.mt"; bool is_state(lua_State * L, int idx) { diff --git a/tests/lua/threads/th3.lua b/tests/lua/threads/th3.lua new file mode 100644 index 000000000..179277740 --- /dev/null +++ b/tests/lua/threads/th3.lua @@ -0,0 +1,12 @@ +S1 = State() +S2 = State() +code = [[ + id = ... + for i = 1, 10000 do + print("id: " .. id .. ", val: " .. i) + end +]] +T1 = thread(S1, code, 1) +T2 = thread(S2, code, 2) +T1:wait() +T2:wait()