From a98fdd9be66c34d145d53560a12cd4a35c37687d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2013 16:47:47 -0800 Subject: [PATCH] refactor(shell): combine lean and leanlua executables in a single executable The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files. Example: ./lean extension1.lua extension2.lua file.lean Signed-off-by: Leonardo de Moura --- doc/lua/test.sh | 6 ++--- doc/lua/test_single.sh | 6 ++--- src/CMakeLists.txt | 1 - src/shell/CMakeLists.txt | 26 ++++++++++++++++++++ src/shell/lean.cpp | 47 +++++++++++++++++++++++++++++++++--- src/shell/lua/CMakeLists.txt | 28 --------------------- src/shell/lua/leanlua.cpp | 24 ------------------ src/tests/util/list.cpp | 1 + tests/lua/test.sh | 6 ++--- tests/lua/test_single.sh | 6 ++--- 10 files changed, 82 insertions(+), 69 deletions(-) delete mode 100644 src/shell/lua/CMakeLists.txt delete mode 100644 src/shell/lua/leanlua.cpp diff --git a/doc/lua/test.sh b/doc/lua/test.sh index 1661aadbbc..e9e5d4316b 100755 --- a/doc/lua/test.sh +++ b/doc/lua/test.sh @@ -1,16 +1,16 @@ #!/bin/sh # Test is all examples in the .md files are working if [ $# -ne 1 ]; then - echo "Usage: test.sh [leanlua-executable-path]" + echo "Usage: test.sh [lean-executable-path]" exit 1 fi ulimit -s unlimited -LEANLUA=$1 +LEAN=$1 NUM_ERRORS=0 for f in `ls *.md`; do echo "-- testing $f" awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua - if $LEANLUA $f.lua > $f.produced.out; then + if $LEAN $f.lua > $f.produced.out; then echo "-- worked" else echo "ERROR executing $f.lua, produced output is at $f.produced.out" diff --git a/doc/lua/test_single.sh b/doc/lua/test_single.sh index 7288daab3b..5faa8bcfdf 100755 --- a/doc/lua/test_single.sh +++ b/doc/lua/test_single.sh @@ -1,15 +1,15 @@ #!/bin/sh # Test is all examples in the .md files are working if [ $# -ne 2 ]; then - echo "Usage: test.sh [leanlua-executable-path] [file]" + echo "Usage: test.sh [lean-executable-path] [file]" exit 1 fi ulimit -s unlimited -LEANLUA=$1 +LEAN=$1 f=$2 echo "-- testing $f" awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua -if $LEANLUA $f.lua > $f.produced.out; then +if $LEAN $f.lua > $f.produced.out; then echo "-- worked" exit 0 else diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index abd5d2eda7..1b0b7e2b2f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -165,7 +165,6 @@ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINK set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage") set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) add_subdirectory(shell) -add_subdirectory(shell/lua) add_subdirectory(tests/util) add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/interval) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c053b43dc6..976ade4270 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -24,3 +24,29 @@ FOREACH(T ${LEANSLOWTESTS}) WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) ENDFOREACH(T) + +# LEANLUATESTS +file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua") +FOREACH(T ${LEANLUATESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanluatest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) +ENDFOREACH(T) + +# LEANLUADOCS +file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md") +FOREACH(T ${LEANLUADOCS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanluadoc_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua" + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) +ENDFOREACH(T) + +if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux")) + if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) + add_test(NAME leanluathreadtests + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads" + COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") + endif() +endif() diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 372bbbe24f..07cd1aacd6 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -19,10 +19,26 @@ using lean::frontend; using lean::parser; using lean::leanlua_state; +enum class input_kind { Unspecified, Lean, Lua }; + static void on_ctrl_c(int ) { lean::request_interrupt(); } +static char const * get_file_extension(char const * fname) { + if (fname == 0) + return 0; + char const * last_dot = 0; + while (true) { + char const * tmp = strchr(fname, '.'); + if (tmp == 0) { + return last_dot; + } + last_dot = tmp + 1; + fname = last_dot; + } +} + bool lean_shell() { std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n"; std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl; @@ -41,10 +57,33 @@ int main(int argc, char ** argv) { frontend f; leanlua_state S; for (int i = 1; i < argc; i++) { - std::ifstream in(argv[i]); - parser p(f, in, &S, false, false); - if (!p()) - ok = false; + input_kind k = input_kind::Unspecified; + char const * ext = get_file_extension(argv[i]); + if (ext) { + if (strcmp(ext, "lean") == 0) { + k = input_kind::Lean; + } else if (strcmp(ext, "lua") == 0) { + k = input_kind::Lua; + } + } + if (k == input_kind::Unspecified) { + // assume the input is in Lean format + k = input_kind::Lean; + } + + if (k == input_kind::Lean) { + std::ifstream in(argv[i]); + parser p(f, in, &S, false, false); + if (!p()) + ok = false; + } else if (k == input_kind::Lua) { + try { + S.dofile(argv[i]); + } catch (lean::exception & ex) { + std::cerr << ex.what() << std::endl; + ok = false; + } + } } return ok ? 0 : 1; } diff --git a/src/shell/lua/CMakeLists.txt b/src/shell/lua/CMakeLists.txt deleted file mode 100644 index 80db0ace94..0000000000 --- a/src/shell/lua/CMakeLists.txt +++ /dev/null @@ -1,28 +0,0 @@ -add_executable(leanlua leanlua.cpp) -target_link_libraries(leanlua ${EXTRA_LIBS}) - -# LEANLUATESTS -file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua") -FOREACH(T ${LEANLUATESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanluatest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua" ${T}) -ENDFOREACH(T) - -# LEANLUADOCS -file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md") -FOREACH(T ${LEANLUADOCS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanluadoc_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua" ${T}) -ENDFOREACH(T) - -if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux")) - if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) - add_test(NAME leanluathreadtests - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads" - COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua") - endif() -endif() diff --git a/src/shell/lua/leanlua.cpp b/src/shell/lua/leanlua.cpp deleted file mode 100644 index 44438e4504..0000000000 --- a/src/shell/lua/leanlua.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/exception.h" -#include "bindings/lua/leanlua_state.h" - -int main(int argc, char ** argv) { - lean::leanlua_state S; - int exitcode = 0; - - for (int i = 1; i < argc; i++) { - try { - S.dofile(argv[i]); - } catch (lean::exception & ex) { - std::cerr << ex.what() << std::endl; - exitcode = 1; - } - } - return exitcode; -} diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index a246c28c12..e28386c712 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/test.h" #include "util/list.h" #include "util/list_fn.h" diff --git a/tests/lua/test.sh b/tests/lua/test.sh index 97f4540c49..4de60d7adf 100755 --- a/tests/lua/test.sh +++ b/tests/lua/test.sh @@ -1,14 +1,14 @@ #!/bin/bash if [ $# -ne 1 ]; then - echo "Usage: test.sh [leanlua-executable-path]" + echo "Usage: test.sh [lean-executable-path]" exit 1 fi ulimit -s unlimited -LEANLUA=$1 +LEAN=$1 NUM_ERRORS=0 for f in `ls *.lua`; do echo "-- testing $f" - if $LEANLUA util.lua $f > $f.produced.out; then + if $LEAN util.lua $f > $f.produced.out; then echo "-- worked" else echo "ERROR executing $f, produced output is at $f.produced.out" diff --git a/tests/lua/test_single.sh b/tests/lua/test_single.sh index ba05e3e031..66f12f0771 100755 --- a/tests/lua/test_single.sh +++ b/tests/lua/test_single.sh @@ -1,13 +1,13 @@ #!/bin/bash if [ $# -ne 2 ]; then - echo "Usage: test.sh [leanlua-executable-path] [file]" + echo "Usage: test.sh [lean-executable-path] [file]" exit 1 fi ulimit -s unlimited -LEANLUA=$1 +LEAN=$1 f=$2 echo "-- testing $f" -if $LEANLUA util.lua $f > $f.produced.out; then +if $LEAN util.lua $f > $f.produced.out; then echo "-- worked" exit 0 else