From 6da194334e76b6d9cc3b29bece202e874b4cf99d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Sep 2013 08:47:06 -0700
Subject: [PATCH] Move 'slow' test files to different subdir. Modify
 CTestCustom.cmake.in to run leantests.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CTestCustom.cmake.in                     | 6 +++---
 src/shell/CMakeLists.txt                     | 3 +++
 tests/lean/slow/config.lean                  | 3 +++
 tests/lean/slow/config.lean.expected.out     | 4 ++++
 tests/lean/{ => slow}/deep.lean              | 0
 tests/lean/{ => slow}/deep.lean.expected.out | 0
 6 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/slow/config.lean
 create mode 100644 tests/lean/slow/config.lean.expected.out
 rename tests/lean/{ => slow}/deep.lean (100%)
 rename tests/lean/{ => slow}/deep.lean.expected.out (100%)

diff --git a/src/CTestCustom.cmake.in b/src/CTestCustom.cmake.in
index deead2fff..9459b6f7a 100644
--- a/src/CTestCustom.cmake.in
+++ b/src/CTestCustom.cmake.in
@@ -1,11 +1,11 @@
 # Complete list of options is available at http://cmake.org/Wiki/CMake/Testing_With_CTest
 
 # List of tests to ignore during the MemCheck stage
-SET(CTEST_CUSTOM_MEMCHECK_IGNORE ${CTEST_CUSTOM_MEMCHECK_IGNORE} 
-    "leantests"
+SET(CTEST_CUSTOM_MEMCHECK_IGNORE ${CTEST_CUSTOM_MEMCHECK_IGNORE}
+    "leanslowtests"
     "threads"
     )
-    
+
 # Regular expression for excluding files from coverage testing
 SET(CTEST_CUSTOM_COVERAGE_EXCLUDE ${CTEST_CUSTOM_COVERAGE_EXCLUDE} "tests/*")
 
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 7cb14376d..82d98d830 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -8,3 +8,6 @@ add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../exampl
 add_test(NAME leantests
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
          COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME leanslowtests
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
+         COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
diff --git a/tests/lean/slow/config.lean b/tests/lean/slow/config.lean
new file mode 100644
index 000000000..905e75340
--- /dev/null
+++ b/tests/lean/slow/config.lean
@@ -0,0 +1,3 @@
+(* Set default configuration for tests *)
+Set pp::colors  false
+Set pp::unicode true
diff --git a/tests/lean/slow/config.lean.expected.out b/tests/lean/slow/config.lean.expected.out
new file mode 100644
index 000000000..7e317fecc
--- /dev/null
+++ b/tests/lean/slow/config.lean.expected.out
@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Set: pp::colors
+  Set: pp::unicode
diff --git a/tests/lean/deep.lean b/tests/lean/slow/deep.lean
similarity index 100%
rename from tests/lean/deep.lean
rename to tests/lean/slow/deep.lean
diff --git a/tests/lean/deep.lean.expected.out b/tests/lean/slow/deep.lean.expected.out
similarity index 100%
rename from tests/lean/deep.lean.expected.out
rename to tests/lean/slow/deep.lean.expected.out