Add support for READLINE. Remark: it is not enabled by default. Rename tcmalloc option to TCMALLOC (using consistent name convention for cmake parameters).

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

src/CMakeLists.txt

@@ -51,15 +51,25 @@ find_package(MPFR 3.1.0)
 set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES})
 
 # tcmalloc
-option(tcmalloc "tcmalloc" ON)
+option(TCMALLOC "TCMALLOC" ON)
-if("${tcmalloc}" MATCHES "ON")
+if("${TCMALLOC}" MATCHES "ON")
   if(${TCMALLOC_FOUND})
     set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
   endif()
+  message(STATUS "Using tcmalloc.")
 else()
   message(STATUS "Using standard malloc.")
 endif()
 
+# Readline
+option(READLINE "READLINE" OFF)
+if("${READLINE}" MATCHES "ON")
+  find_package(Readline)
+  set(EXTRA_LIBS ${EXTRA_LIBS} ${READLINE_LIBRARY})
+  message(STATUS "Using GNU readline")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DLEAN_USE_READLINE")
+endif()
+
 include_directories(${LEAN_SOURCE_DIR}/util)
 include_directories(${LEAN_SOURCE_DIR}/util/numerics)
 include_directories(${LEAN_SOURCE_DIR}/util/sexpr)

src/cmake/Modules/FindReadline.cmake

@@ -0,0 +1,16 @@
+FIND_PATH(READLINE_INCLUDE_DIR readline/readline.h)
+FIND_LIBRARY(READLINE_LIBRARY NAMES readline)
+
+IF (READLINE_INCLUDE_DIR AND READLINE_LIBRARY)
+   SET(READLINE_FOUND TRUE)
+ENDIF (READLINE_INCLUDE_DIR AND READLINE_LIBRARY)
+
+IF (READLINE_FOUND)
+   IF (NOT Readline_FIND_QUIETLY)
+      MESSAGE(STATUS "Found GNU readline: ${READLINE_LIBRARY}")
+   ENDIF (NOT Readline_FIND_QUIETLY)
+ELSE (READLINE_FOUND)
+   IF (Readline_FIND_REQUIRED)
+      MESSAGE(FATAL_ERROR "Could not find GNU readline")
+   ENDIF (Readline_FIND_REQUIRED)
+ENDIF (READLINE_FOUND)

src/frontends/lean/lean_parser.cpp

@@ -20,6 +20,13 @@ Author: Leonardo de Moura
 #include "lean_scanner.h"
 #include "lean_notation.h"
 #include "lean_pp.h"
+#ifdef LEAN_USE_READLINE
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include <readline/readline.h>
+#include <readline/history.h>
+#endif
 
 namespace lean {
 // ==========================================
@@ -1156,12 +1163,30 @@ public:
             throw parser_exception(ex.what(), m_scanner.get_line(), m_scanner.get_pos());
         }
     }
-
 };
 bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions, bool interactive) {
     parser_fn::show_prompt(interactive, fe);
     return parser_fn(fe, in, use_exceptions, interactive).parse_commands();
 }
+bool parse_commands_from_stdin(frontend & fe) {
+#ifdef LEAN_USE_READLINE
+    bool errors = false;
+    char * input;
+    while (true) {
+        input = readline("# ");
+        if (!input)
+            return errors;
+        std::istringstream strm(input);
+        if (parse_commands(fe, strm, false, false))
+            add_history(input);
+        else
+            errors = true;
+        free(input);
+    }
+#else
+    return parse_commands(fe, std::cin, false, true) ? 0 : 1;
+#endif
+}
 expr parse_expr(frontend const & fe, std::istream & in) {
     return parser_fn(const_cast<frontend&>(fe), in, true, false).parse_expr_main();
 }

src/frontends/lean/lean_parser.h

@@ -10,5 +10,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false);
+bool parse_commands_from_stdin(frontend & fe);
 expr parse_expr(frontend const & fe, std::istream & in);
 }

src/shell/lean.cpp

@@ -10,7 +10,7 @@ int main(int argc, char ** argv) {
     std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
     frontend f;
     if (argc == 1) {
-        return parse_commands(f, std::cin, false, true) ? 0 : 1;
+        return parse_commands_from_stdin(f) ? 0 : 1;
     } else {
         bool ok = true;
         for (int i = 1; i < argc; i++) {