From 771b099c0cb14381677799f7097744aaf7396c5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 16:38:29 -0800 Subject: [PATCH] fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser_cmds.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 28143a74c..d6ad01622 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -733,6 +733,7 @@ void parser_imp::parse_end() { throw parser_error("invalid 'end', not inside of a scope or namespace", m_last_cmd_pos); scope_kind k = m_scope_kinds.back(); m_scope_kinds.pop_back(); + m_script_state->apply([&](lua_State * L) { lua_gc(L, LUA_GCCOLLECT, LUA_TUSERDATA); }); switch (k) { case scope_kind::Scope: { if (!m_env->has_parent())