From 0eaa98221b50d4552159323ceb5ef0b4148d0143 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 9 Dec 2013 12:17:43 -0800 Subject: [PATCH] fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests Signed-off-by: Leonardo de Moura --- src/cmake/check_failure.sh | 7 +++++ src/cmake/redirect.sh | 11 ++++++++ src/shell/CMakeLists.txt | 16 ++++++++++- src/shell/lean.cpp | 31 +++++++++++++++------- src/shell/lua_repl.h | 41 +++++++++++++++++++++++++++++ tests/lean/single.lean | 6 +++++ tests/lean/single.lean.expected.out | 7 +++++ tests/lua/single.lua | 4 +++ 8 files changed, 112 insertions(+), 11 deletions(-) create mode 100755 src/cmake/check_failure.sh create mode 100755 src/cmake/redirect.sh create mode 100644 src/shell/lua_repl.h create mode 100644 tests/lean/single.lean create mode 100644 tests/lean/single.lean.expected.out create mode 100644 tests/lua/single.lua diff --git a/src/cmake/check_failure.sh b/src/cmake/check_failure.sh new file mode 100755 index 000000000..4870fba4a --- /dev/null +++ b/src/cmake/check_failure.sh @@ -0,0 +1,7 @@ +#!/bin/bash +# Auxiliary script that succeeds iff if the execution of input +# arguments fail. +if $*; then + echo "unexpected success" + exit 1 +fi diff --git a/src/cmake/redirect.sh b/src/cmake/redirect.sh new file mode 100755 index 000000000..1f61db999 --- /dev/null +++ b/src/cmake/redirect.sh @@ -0,0 +1,11 @@ +#!/bin/bash +# Auxiliary script for redirecting input +# Given the arguments $1 ... $n-1 $n, +# it executes the command +# $1 ... $n-1 < $n +# This is a hack to workaround a ctest limitation +length=$(($#-1)) +array=${@:1:$length} +shift `expr $# - 1` +last=`echo $1` +$array < $last diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 033bba4d7..cb19253bd 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -4,7 +4,21 @@ add_executable(lean lean.cpp) add_dependencies(lean githash) target_link_libraries(lean ${EXTRA_LIBS}) -add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean") +add_test(example1_stdin1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") +add_test(example1_stdin2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "-l" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") +add_test(example1_stdin3 ${LEAN_SOURCE_DIR}/cmake/redirect.sh ${CMAKE_CURRENT_BINARY_DIR}/lean "--lean" "${LEAN_SOURCE_DIR}/../tests/lean/single.lean") +add_test(lean_help1 ${CMAKE_CURRENT_BINARY_DIR}/lean --help) +add_test(lean_help2 ${CMAKE_CURRENT_BINARY_DIR}/lean --h) +add_test(lean_version1 ${CMAKE_CURRENT_BINARY_DIR}/lean --version) +add_test(lean_version2 ${CMAKE_CURRENT_BINARY_DIR}/lean --v) +add_test(lean_ghash1 ${CMAKE_CURRENT_BINARY_DIR}/lean -g) +add_test(lean_ghash2 ${CMAKE_CURRENT_BINARY_DIR}/lean --githash) +add_test(lean_luahook1 ${CMAKE_CURRENT_BINARY_DIR}/lean --luahook=100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") +add_test(lean_luahook2 ${CMAKE_CURRENT_BINARY_DIR}/lean -c 100 "${LEAN_SOURCE_DIR}/../tests/lua/big.lua") +add_test(lean_lua1 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "--lua" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") +add_test(lean_lua2 ${LEAN_SOURCE_DIR}/cmake/redirect.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-u" "${LEAN_SOURCE_DIR}/../tests/lua/single.lua") +add_test(lean_unknown_option ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") + # LEAN EXAMPLES file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean") diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 3df97c021..d11ba4ba7 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -15,9 +15,12 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "util/script_state.h" #include "kernel/printer.h" +#include "library/io_state.h" +#include "library/kernel_bindings.h" #include "frontends/lean/parser.h" #include "frontends/lean/frontend.h" #include "frontends/lua/register_modules.h" +#include "shell/lua_repl.h" #include "version.h" #include "githash.h" // NOLINT @@ -83,7 +86,7 @@ int main(int argc, char ** argv) { lean::register_modules(); input_kind default_k = input_kind::Lean; // default while (true) { - int c = getopt_long(argc, argv, "gvhc:012", g_long_options, &optind); + int c = getopt_long(argc, argv, "lugvhc:012", g_long_options, &optind); if (c == -1) break; // end of command line switch (c) { @@ -111,19 +114,27 @@ int main(int argc, char ** argv) { return 1; } } - frontend f; - script_state S; if (optind >= argc) { display_header(std::cout); - #if defined(LEAN_WINDOWS) - std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl; - #else - std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; - #endif - shell sh(f, &S); signal(SIGINT, on_ctrl_c); - return sh(); + if (default_k == input_kind::Lean) { + #if defined(LEAN_WINDOWS) + std::cout << "Type 'Exit.' to exit or 'Help.' for help."<< std::endl; + #else + std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl; + #endif + frontend f; + script_state S; + shell sh(f, &S); + return sh() ? 0 : 1; + } else { + lean_assert(default_k == input_kind::Lua); + script_state S; + S.dostring(g_lua_repl); + } } else { + frontend f; + script_state S; bool ok = true; for (int i = optind; i < argc; i++) { char const * ext = get_file_extension(argv[i]); diff --git a/src/shell/lua_repl.h b/src/shell/lua_repl.h new file mode 100644 index 000000000..bae05c749 --- /dev/null +++ b/src/shell/lua_repl.h @@ -0,0 +1,41 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +// Very simple read-eval-print for Lua +static char const * g_lua_repl = + "local function trim(s)\n" + " return s:gsub('^%s+', ''):gsub('%s+$', '')\n" + "end\n" + "local function show_results(...)\n" + " if select('#', ...) > 1 then\n" + " print(select(2, ...))\n" + " end\n" + "end\n" + "print([[Type 'Exit' to exit.]])\n" + "repeat\n" + " io.write'lean > '\n" + " local s = io.read()\n" + " if s == nil then print(""); break end\n" + " if trim(s) == 'Exit' then break end\n" + " local f, err = load(s, 'stdin')\n" + " if err then\n" + " f = load('return (' .. s .. ')', 'stdin')\n" + " end\n" + " if f then\n" + " local ok, err = pcall(f)\n" + " if not ok then\n" + " if is_exception(err) then\n" + " print(err:what())\n" + " else\n" + " print(err)\n" + " end\n" + " else\n" + " if err then print(err) end\n" + " end\n" + " else\n" + " print(err)\n" + " end\n" + "until false\n"; diff --git a/tests/lean/single.lean b/tests/lean/single.lean new file mode 100644 index 000000000..99b96f480 --- /dev/null +++ b/tests/lean/single.lean @@ -0,0 +1,6 @@ +Variables a b c : Int. +Show a + b + c. +Check a + b. +Exit. +(* the following line should be executed *) +Check a + true. diff --git a/tests/lean/single.lean.expected.out b/tests/lean/single.lean.expected.out new file mode 100644 index 000000000..4839be9f7 --- /dev/null +++ b/tests/lean/single.lean.expected.out @@ -0,0 +1,7 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: c +a + b + c +a + b : ℤ diff --git a/tests/lua/single.lua b/tests/lua/single.lua new file mode 100644 index 000000000..7f687f55d --- /dev/null +++ b/tests/lua/single.lua @@ -0,0 +1,4 @@ +print("hello world") +local env = environment() +parse_lean_cmds([[ Variables a b : Int ]], env) +print(parse_lean([[a + b + 10]], env))