From c8b0c10c88eb3ace0ec5ec15adca853b8d1ea0a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 Nov 2013 10:56:29 -0800
Subject: [PATCH] refactor(lua): make Lua a required (non-optional) package

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                 | 21 ++++++++-------------
 src/bindings/lua/expr.cpp          |  2 --
 src/bindings/lua/expr.h            |  2 --
 src/bindings/lua/format.cpp        |  2 --
 src/bindings/lua/format.h          |  2 --
 src/bindings/lua/leanlua_state.cpp | 27 +--------------------------
 src/bindings/lua/name.cpp          |  2 --
 src/bindings/lua/name.h            |  2 --
 src/bindings/lua/numerics.cpp      |  2 --
 src/bindings/lua/numerics.h        |  2 --
 src/bindings/lua/options.cpp       |  2 --
 src/bindings/lua/options.h         |  2 --
 src/bindings/lua/sexpr.cpp         |  2 --
 src/bindings/lua/sexpr.h           |  2 --
 src/bindings/lua/util.cpp          |  2 --
 src/bindings/lua/util.h            |  2 --
 16 files changed, 9 insertions(+), 67 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c3eb8a8e66..796aa6cfcd 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -121,19 +121,14 @@ if(NOT "${TCMALLOC_FOUND}" AND "${TRACK_MEMORY_USAGE}" MATCHES "ON")
   endif()
 endif()
 
-find_package(Lua)
-if ("${LUA_FOUND}" MATCHES "TRUE")
-  message(STATUS "Using Lua script language")
-  set(EXTRA_LIBS ${EXTRA_LIBS} ${LUA_LIBRARIES})
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${LUA_INCLUDE_DIR} -D LEAN_USE_LUA")
-  if ("${HAS_LUA_NEWSTATE}$" MATCHES "TRUE")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_NEWSTATE")
-  endif()
-  if ("${HAS_LUA_OBJLEN}$" MATCHES "TRUE")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_OBJLEN")
-  endif()
-else()
-    message(WARNING "FAILED to find Lua script language, it will not be available")
+find_package(Lua REQUIRED)
+set(EXTRA_LIBS ${EXTRA_LIBS} ${LUA_LIBRARIES})
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${LUA_INCLUDE_DIR}")
+if ("${HAS_LUA_NEWSTATE}$" MATCHES "TRUE")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_NEWSTATE")
+endif()
+if ("${HAS_LUA_OBJLEN}$" MATCHES "TRUE")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_OBJLEN")
 endif()
 
 include_directories(${LEAN_SOURCE_DIR})
diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp
index 87f80a3cf5..04c3609cc2 100644
--- a/src/bindings/lua/expr.cpp
+++ b/src/bindings/lua/expr.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <sstream>
 #include <lua.hpp>
 #include <utility>
@@ -210,4 +209,3 @@ void open_expr(lua_State * L) {
     set_global_function<expr_pi>(L, "Pi");
 }
 }
-#endif
diff --git a/src/bindings/lua/expr.h b/src/bindings/lua/expr.h
index e627a93423..7173a5fd4c 100644
--- a/src/bindings/lua/expr.h
+++ b/src/bindings/lua/expr.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class expr;
@@ -13,4 +12,3 @@ bool is_expr(lua_State * L, int idx);
 expr & to_expr(lua_State * L, int idx);
 int push_expr(lua_State * L, expr const & o);
 }
-#endif
diff --git a/src/bindings/lua/format.cpp b/src/bindings/lua/format.cpp
index f1869bd5fa..4b692b4637 100644
--- a/src/bindings/lua/format.cpp
+++ b/src/bindings/lua/format.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <sstream>
 #include <lua.hpp>
 #include <cstring>
@@ -133,4 +132,3 @@ void open_format(lua_State * L) {
     set_global_function<format_space>(L, "space");
 }
 }
-#endif
diff --git a/src/bindings/lua/format.h b/src/bindings/lua/format.h
index f93dd5eac6..6cb36258c1 100644
--- a/src/bindings/lua/format.h
+++ b/src/bindings/lua/format.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class format;
@@ -13,4 +12,3 @@ bool is_format(lua_State * L, int idx);
 format & to_format(lua_State * L, int idx);
 int push_format(lua_State * L, format const & o);
 }
-#endif
diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp
index c99c70ab3e..06ed099b1c 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/bindings/lua/leanlua_state.cpp
@@ -8,13 +8,11 @@ Author: Leonardo de Moura
 #include <sstream>
 #include <mutex>
 #include <string>
+#include <lua.hpp>
 #include "util/debug.h"
 #include "util/exception.h"
 #include "util/memory.h"
 #include "bindings/lua/leanlua_state.h"
-
-#ifdef LEAN_USE_LUA
-#include <lua.hpp>
 #include "bindings/lua/name.h"
 #include "bindings/lua/numerics.h"
 #include "bindings/lua/options.h"
@@ -88,30 +86,7 @@ void leanlua_state::dofile(char const * fname) {
 void leanlua_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
-}
-#else
-namespace lean {
-leanlua_state::leanlua_state() {
-}
 
-leanlua_state::~leanlua_state() {
-}
-
-[[ noreturn ]] void throw_lua_not_supported() {
-    throw exception("Lean was compiled without Lua support");
-}
-
-void leanlua_state::dofile(char const * fname) {
-    throw_lua_not_supported();
-}
-
-void leanlua_state::dostring(char const * str) {
-    throw_lua_not_supported();
-}
-}
-#endif
-
-namespace lean {
 lua_exception::lua_exception(char const * lua_error):exception("") {
     lean_assert(lua_error);
     std::string fname;
diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp
index 07b4b38cc2..70cec2bdd9 100644
--- a/src/bindings/lua/name.cpp
+++ b/src/bindings/lua/name.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 #include "util/debug.h"
 #include "util/name.h"
@@ -88,4 +87,3 @@ void open_name(lua_State * L) {
     set_global_function<mk_name>(L, "name");
 }
 }
-#endif
diff --git a/src/bindings/lua/name.h b/src/bindings/lua/name.h
index c87b5c3e0c..72ef3aeab7 100644
--- a/src/bindings/lua/name.h
+++ b/src/bindings/lua/name.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class name;
@@ -14,4 +13,3 @@ name & to_name(lua_State * L, int idx);
 name to_name_ext(lua_State * L, int idx);
 int push_name(lua_State * L, name const & n);
 }
-#endif
diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp
index 83fed4c23a..7296ee6895 100644
--- a/src/bindings/lua/numerics.cpp
+++ b/src/bindings/lua/numerics.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <sstream>
 #include <lua.hpp>
 #include "util/debug.h"
@@ -235,4 +234,3 @@ void open_mpq(lua_State * L) {
     set_global_function<mk_mpq>(L, "mpq");
 }
 }
-#endif
diff --git a/src/bindings/lua/numerics.h b/src/bindings/lua/numerics.h
index 9dda2ade0f..c6744b03d2 100644
--- a/src/bindings/lua/numerics.h
+++ b/src/bindings/lua/numerics.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class mpz;
@@ -19,4 +18,3 @@ bool is_mpq(lua_State * L, int idx);
 mpq & to_mpq(lua_State * L, int idx);
 int push_mpq(lua_State * L, mpq const & val);
 }
-#endif
diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp
index 4020036864..25fb93d3e8 100644
--- a/src/bindings/lua/options.cpp
+++ b/src/bindings/lua/options.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <sstream>
 #include <lua.hpp>
 #include "util/debug.h"
@@ -198,4 +197,3 @@ void open_options(lua_State * L) {
     set_global_function<mk_option>(L, "options");
 }
 }
-#endif
diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h
index 81333a6a62..3441805fa5 100644
--- a/src/bindings/lua/options.h
+++ b/src/bindings/lua/options.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class options;
@@ -13,4 +12,3 @@ bool is_options(lua_State * L, int idx);
 options & to_options(lua_State * L, int idx);
 int push_options(lua_State * L, options const & o);
 }
-#endif
diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp
index 454edd983b..e3da2304e2 100644
--- a/src/bindings/lua/sexpr.cpp
+++ b/src/bindings/lua/sexpr.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <sstream>
 #include <lua.hpp>
 #include "util/debug.h"
@@ -208,4 +207,3 @@ void open_sexpr(lua_State * L) {
     set_global_function<mk_sexpr>(L, "sexpr");
 }
 }
-#endif
diff --git a/src/bindings/lua/sexpr.h b/src/bindings/lua/sexpr.h
index 40c11efacc..fab2e197ac 100644
--- a/src/bindings/lua/sexpr.h
+++ b/src/bindings/lua/sexpr.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 class sexpr;
@@ -13,4 +12,3 @@ bool is_sexpr(lua_State * L, int idx);
 sexpr & to_sexpr(lua_State * L, int idx);
 int push_sexpr(lua_State * L, sexpr const & e);
 }
-#endif
diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp
index 1af8b657a7..e7be0af803 100644
--- a/src/bindings/lua/util.cpp
+++ b/src/bindings/lua/util.cpp
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 #include <exception>
 #include <string>
@@ -71,4 +70,3 @@ int safe_function_wrapper(lua_State * L, lua_CFunction f){
     return luaL_error(L, error_msg);
 }
 }
-#endif
diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h
index e4fdbf0814..4be0cbcc33 100644
--- a/src/bindings/lua/util.h
+++ b/src/bindings/lua/util.h
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#ifdef LEAN_USE_LUA
 #include <lua.hpp>
 namespace lean {
 void setfuncs(lua_State * L, luaL_Reg const * l, int nup);
@@ -22,4 +21,3 @@ template<lua_CFunction F> void set_global_function(lua_State * L, char const * n
     lua_setglobal(L, name);
 }
 }
-#endif