From 2a59beee0a73fa57d79915b9dbcbd2434950346a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Apr 2014 17:49:23 -0700 Subject: [PATCH] feat(shell): reactivate lean shell, only Lua frontend is working Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 +- src/shell/CMakeLists.txt | 210 +++++++++++++++++++-------------------- src/shell/lean.cpp | 86 +++++++++------- 3 files changed, 154 insertions(+), 144 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9894d2dae..d5ba45549 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -238,7 +238,7 @@ else() endif() 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) # add_subdirectory(builtin) # add_subdirectory(emacs) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 1a136bd21..672733f45 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -3,119 +3,119 @@ target_link_libraries(lean ${EXTRA_LIBS}) install(TARGETS lean DESTINATION bin) -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_path1 ${CMAKE_CURRENT_BINARY_DIR}/lean -p) -add_test(lean_path2 ${CMAKE_CURRENT_BINARY_DIR}/lean --path) -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") -add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") -add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua") +# 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_path1 ${CMAKE_CURRENT_BINARY_DIR}/lean -p) +# add_test(lean_path2 ${CMAKE_CURRENT_BINARY_DIR}/lean --path) +# 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") +# add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") +# add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua") -# LEAN EXAMPLES -file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean") -FOREACH(T ${LEANEXAMPLES}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanex_${T_NAME}" - COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T}) -ENDFOREACH(T) +# # LEAN EXAMPLES +# file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/lean/*.lean") +# FOREACH(T ${LEANEXAMPLES}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leanex_${T_NAME}" +# COMMAND ${CMAKE_CURRENT_BINARY_DIR}/lean ${T}) +# ENDFOREACH(T) -# LEAN TESTS -file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") -FOREACH(T ${LEANTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leantest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) -ENDFOREACH(T) +# # LEAN TESTS +# file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") +# FOREACH(T ${LEANTESTS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leantest_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" +# COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) +# ENDFOREACH(T) -# LEAN PP TESTS -# For making sure that Lean can parse the output produced by its pretty printer -file(GLOB LEANPPTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") -FOREACH(T ${LEANPPTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanpptest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND "./test_single_pp.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) -ENDFOREACH(T) +# # LEAN PP TESTS +# # For making sure that Lean can parse the output produced by its pretty printer +# file(GLOB LEANPPTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") +# FOREACH(T ${LEANPPTESTS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leanpptest_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" +# COMMAND "./test_single_pp.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) +# ENDFOREACH(T) -# LEAN INTERACTIVE TESTS -file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean") -FOREACH(T ${LEANINTERACTIVETESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leaninteractivetest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) -ENDFOREACH(T) +# # LEAN INTERACTIVE TESTS +# file(GLOB LEANINTERACTIVETESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean") +# FOREACH(T ${LEANINTERACTIVETESTS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leaninteractivetest_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" +# COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) +# ENDFOREACH(T) -# LEAN SLOW TESTS -file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean") -FOREACH(T ${LEANSLOWTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanslowtest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" - COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) -ENDFOREACH(T) +# # LEAN SLOW TESTS +# file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean") +# FOREACH(T ${LEANSLOWTESTS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leanslowtest_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow" +# COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME}) +# ENDFOREACH(T) -# LEAN LUA TESTS -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" ${T_NAME}) -ENDFOREACH(T) +# # LEAN LUA TESTS +# 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" ${T_NAME}) +# ENDFOREACH(T) -# LEAN DOCS -file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md") -FOREACH(T ${LEANDOCS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leandoc_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean" - COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) -ENDFOREACH(T) +# # LEAN DOCS +# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md") +# FOREACH(T ${LEANDOCS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leandoc_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean" +# COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) +# ENDFOREACH(T) -# LEAN LUA DOCS -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" ${T}) -ENDFOREACH(T) +# # LEAN LUA DOCS +# 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" ${T}) +# ENDFOREACH(T) -# LEAN LUA THREAD TESTS -if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux")) - if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${MULTI_THREAD} MATCHES "ON")) - file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua") - FOREACH(T ${LEANLUATHREADTESTS}) - GET_FILENAME_COMPONENT(T_NAME ${T} NAME) - add_test(NAME "leanluathreadtest_${T_NAME}" - WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads" - COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) - ENDFOREACH(T) - endif() -endif() +# # LEAN LUA THREAD TESTS +# if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux")) +# if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${MULTI_THREAD} MATCHES "ON")) +# file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua") +# FOREACH(T ${LEANLUATHREADTESTS}) +# GET_FILENAME_COMPONENT(T_NAME ${T} NAME) +# add_test(NAME "leanluathreadtest_${T_NAME}" +# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads" +# COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T}) +# ENDFOREACH(T) +# endif() +# endif() -# Create the script lean.sh -# This is used to create a soft dependency on the Lean executable -# Some rules can only be applied if the lean executable exists, -# but we don't want a dependency on the executable because -# the rules would be applied whenever the executable is rebuilt. -# These are the rules for automatically generating .olean files and -# C++/Lean interface files. -add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lean.sh - COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/mk_lean_sh.sh ${CMAKE_CURRENT_BINARY_DIR} - DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean) -add_custom_target(lean_sh DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean.sh) +# # Create the script lean.sh +# # This is used to create a soft dependency on the Lean executable +# # Some rules can only be applied if the lean executable exists, +# # but we don't want a dependency on the executable because +# # the rules would be applied whenever the executable is rebuilt. +# # These are the rules for automatically generating .olean files and +# # C++/Lean interface files. +# add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/lean.sh +# COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/mk_lean_sh.sh ${CMAKE_CURRENT_BINARY_DIR} +# DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean) +# add_custom_target(lean_sh DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/lean.sh) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 9be435508..f2e5e4bf6 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/kernel_exception.h" #include "kernel/formatter.h" +#if 0 #include "kernel/io_state.h" #include "library/printer.h" #include "library/kernel_bindings.h" @@ -29,17 +30,21 @@ Author: Leonardo de Moura #include "frontends/lean/frontend.h" #include "frontends/lean/register_module.h" #include "frontends/lua/register_modules.h" +#endif #include "version.h" #include "githash.h" // NOLINT -using lean::shell; -using lean::parser; using lean::script_state; using lean::unreachable_reached; + +#if 0 +using lean::shell; +using lean::parser; using lean::invoke_debugger; using lean::notify_assertion_violation; using lean::environment; using lean::io_state; +#endif enum class input_kind { Unspecified, Lean, OLean, Lua }; @@ -110,11 +115,11 @@ static struct option g_long_options[] = { int main(int argc, char ** argv) { lean::save_stack_info(); - lean::register_modules(); - bool no_kernel = false; - bool export_objects = false; - bool trust_imported = false; - bool quiet = false; + // lean::register_modules(); + // bool no_kernel = false; + // bool export_objects = false; + // bool trust_imported = false; + // bool quiet = false; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { @@ -150,18 +155,18 @@ int main(int argc, char ** argv) { lean::set_thread_stack_size(atoi(optarg)*1024); break; case 'n': - no_kernel = true; + // no_kernel = true; break; case 'o': output = optarg; - export_objects = true; + // export_objects = true; break; case 't': - trust_imported = true; - lean::set_default_trust_imported_for_lua(true); + // trust_imported = true; + // lean::set_default_trust_imported_for_lua(true); break; case 'q': - quiet = true; + // quiet = true; break; default: std::cerr << "Unknown command line option\n"; @@ -169,16 +174,20 @@ int main(int argc, char ** argv) { return 1; } } - environment env; - env->set_trusted_imported(trust_imported); - io_state ios = init_frontend(env, no_kernel); - if (quiet) - ios.set_option("verbose", false); + + // environment env; + // env->set_trusted_imported(trust_imported); + // io_state ios = init_frontend(env, no_kernel); + // if (quiet) + // ios.set_option("verbose", false); + script_state S; - S.apply([&](lua_State * L) { - set_global_environment(L, env); - set_global_io_state(L, ios); - }); + + // S.apply([&](lua_State * L) { + // set_global_environment(L, env); + // set_global_io_state(L, ios); + // }); + try { if (optind >= argc) { display_header(std::cout); @@ -189,11 +198,12 @@ int main(int argc, char ** argv) { #else std::cout << "Type Ctrl-D or 'exit.' to exit or 'help.' for help."<< std::endl; #endif - shell sh(env, &S); - int status = sh() ? 0 : 1; - if (export_objects) - env->export_objects(output); - return status; + // shell sh(env, &S); + // int status = sh() ? 0 : 1; + // if (export_objects) + // env->export_objects(output); + // return status; + return 0; } else { lean_assert(default_k == input_kind::Lua); S.import("repl"); @@ -214,32 +224,32 @@ int main(int argc, char ** argv) { } } if (k == input_kind::Lean) { - if (!parse_commands(env, ios, argv[i], &S, false, false)) - ok = false; + // if (!parse_commands(env, ios, argv[i], &S, false, false)) + // ok = false; } else if (k == input_kind::OLean) { - try { - env->load(std::string(argv[i]), ios); - } catch (lean::exception & ex) { - std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n"; - ok = false; - } + // try { + // env->load(std::string(argv[i]), ios); + // } catch (lean::exception & ex) { + // std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n"; + // ok = false; + // } } else if (k == input_kind::Lua) { try { S.dofile(argv[i]); } catch (lean::exception & ex) { - ::lean::display_error(ios, nullptr, ex); + // ::lean::display_error(ios, nullptr, ex); ok = false; } } else { lean_unreachable(); // LCOV_EXCL_LINE } } - if (export_objects) - env->export_objects(output); + // if (export_objects) + // env->export_objects(output); return ok ? 0 : 1; } } catch (lean::exception & ex) { - ::lean::display_error(ios, nullptr, ex); + // ::lean::display_error(ios, nullptr, ex); } return 1; }