From a10aa0880fd7296edda11dfddffc2d29d85459ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Nov 2013 08:26:04 -0800 Subject: [PATCH] fix(build): add CheckLuaObjlen.cc test, not every Lua version has the function lua_objlen Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 3 +++ src/bindings/lua/expr.cpp | 6 +++--- src/bindings/lua/util.cpp | 8 ++++++++ src/bindings/lua/util.h | 1 + src/cmake/Modules/CheckLuaObjlen.cc | 20 ++++++++++++++++++++ src/cmake/Modules/FindLua.cmake | 14 ++++++++++++++ 6 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 src/cmake/Modules/CheckLuaObjlen.cc diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6895ccc650..c3eb8a8e66 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -129,6 +129,9 @@ if ("${LUA_FOUND}" MATCHES "TRUE") if ("${HAS_LUA_NEWSTATE}$" MATCHES "TRUE") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_NEWSTATE") endif() + if ("${HAS_LUA_OBJLEN}$" MATCHES "TRUE") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_OBJLEN") + endif() else() message(WARNING "FAILED to find Lua script language, it will not be available") endif() diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index f05da834cd..87f80a3cf5 100644 --- a/src/bindings/lua/expr.cpp +++ b/src/bindings/lua/expr.cpp @@ -112,7 +112,7 @@ static std::pair get_expr_pair_from_table(lua_State * L, int t, int lua_pushvalue(L, t); // push table on the top lua_pushinteger(L, i); lua_gettable(L, -2); // now table {ai, bi} is on the top - if (!lua_istable(L, -1) || lua_objlen(L, -1) != 2) + if (!lua_istable(L, -1) || objlen(L, -1) != 2) luaL_error(L, "arg #1 must be of the form '{{expr, expr}, ...}'"); expr ai = get_expr_from_table(L, -1, 1); expr bi = get_expr_from_table(L, -1, 2); @@ -127,7 +127,7 @@ static int expr_fun(lua_State * L) { if (nargs == 2) { if (!lua_istable(L, 1)) luaL_error(L, "Lean fun expects arg #1 to be of the form '{{expr, expr}, ...}'"); - int len = lua_objlen(L, 1); + int len = objlen(L, 1); if (len == 0) luaL_error(L, "Lean fun expects arg #1 to be non-empty table"); expr r = to_expr(L, 2); @@ -157,7 +157,7 @@ static int expr_pi(lua_State * L) { if (nargs == 2) { if (!lua_istable(L, 1)) luaL_error(L, "Lean Pi expects arg #1 to be of the form '{{expr, expr}, ...}'"); - int len = lua_objlen(L, 1); + int len = objlen(L, 1); if (len == 0) luaL_error(L, "Lean Pi expects arg #1 to be non-empty table"); expr r = to_expr(L, 2); diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp index ebbc448567..1af8b657a7 100644 --- a/src/bindings/lua/util.cpp +++ b/src/bindings/lua/util.cpp @@ -44,6 +44,14 @@ bool testudata(lua_State * L, int ud, char const * tname) { return nullptr; // value is not a userdata with a metatable } +size_t objlen(lua_State * L, int idx) { + #ifdef LEAN_USE_LUA_OBJLEN + return lua_objlen(L, idx); + #else + return lua_rawlen(L, idx); + #endif +} + int safe_function_wrapper(lua_State * L, lua_CFunction f){ static thread_local std::string _error_msg; char const * error_msg; diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h index 044ebae485..e4fdbf0814 100644 --- a/src/bindings/lua/util.h +++ b/src/bindings/lua/util.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura namespace lean { void setfuncs(lua_State * L, luaL_Reg const * l, int nup); bool testudata(lua_State * L, int idx, char const * mt); +size_t objlen(lua_State * L, int idx); /** \brief Wrapper for invoking function f, and catching Lean exceptions. */ diff --git a/src/cmake/Modules/CheckLuaObjlen.cc b/src/cmake/Modules/CheckLuaObjlen.cc new file mode 100644 index 0000000000..abb4bd69d2 --- /dev/null +++ b/src/cmake/Modules/CheckLuaObjlen.cc @@ -0,0 +1,20 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include + +// Little program for checking whether lua_objlen is available +int main() { + lua_State * L; + L = luaL_newstate(); + lua_newtable(L); + if (lua_objlen(L, -1) == 0) + return 0; + else + return 1; +} diff --git a/src/cmake/Modules/FindLua.cmake b/src/cmake/Modules/FindLua.cmake index 444ab8b791..681f9fb729 100644 --- a/src/cmake/Modules/FindLua.cmake +++ b/src/cmake/Modules/FindLua.cmake @@ -130,4 +130,18 @@ if (LUA_FOUND) else() message(STATUS "lua_newstate is not supported by your Lua engine, Lean will not be able to track memory consumed by the Lua engine") endif() + + try_run(LUA_CHECK2 LUA_CHECK_BUILD2 + ${LEAN_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp + ${LEAN_SOURCE_DIR}/cmake/Modules/CheckLuaObjlen.cc + CMAKE_FLAGS -DINCLUDE_DIRECTORIES=${LUA_INCLUDE_DIR} + -DLINK_LIBRARIES=${LUA_LIBRARIES} + RUN_OUTPUT_VARIABLE LUA_TRY_OUT) + if ("${LUA_CHECK2}" MATCHES "0" AND "${LUA_CHECK_BUILD2}$" MATCHES "TRUE") + message(STATUS "lua_objlen found") + set(HAS_LUA_OBJLEN TRUE) + else() + message(STATUS "lua_objlen is not available, using lua_rawlen instead") + endif() + endif ()