test(lua): reactivate some of the Lua unit tests

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

src/shell/CMakeLists.txt

@@ -67,14 +67,14 @@ install(TARGETS lean DESTINATION bin)
 #            COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME})
 # ENDFOREACH(T)
 
-# # LEAN LUA TESTS
+# LEAN LUA TESTS
-# file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
+file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
-# FOREACH(T ${LEANLUATESTS})
+FOREACH(T ${LEANLUATESTS})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leanluatest_${T_NAME}"
+  add_test(NAME "leanluatest_${T_NAME}"
-#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
-#            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME})
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME})
-# ENDFOREACH(T)
+ENDFOREACH(T)
 
 # # LEAN DOCS
 # file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md")

tests/lua/map2.lua

@@ -1,4 +1,4 @@
-local m = splay_map()
+local m = rb_map()
 for i = 1, 100 do
    m:insert(i, i * 3)
 end

tests/lua/n5.lua

@@ -1,5 +1,3 @@
 assert(not pcall(function() name(mpz(10)) end))
 assert(not pcall(function() name(function() return 1 end) end))
-assert(Const{"x", name("y", 1), 1}:fields() == name("x", "y", 1, 1))
-assert(not pcall(function() Const({"x", function() return 1 end}) end))
 assert(name("x", 1):hash() == name("x", 1):hash())