feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint

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

src/shell/CMakeLists.txt

@@ -58,14 +58,15 @@ FOREACH(T ${LEANITTESTS})
            COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)
 
-# # LEAN SLOW TESTS
+# LEAN SLOW TESTS
-# file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
+file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean")
-# FOREACH(T ${LEANSLOWTESTS})
+FOREACH(T ${LEANSLOWTESTS})
-#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-#   add_test(NAME "leanslowtest_${T_NAME}"
+  add_test(NAME "leanslowtest_${T_NAME}"
-#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
-#            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)
+  set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
+ENDFOREACH(T)
 
 # LEAN LUA TESTS
 file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")

tests/lean/slow/test_single.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+if [ $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file]"
+    exit 1
+fi
+ulimit -s 8192
+LEAN=$1
+export LEAN_PATH=../../../library/standard:.
+f=$2
+echo "-- testing $f"
+if $LEAN $f; then
+   echo "-- checked"
+else
+   echo "failed $f"
+   exit 1
+fi