fix(build): add CheckLuaObjlen.cc test, not every Lua version has the function lua_objlen

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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()

src/bindings/lua/expr.cpp

@@ -112,7 +112,7 @@ static std::pair<expr, expr> 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);

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;

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.
 */

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 <iostream>
+#include <memory>
+#include <lua.hpp>
+
+// 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;
+}

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 ()