diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index aa35db718a..c83d6e8647 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -446,7 +446,6 @@ endfunction() add_subdirectory(tests/util) add_subdirectory(tests/kernel) add_subdirectory(tests/library) -add_subdirectory(tests/shell) # Include style check if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND PYTHONINTERP_FOUND) diff --git a/src/tests/shell/.gitignore b/src/tests/shell/.gitignore deleted file mode 100644 index 4cf1a84d6e..0000000000 --- a/src/tests/shell/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*.produced.out diff --git a/src/tests/shell/CMakeLists.txt b/src/tests/shell/CMakeLists.txt deleted file mode 100644 index f17d4fdf76..0000000000 --- a/src/tests/shell/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_executable(shell_test shell.cpp) -target_link_libraries(shell_test leanstatic) diff --git a/src/tests/shell/shell.cpp b/src/tests/shell/shell.cpp deleted file mode 100644 index d12cf1be94..0000000000 --- a/src/tests/shell/shell.cpp +++ /dev/null @@ -1,21 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/test.h" -#include "shell/lean_js.h -using namespace lean; - -int main() { - save_stack_info(); - initialize_emscripten(); - std::string msg = "{\"seq_num\": 0, \"command\": \"sync\", \"file_name\": \"f\", \"content\": \"inductive f\\ndef g := f\"}"; - emscripten_process_request(reinterpret_cast(msg.c_str())); - msg = "{\"seq_num\": 1, \"command\": \"info\", \"file_name\": \"f\", \"line\": 2, \"column\": 9}"; - emscripten_process_request(reinterpret_cast(msg.c_str())); - finalize_emscripten(); -} diff --git a/src/tests/shell/shell_test.expected.out b/src/tests/shell/shell_test.expected.out deleted file mode 100644 index 74f6c648af..0000000000 --- a/src/tests/shell/shell_test.expected.out +++ /dev/null @@ -1 +0,0 @@ -{"message":"file invalidated","response":"ok","seq_num":0} diff --git a/src/tests/shell/test.sh b/src/tests/shell/test.sh deleted file mode 100644 index 3c41d18130..0000000000 --- a/src/tests/shell/test.sh +++ /dev/null @@ -1,23 +0,0 @@ -#!/bin/sh -set -e -if [ $# -ne 1 ]; then - echo "Usage: test.sh [shell_test-path]" - exit 1 -fi -SHELL_TEST=$1 -f="shell_test" - -LEAN_PATH=../../../library:. $SHELL_TEST > $f.produced.out - -if test -f "$f.expected.out"; then - if diff --ignore-all-space "$f.produced.out" "$f.expected.out"; then - echo "-- checked" - exit 0 - else - echo "ERROR: file $f.produced.out does not match $f.expected.out" - exit 1 - fi -else - echo "ERROR: file $f.expected.out does not exist" - exit 1 -fi