diff --git a/src/cmake/check_main.sh b/src/cmake/check_main.sh deleted file mode 100644 index ad69f829e6..0000000000 --- a/src/cmake/check_main.sh +++ /dev/null @@ -1,69 +0,0 @@ -#!/usr/bin/env bash - -set -e - -if [ $# -ne 3 -a $# -ne 2 ]; then - echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?" - exit 1 -fi -ulimit -s 8192 -LEAN=$1 -BIN_DIR=../../../bin -export LEAN_PATH=Init=../../../src/Init:Test=. - -if [ $# -ne 3 ]; then - INTERACTIVE=no -else - INTERACTIVE=$3 -fi -ff=$2 - -if [[ "$OSTYPE" == "msys" ]]; then - # Windows running MSYS2 - # Replace /c/ with c:, and / with \\ - ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g') -fi - -DIFF=diff -if diff --color --help >/dev/null 2>&1; then - DIFF="diff --color"; -fi - -$LEAN --cpp="$ff".cpp "$ff" || echo oh ho! -if [ $? -ne 0 ]; then - echo "Failed to compile $ff into C++ file" - exit 1 -fi - -$BIN_DIR/leanc -O3 -DNDEBUG -o "$ff.out" $ff.cpp -if [ $? -ne 0 ]; then - echo "Failed to compile C++ file $ff.cpp" - exit 1 -fi -"./$ff.out" > "$ff.produced.out" 2>&1 || true - -if test -f "$ff.expected.out"; then - if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then - echo "-- checked" - exit 0 - else - echo "ERROR: file $ff.produced.out does not match $ff.expected.out" - if [ $INTERACTIVE == "yes" ]; then - meld "$ff.produced.out" "$ff.expected.out" - if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then - echo "-- mismatch was fixed" - fi - fi - exit 1 - fi -else - echo "ERROR: file $ff.expected.out does not exist" - if [ $INTERACTIVE == "yes" ]; then - read -p "copy $ff.produced.out (y/n)? " - if [ $REPLY == "y" ]; then - cp -- "$ff.produced.out" "$ff.expected.out" - echo "-- copied $ff.produced.out --> $ff.expected.out" - fi - fi - exit 1 -fi diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 515791a832..4cbd9b5536 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -143,9 +143,6 @@ add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) # add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") -add_test(NAME lean_test_main_error - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash "${LEAN_SOURCE_DIR}/cmake/check_main.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_error.lean") if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) # The following test cannot be executed on Windows because of the # bash script timeout.sh diff --git a/tests/lean/run/print_error.lean b/tests/compiler/print_error.lean similarity index 100% rename from tests/lean/run/print_error.lean rename to tests/compiler/print_error.lean diff --git a/tests/lean/run/print_error.lean.expected.out b/tests/compiler/print_error.lean.expected.out similarity index 100% rename from tests/lean/run/print_error.lean.expected.out rename to tests/compiler/print_error.lean.expected.out diff --git a/tests/compiler/print_error.lean.expected.ret b/tests/compiler/print_error.lean.expected.ret new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/compiler/print_error.lean.expected.ret @@ -0,0 +1 @@ +1 diff --git a/tests/compiler/test_single.sh b/tests/compiler/test_single.sh index 91d42d341e..5920e5870c 100755 --- a/tests/compiler/test_single.sh +++ b/tests/compiler/test_single.sh @@ -37,10 +37,16 @@ if [ $? -ne 0 ]; then exit 1 fi -"./$ff.out" > "$ff.produced.out" -if [ $? -ne 0 ]; then - echo "Failed to execute $ff.out" - exit 1 +expected_ret=0 +if [ -f "$ff.expected.ret" ]; then + expected_ret=$(< "$ff.expected.ret") +fi +ret=0 +"./$ff.out" > "$ff.produced.out" 2>&1 || ret=$? +if [ -n $expected_ret ] && [ $ret -ne $expected_ret ]; then + echo "Unexpected return code $ret executing $ff.out; expected $expected_ret.\nOutput:" + cat "$ff.produced.out" + exit 1 fi if test -f "$ff.expected.out"; then diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh index 2f591b8cf0..c21f6ea232 100755 --- a/tests/compiler/test_single_interpret.sh +++ b/tests/compiler/test_single_interpret.sh @@ -25,10 +25,14 @@ if diff --color --help >/dev/null 2>&1; then DIFF="diff --color"; fi -$LEAN --run "$ff" > "$ff.interp.produced.out" -if [ $? -ne 0 ]; then - echo "Failed to execute $ff" - exit 1 +expected_ret=0 +if [ -f "$ff.expected.ret" ]; then + expected_ret=$(< "$ff.expected.ret") +fi +$LEAN --run "$ff" > "$ff.interp.produced.out" 2>&1 +if [ $? -ne $expected_ret ]; then + echo "Unexpected return code $? executing $ff; expected $expected_ret" + exit 1 fi if test -f "$ff.expected.out"; then