feat(shell): reactivate lean shell, only Lua frontend is working
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
cdae3ee780
commit
2a59beee0a
3 changed files with 154 additions and 144 deletions
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue