From a6116e3156823163658ad0306b17bc7ecd71a5e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Apr 2014 10:36:57 -0700 Subject: [PATCH] test(lua): reactivate some of the Lua unit tests Signed-off-by: Leonardo de Moura --- src/shell/CMakeLists.txt | 16 ++++++++-------- tests/lua/map2.lua | 2 +- tests/lua/n5.lua | 2 -- tests/lua/{ => old}/big.lua | 0 tests/lua/{ => old}/ceq1.lua | 0 tests/lua/{ => old}/cex_builder1.lua | 0 tests/lua/{ => old}/coercion_bug1.lua | 0 tests/lua/{ => old}/context1.lua | 0 tests/lua/{ => old}/env1.lua | 0 tests/lua/{ => old}/env2.lua | 0 tests/lua/{ => old}/env3.lua | 0 tests/lua/{ => old}/env4.lua | 0 tests/lua/{ => old}/expr1.lua | 0 tests/lua/{ => old}/expr2.lua | 0 tests/lua/{ => old}/expr3.lua | 0 tests/lua/{ => old}/expr4.lua | 0 tests/lua/{ => old}/expr5.lua | 0 tests/lua/{ => old}/expr6.lua | 0 tests/lua/{ => old}/expr7.lua | 0 tests/lua/{ => old}/expr8.lua | 0 tests/lua/{ => old}/fields.lua | 0 tests/lua/{ => old}/fmt1.lua | 0 tests/lua/{ => old}/front.lua | 0 tests/lua/{ => old}/goal1.lua | 0 tests/lua/{ => old}/hidden1.lua | 0 tests/lua/{ => old}/hop1.lua | 0 tests/lua/{ => old}/hop2.lua | 0 tests/lua/{ => old}/import.lua | 0 tests/lua/{ => old}/io_state1.lua | 0 tests/lua/{ => old}/is_prop1.lua | 0 tests/lua/{ => old}/jst1.lua | 0 tests/lua/{ => old}/level1.lua | 0 tests/lua/{ => old}/localctx1.lua | 0 tests/lua/{ => old}/m1.lua | 0 tests/lua/{ => old}/map.lua | 0 tests/lua/{ => old}/menv1.lua | 0 tests/lua/{ => old}/num2.lua | 0 tests/lua/{ => old}/parser1.lua | 0 tests/lua/{ => old}/parser2.lua | 0 tests/lua/{ => old}/proof_builder1.lua | 0 tests/lua/{ => old}/proof_state1.lua | 0 tests/lua/{ => old}/proof_stats.lua | 0 tests/lua/{ => old}/simp1.lua | 0 tests/lua/{ => old}/single.lua | 0 tests/lua/{ => old}/splay1.lua | 0 tests/lua/{ => old}/st1.lua | 0 tests/lua/{ => old}/st2.lua | 0 tests/lua/{ => old}/st3.lua | 0 tests/lua/{ => old}/tactic1.lua | 0 tests/lua/{ => old}/template1.lua | 0 tests/lua/{ => old}/ty1.lua | 0 tests/lua/{ => old}/ty2.lua | 0 tests/lua/{ => old}/unify1.lua | 0 53 files changed, 9 insertions(+), 11 deletions(-) rename tests/lua/{ => old}/big.lua (100%) rename tests/lua/{ => old}/ceq1.lua (100%) rename tests/lua/{ => old}/cex_builder1.lua (100%) rename tests/lua/{ => old}/coercion_bug1.lua (100%) rename tests/lua/{ => old}/context1.lua (100%) rename tests/lua/{ => old}/env1.lua (100%) rename tests/lua/{ => old}/env2.lua (100%) rename tests/lua/{ => old}/env3.lua (100%) rename tests/lua/{ => old}/env4.lua (100%) rename tests/lua/{ => old}/expr1.lua (100%) rename tests/lua/{ => old}/expr2.lua (100%) rename tests/lua/{ => old}/expr3.lua (100%) rename tests/lua/{ => old}/expr4.lua (100%) rename tests/lua/{ => old}/expr5.lua (100%) rename tests/lua/{ => old}/expr6.lua (100%) rename tests/lua/{ => old}/expr7.lua (100%) rename tests/lua/{ => old}/expr8.lua (100%) rename tests/lua/{ => old}/fields.lua (100%) rename tests/lua/{ => old}/fmt1.lua (100%) rename tests/lua/{ => old}/front.lua (100%) rename tests/lua/{ => old}/goal1.lua (100%) rename tests/lua/{ => old}/hidden1.lua (100%) rename tests/lua/{ => old}/hop1.lua (100%) rename tests/lua/{ => old}/hop2.lua (100%) rename tests/lua/{ => old}/import.lua (100%) rename tests/lua/{ => old}/io_state1.lua (100%) rename tests/lua/{ => old}/is_prop1.lua (100%) rename tests/lua/{ => old}/jst1.lua (100%) rename tests/lua/{ => old}/level1.lua (100%) rename tests/lua/{ => old}/localctx1.lua (100%) rename tests/lua/{ => old}/m1.lua (100%) rename tests/lua/{ => old}/map.lua (100%) rename tests/lua/{ => old}/menv1.lua (100%) rename tests/lua/{ => old}/num2.lua (100%) rename tests/lua/{ => old}/parser1.lua (100%) rename tests/lua/{ => old}/parser2.lua (100%) rename tests/lua/{ => old}/proof_builder1.lua (100%) rename tests/lua/{ => old}/proof_state1.lua (100%) rename tests/lua/{ => old}/proof_stats.lua (100%) rename tests/lua/{ => old}/simp1.lua (100%) rename tests/lua/{ => old}/single.lua (100%) rename tests/lua/{ => old}/splay1.lua (100%) rename tests/lua/{ => old}/st1.lua (100%) rename tests/lua/{ => old}/st2.lua (100%) rename tests/lua/{ => old}/st3.lua (100%) rename tests/lua/{ => old}/tactic1.lua (100%) rename tests/lua/{ => old}/template1.lua (100%) rename tests/lua/{ => old}/ty1.lua (100%) rename tests/lua/{ => old}/ty2.lua (100%) rename tests/lua/{ => old}/unify1.lua (100%) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 672733f45..371fc23bb 100644 --- a/src/shell/CMakeLists.txt +++ b/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 -# file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua") -# FOREACH(T ${LEANLUATESTS}) -# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) -# add_test(NAME "leanluatest_${T_NAME}" -# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" -# COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) -# ENDFOREACH(T) +# LEAN LUA TESTS +file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua") +FOREACH(T ${LEANLUATESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanluatest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) +ENDFOREACH(T) # # LEAN DOCS # file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md") diff --git a/tests/lua/map2.lua b/tests/lua/map2.lua index 4a3f248a6..2349cf51d 100644 --- a/tests/lua/map2.lua +++ b/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 diff --git a/tests/lua/n5.lua b/tests/lua/n5.lua index 469e6c973..bfd113c5d 100644 --- a/tests/lua/n5.lua +++ b/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()) diff --git a/tests/lua/big.lua b/tests/lua/old/big.lua similarity index 100% rename from tests/lua/big.lua rename to tests/lua/old/big.lua diff --git a/tests/lua/ceq1.lua b/tests/lua/old/ceq1.lua similarity index 100% rename from tests/lua/ceq1.lua rename to tests/lua/old/ceq1.lua diff --git a/tests/lua/cex_builder1.lua b/tests/lua/old/cex_builder1.lua similarity index 100% rename from tests/lua/cex_builder1.lua rename to tests/lua/old/cex_builder1.lua diff --git a/tests/lua/coercion_bug1.lua b/tests/lua/old/coercion_bug1.lua similarity index 100% rename from tests/lua/coercion_bug1.lua rename to tests/lua/old/coercion_bug1.lua diff --git a/tests/lua/context1.lua b/tests/lua/old/context1.lua similarity index 100% rename from tests/lua/context1.lua rename to tests/lua/old/context1.lua diff --git a/tests/lua/env1.lua b/tests/lua/old/env1.lua similarity index 100% rename from tests/lua/env1.lua rename to tests/lua/old/env1.lua diff --git a/tests/lua/env2.lua b/tests/lua/old/env2.lua similarity index 100% rename from tests/lua/env2.lua rename to tests/lua/old/env2.lua diff --git a/tests/lua/env3.lua b/tests/lua/old/env3.lua similarity index 100% rename from tests/lua/env3.lua rename to tests/lua/old/env3.lua diff --git a/tests/lua/env4.lua b/tests/lua/old/env4.lua similarity index 100% rename from tests/lua/env4.lua rename to tests/lua/old/env4.lua diff --git a/tests/lua/expr1.lua b/tests/lua/old/expr1.lua similarity index 100% rename from tests/lua/expr1.lua rename to tests/lua/old/expr1.lua diff --git a/tests/lua/expr2.lua b/tests/lua/old/expr2.lua similarity index 100% rename from tests/lua/expr2.lua rename to tests/lua/old/expr2.lua diff --git a/tests/lua/expr3.lua b/tests/lua/old/expr3.lua similarity index 100% rename from tests/lua/expr3.lua rename to tests/lua/old/expr3.lua diff --git a/tests/lua/expr4.lua b/tests/lua/old/expr4.lua similarity index 100% rename from tests/lua/expr4.lua rename to tests/lua/old/expr4.lua diff --git a/tests/lua/expr5.lua b/tests/lua/old/expr5.lua similarity index 100% rename from tests/lua/expr5.lua rename to tests/lua/old/expr5.lua diff --git a/tests/lua/expr6.lua b/tests/lua/old/expr6.lua similarity index 100% rename from tests/lua/expr6.lua rename to tests/lua/old/expr6.lua diff --git a/tests/lua/expr7.lua b/tests/lua/old/expr7.lua similarity index 100% rename from tests/lua/expr7.lua rename to tests/lua/old/expr7.lua diff --git a/tests/lua/expr8.lua b/tests/lua/old/expr8.lua similarity index 100% rename from tests/lua/expr8.lua rename to tests/lua/old/expr8.lua diff --git a/tests/lua/fields.lua b/tests/lua/old/fields.lua similarity index 100% rename from tests/lua/fields.lua rename to tests/lua/old/fields.lua diff --git a/tests/lua/fmt1.lua b/tests/lua/old/fmt1.lua similarity index 100% rename from tests/lua/fmt1.lua rename to tests/lua/old/fmt1.lua diff --git a/tests/lua/front.lua b/tests/lua/old/front.lua similarity index 100% rename from tests/lua/front.lua rename to tests/lua/old/front.lua diff --git a/tests/lua/goal1.lua b/tests/lua/old/goal1.lua similarity index 100% rename from tests/lua/goal1.lua rename to tests/lua/old/goal1.lua diff --git a/tests/lua/hidden1.lua b/tests/lua/old/hidden1.lua similarity index 100% rename from tests/lua/hidden1.lua rename to tests/lua/old/hidden1.lua diff --git a/tests/lua/hop1.lua b/tests/lua/old/hop1.lua similarity index 100% rename from tests/lua/hop1.lua rename to tests/lua/old/hop1.lua diff --git a/tests/lua/hop2.lua b/tests/lua/old/hop2.lua similarity index 100% rename from tests/lua/hop2.lua rename to tests/lua/old/hop2.lua diff --git a/tests/lua/import.lua b/tests/lua/old/import.lua similarity index 100% rename from tests/lua/import.lua rename to tests/lua/old/import.lua diff --git a/tests/lua/io_state1.lua b/tests/lua/old/io_state1.lua similarity index 100% rename from tests/lua/io_state1.lua rename to tests/lua/old/io_state1.lua diff --git a/tests/lua/is_prop1.lua b/tests/lua/old/is_prop1.lua similarity index 100% rename from tests/lua/is_prop1.lua rename to tests/lua/old/is_prop1.lua diff --git a/tests/lua/jst1.lua b/tests/lua/old/jst1.lua similarity index 100% rename from tests/lua/jst1.lua rename to tests/lua/old/jst1.lua diff --git a/tests/lua/level1.lua b/tests/lua/old/level1.lua similarity index 100% rename from tests/lua/level1.lua rename to tests/lua/old/level1.lua diff --git a/tests/lua/localctx1.lua b/tests/lua/old/localctx1.lua similarity index 100% rename from tests/lua/localctx1.lua rename to tests/lua/old/localctx1.lua diff --git a/tests/lua/m1.lua b/tests/lua/old/m1.lua similarity index 100% rename from tests/lua/m1.lua rename to tests/lua/old/m1.lua diff --git a/tests/lua/map.lua b/tests/lua/old/map.lua similarity index 100% rename from tests/lua/map.lua rename to tests/lua/old/map.lua diff --git a/tests/lua/menv1.lua b/tests/lua/old/menv1.lua similarity index 100% rename from tests/lua/menv1.lua rename to tests/lua/old/menv1.lua diff --git a/tests/lua/num2.lua b/tests/lua/old/num2.lua similarity index 100% rename from tests/lua/num2.lua rename to tests/lua/old/num2.lua diff --git a/tests/lua/parser1.lua b/tests/lua/old/parser1.lua similarity index 100% rename from tests/lua/parser1.lua rename to tests/lua/old/parser1.lua diff --git a/tests/lua/parser2.lua b/tests/lua/old/parser2.lua similarity index 100% rename from tests/lua/parser2.lua rename to tests/lua/old/parser2.lua diff --git a/tests/lua/proof_builder1.lua b/tests/lua/old/proof_builder1.lua similarity index 100% rename from tests/lua/proof_builder1.lua rename to tests/lua/old/proof_builder1.lua diff --git a/tests/lua/proof_state1.lua b/tests/lua/old/proof_state1.lua similarity index 100% rename from tests/lua/proof_state1.lua rename to tests/lua/old/proof_state1.lua diff --git a/tests/lua/proof_stats.lua b/tests/lua/old/proof_stats.lua similarity index 100% rename from tests/lua/proof_stats.lua rename to tests/lua/old/proof_stats.lua diff --git a/tests/lua/simp1.lua b/tests/lua/old/simp1.lua similarity index 100% rename from tests/lua/simp1.lua rename to tests/lua/old/simp1.lua diff --git a/tests/lua/single.lua b/tests/lua/old/single.lua similarity index 100% rename from tests/lua/single.lua rename to tests/lua/old/single.lua diff --git a/tests/lua/splay1.lua b/tests/lua/old/splay1.lua similarity index 100% rename from tests/lua/splay1.lua rename to tests/lua/old/splay1.lua diff --git a/tests/lua/st1.lua b/tests/lua/old/st1.lua similarity index 100% rename from tests/lua/st1.lua rename to tests/lua/old/st1.lua diff --git a/tests/lua/st2.lua b/tests/lua/old/st2.lua similarity index 100% rename from tests/lua/st2.lua rename to tests/lua/old/st2.lua diff --git a/tests/lua/st3.lua b/tests/lua/old/st3.lua similarity index 100% rename from tests/lua/st3.lua rename to tests/lua/old/st3.lua diff --git a/tests/lua/tactic1.lua b/tests/lua/old/tactic1.lua similarity index 100% rename from tests/lua/tactic1.lua rename to tests/lua/old/tactic1.lua diff --git a/tests/lua/template1.lua b/tests/lua/old/template1.lua similarity index 100% rename from tests/lua/template1.lua rename to tests/lua/old/template1.lua diff --git a/tests/lua/ty1.lua b/tests/lua/old/ty1.lua similarity index 100% rename from tests/lua/ty1.lua rename to tests/lua/old/ty1.lua diff --git a/tests/lua/ty2.lua b/tests/lua/old/ty2.lua similarity index 100% rename from tests/lua/ty2.lua rename to tests/lua/old/ty2.lua diff --git a/tests/lua/unify1.lua b/tests/lua/old/unify1.lua similarity index 100% rename from tests/lua/unify1.lua rename to tests/lua/old/unify1.lua