chore(tests/shell/test): remove

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)

src/tests/shell/.gitignore

@@ -1 +0,0 @@
-*.produced.out

src/tests/shell/CMakeLists.txt

@@ -1,2 +0,0 @@
-add_executable(shell_test shell.cpp)
-target_link_libraries(shell_test leanstatic)

src/tests/shell/shell.cpp

@@ -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 <string>
-#include <vector>
-#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<uintptr_t>(msg.c_str()));
-    msg = "{\"seq_num\": 1, \"command\": \"info\", \"file_name\": \"f\", \"line\": 2, \"column\": 9}";
-    emscripten_process_request(reinterpret_cast<uintptr_t>(msg.c_str()));
-    finalize_emscripten();
-}

src/tests/shell/shell_test.expected.out

@@ -1 +0,0 @@
-{"message":"file invalidated","response":"ok","seq_num":0}

src/tests/shell/test.sh

@@ -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