diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d5ba45549..63b2950ed 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -229,8 +229,8 @@ set(LEAN_LIBS ${LEAN_LIBS} library) # set(LEAN_LIBS ${LEAN_LIBS} error_handling) # add_subdirectory(frontends/lean) # set(LEAN_LIBS ${LEAN_LIBS} lean_frontend) -# add_subdirectory(frontends/lua) -# set(LEAN_LIBS ${LEAN_LIBS} leanlua) +add_subdirectory(frontends/lua) +set(LEAN_LIBS ${LEAN_LIBS} leanlua) if("${MULTI_THREAD}" MATCHES "ON") set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}") else() diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp index cbe60038b..26f00c822 100644 --- a/src/frontends/lua/register_modules.cpp +++ b/src/frontends/lua/register_modules.cpp @@ -7,21 +7,21 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "util/numerics/register_module.h" #include "util/sexpr/register_module.h" -#include "library/register_module.h" -#include "library/io_state_stream.h" -#include "library/arith/register_module.h" -#include "library/simplifier/register_module.h" -#include "library/tactic/register_module.h" -#include "frontends/lean/register_module.h" +// #include "library/register_module.h" +// #include "library/io_state_stream.h" +// #include "library/arith/register_module.h" +// #include "library/simplifier/register_module.h" +// #include "library/tactic/register_module.h" +// #include "frontends/lean/register_module.h" namespace lean { void register_modules() { register_numerics_module(); register_sexpr_module(); - register_core_module(); - register_arith_module(); - register_simplifier_module(); - register_tactic_module(); - register_frontend_lean_module(); + // register_core_module(); + // register_arith_module(); + // register_simplifier_module(); + // register_tactic_module(); + // register_frontend_lean_module(); } } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index f2e5e4bf6..371db206d 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -29,8 +29,8 @@ Author: Leonardo de Moura #include "frontends/lean/shell.h" #include "frontends/lean/frontend.h" #include "frontends/lean/register_module.h" -#include "frontends/lua/register_modules.h" #endif +#include "frontends/lua/register_modules.h" #include "version.h" #include "githash.h" // NOLINT @@ -115,7 +115,7 @@ static struct option g_long_options[] = { int main(int argc, char ** argv) { lean::save_stack_info(); - // lean::register_modules(); + lean::register_modules(); // bool no_kernel = false; // bool export_objects = false; // bool trust_imported = false;