From af927ecb7a8b9bfd960a6b186edef3137e3c4dd5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Apr 2014 17:57:39 -0700
Subject: [PATCH] refactor(frontends/lua): reactivate some of the Lua
 extensions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                     |  4 ++--
 src/frontends/lua/register_modules.cpp | 22 +++++++++++-----------
 src/shell/lean.cpp                     |  4 ++--
 3 files changed, 15 insertions(+), 15 deletions(-)

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;