feat(frontends/lean/server): add 'OPTIONS' command to 'lean --server'

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

doc/server.org

@@ -258,3 +258,30 @@ until all pending information has been computed.
 #+BEGIN_SRC
 WAIT
 #+END_SRC
+
+** Options
+
+The command =OPTIONS= display all configuration options available
+in Lean. It has the form
+
+#+BEGIN_SRC
+OPTIONS
+#+END_SRC
+
+The output is a sequence of entries
+
+#+BEGIN_SRC
+-- BEGINOPTIONS
+[entry]*
+-- ENDOPTIONS
+#+END_SRC
+
+where each entry is of the form
+
+#+BEGIN_SRC
+-- [name]|[kind]|[default-value]|[description]
+#+END_SRC
+
+The available =kinds= are: =Bool=, =Int=, =Unsigned Int=, =Double=,
+=String=, and =S-Expressions=.
+

src/frontends/lean/pp_options.cpp

@@ -7,11 +7,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp_options.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
-#define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
+#define LEAN_DEFAULT_PP_MAX_DEPTH 1000000
 #endif
 
 #ifndef LEAN_DEFAULT_PP_MAX_STEPS
-#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits<unsigned>::max()
+#define LEAN_DEFAULT_PP_MAX_STEPS 10000000
 #endif
 
 #ifndef LEAN_DEFAULT_PP_NOTATION

src/frontends/lean/server.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <functional>
 #include "util/sstream.h"
+#include "util/sexpr/option_declarations.h"
 #include "frontends/lean/server.h"
 #include "frontends/lean/parser.h"
 
@@ -214,6 +215,7 @@ static std::string g_eval("EVAL");
 static std::string g_wait("WAIT");
 static std::string g_clear_cache("CLEAR_CACHE");
 static std::string g_echo("ECHO");
+static std::string g_options("OPTIONS");
 
 static bool is_command(std::string const & cmd, std::string const & line) {
     return line.compare(0, cmd.size(), cmd) == 0;
@@ -346,6 +348,16 @@ void server::eval(std::string const & line) {
     }
 }
 
+void server::show_options() {
+    m_out << "-- BEGINOPTIONS" << std::endl;
+    option_declarations const & decls = get_option_declarations();
+    for (auto it = decls.begin(); it != decls.end(); it++) {
+        option_declaration const & d = it->second;
+        m_out << "-- " << d.get_name() << "|" << d.kind() << "|" << d.get_default_value() << "|" << d.get_description() << "\n";
+    }
+    m_out << "-- ENDOPTIONS" << std::endl;
+}
+
 bool server::operator()(std::istream & in) {
     for (std::string line; std::getline(in, line);) {
         try {
@@ -382,6 +394,8 @@ bool server::operator()(std::istream & in) {
                 eval(line);
             } else if (is_command(g_clear_cache, line)) {
                 m_cache.clear();
+            } else if (is_command(g_options, line)) {
+                show_options();
             } else if (is_command(g_wait, line)) {
                 m_worker.wait();
             } else {

src/frontends/lean/server.h

@@ -83,6 +83,7 @@ class server {
     unsigned find(unsigned linenum);
     void read_line(std::istream & in, std::string & line);
     void interrupt_worker();
+    void show_options();
     unsigned get_linenum(std::string const & line, std::string const & cmd);
 
 public: