refactor(shell): combine lean and leanlua executables in a single executable

The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

doc/lua/test.sh

@@ -1,16 +1,16 @@
 #!/bin/sh
 # Test is all examples in the .md files are working
 if [ $# -ne 1 ]; then
-    echo "Usage: test.sh [leanlua-executable-path]"
+    echo "Usage: test.sh [lean-executable-path]"
     exit 1
 fi
 ulimit -s unlimited
-LEANLUA=$1
+LEAN=$1
 NUM_ERRORS=0
 for f in `ls *.md`; do
     echo "-- testing $f"
     awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua
-    if $LEANLUA $f.lua > $f.produced.out; then
+    if $LEAN $f.lua > $f.produced.out; then
         echo "-- worked"
     else
         echo "ERROR executing $f.lua, produced output is at $f.produced.out"

doc/lua/test_single.sh

@@ -1,15 +1,15 @@
 #!/bin/sh
 # Test is all examples in the .md files are working
 if [ $# -ne 2 ]; then
-    echo "Usage: test.sh [leanlua-executable-path] [file]"
+    echo "Usage: test.sh [lean-executable-path] [file]"
     exit 1
 fi
 ulimit -s unlimited
-LEANLUA=$1
+LEAN=$1
 f=$2
 echo "-- testing $f"
 awk 'BEGIN{ in_block = 0 } !/```/{ if (in_block == 1) print $0; else print "" } /```/ && !/```lua/{ in_block = 0; print "" } /```lua/{ in_block = 1; print "" }' $f > $f.lua
-if $LEANLUA $f.lua > $f.produced.out; then
+if $LEAN $f.lua > $f.produced.out; then
     echo "-- worked"
     exit 0
 else

src/CMakeLists.txt

@@ -165,7 +165,6 @@ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINK
 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/lua)
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/util/interval)

src/shell/CMakeLists.txt

@@ -24,3 +24,29 @@ FOREACH(T ${LEANSLOWTESTS})
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/slow"
            COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
 ENDFOREACH(T)
+
+# LEANLUATESTS
+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})
+ENDFOREACH(T)
+
+# LEANLUADOCS
+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})
+ENDFOREACH(T)
+
+if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
+  if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang"))
+    add_test(NAME leanluathreadtests
+      WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads"
+      COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+  endif()
+endif()

src/shell/lean.cpp

@@ -19,10 +19,26 @@ using lean::frontend;
 using lean::parser;
 using lean::leanlua_state;
 
+enum class input_kind { Unspecified, Lean, Lua };
+
 static void on_ctrl_c(int ) {
     lean::request_interrupt();
 }
 
+static char const * get_file_extension(char const * fname) {
+    if (fname == 0)
+        return 0;
+    char const * last_dot = 0;
+    while (true) {
+        char const * tmp = strchr(fname, '.');
+        if (tmp == 0) {
+            return last_dot;
+        }
+        last_dot  = tmp + 1;
+        fname = last_dot;
+    }
+}
+
 bool lean_shell() {
     std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
     std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
@@ -41,10 +57,33 @@ int main(int argc, char ** argv) {
         frontend f;
         leanlua_state S;
         for (int i = 1; i < argc; i++) {
-            std::ifstream in(argv[i]);
-            parser p(f, in, &S, false, false);
-            if (!p())
-                ok = false;
+            input_kind k = input_kind::Unspecified;
+            char const * ext = get_file_extension(argv[i]);
+            if (ext) {
+                if (strcmp(ext, "lean") == 0) {
+                    k = input_kind::Lean;
+                } else if (strcmp(ext, "lua") == 0) {
+                    k = input_kind::Lua;
+                }
+            }
+            if (k == input_kind::Unspecified) {
+                // assume the input is in Lean format
+                k = input_kind::Lean;
+            }
+
+            if (k == input_kind::Lean) {
+                std::ifstream in(argv[i]);
+                parser p(f, in, &S, false, false);
+                if (!p())
+                    ok = false;
+            } else if (k == input_kind::Lua) {
+                try {
+                    S.dofile(argv[i]);
+                } catch (lean::exception & ex) {
+                    std::cerr << ex.what() << std::endl;
+                    ok = false;
+                }
+            }
         }
         return ok ? 0 : 1;
     }

src/shell/lua/CMakeLists.txt

@@ -1,28 +0,0 @@
-add_executable(leanlua leanlua.cpp)
-target_link_libraries(leanlua ${EXTRA_LIBS})
-
-# LEANLUATESTS
-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}/leanlua" ${T})
-ENDFOREACH(T)
-
-# LEANLUADOCS
-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}/leanlua" ${T})
-ENDFOREACH(T)
-
-if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
-  if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang"))
-    add_test(NAME leanluathreadtests
-      WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads"
-      COMMAND "../test.sh" "${CMAKE_CURRENT_BINARY_DIR}/leanlua")
-  endif()
-endif()

src/shell/lua/leanlua.cpp

@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <iostream>
-#include "util/exception.h"
-#include "bindings/lua/leanlua_state.h"
-
-int main(int argc, char ** argv) {
-    lean::leanlua_state S;
-    int exitcode = 0;
-
-    for (int i = 1; i < argc; i++) {
-        try {
-            S.dofile(argv[i]);
-        } catch (lean::exception & ex) {
-            std::cerr << ex.what() << std::endl;
-            exitcode = 1;
-        }
-    }
-    return exitcode;
-}

src/tests/util/list.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include <utility>
 #include "util/test.h"
 #include "util/list.h"
 #include "util/list_fn.h"

tests/lua/test.sh

@@ -1,14 +1,14 @@
 #!/bin/bash
 if [ $# -ne 1 ]; then
-    echo "Usage: test.sh [leanlua-executable-path]"
+    echo "Usage: test.sh [lean-executable-path]"
     exit 1
 fi
 ulimit -s unlimited
-LEANLUA=$1
+LEAN=$1
 NUM_ERRORS=0
 for f in `ls *.lua`; do
     echo "-- testing $f"
-    if $LEANLUA util.lua $f > $f.produced.out; then
+    if $LEAN util.lua $f > $f.produced.out; then
         echo "-- worked"
     else
         echo "ERROR executing $f, produced output is at $f.produced.out"

tests/lua/test_single.sh

@@ -1,13 +1,13 @@
 #!/bin/bash
 if [ $# -ne 2 ]; then
-    echo "Usage: test.sh [leanlua-executable-path] [file]"
+    echo "Usage: test.sh [lean-executable-path] [file]"
     exit 1
 fi
 ulimit -s unlimited
-LEANLUA=$1
+LEAN=$1
 f=$2
 echo "-- testing $f"
-if $LEANLUA util.lua $f > $f.produced.out; then
+if $LEAN util.lua $f > $f.produced.out; then
     echo "-- worked"
     exit 0
 else