feat(frontends/lean/server): use separate thread for processing requests in server mode, interrupt whole parser when on interruption (when collecting information)

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

src/frontends/lean/parser.cpp

@@ -220,7 +220,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
         if (m_verbose)
             regular_stream() << "!!!Interrupted!!!" << endl;
         sync();
-        if (m_use_exceptions)
+        if (m_use_exceptions || m_info_manager)
             throw;
     } catch (script_exception & ex) {
         reset_interrupt();

src/frontends/lean/parser.h

@@ -96,7 +96,7 @@ class parser {
     // cache support
     definition_cache *     m_cache;
     // index support
-    declaration_index *     m_index;
+    declaration_index *    m_index;
 
     void display_warning_pos(unsigned line, unsigned pos);
     void display_warning_pos(pos_info p);

src/frontends/lean/server.cpp

@@ -11,14 +11,12 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 
 namespace lean {
-server::file::file(std::string const & fname):m_fname(fname), m_from(0) {}
+server::file::file(std::string const & fname):m_fname(fname) {}
 
 void server::file::replace_line(unsigned linenum, std::string const & new_line) {
     while (linenum >= m_lines.size())
         m_lines.push_back("");
     m_lines[linenum] = new_line;
-    if (linenum < m_from)
-        m_from = linenum;
 }
 
 void server::file::insert_line(unsigned linenum, std::string const & new_line) {
@@ -32,8 +30,6 @@ void server::file::insert_line(unsigned linenum, std::string const & new_line) {
         m_lines[i] = m_lines[i-1];
     }
     m_lines[linenum] = new_line;
-    if (linenum < m_from)
-        m_from = linenum;
 }
 
 void server::file::remove_line(unsigned linenum) {
@@ -43,8 +39,6 @@ void server::file::remove_line(unsigned linenum) {
     for (unsigned i = linenum; i < m_lines.size()-1; i++)
         m_lines[i] = m_lines[i+1];
     m_lines.pop_back();
-    if (linenum < m_from)
-        m_from = linenum;
 }
 
 /**
@@ -74,6 +68,25 @@ unsigned server::file::find(unsigned linenum) {
 server::server(environment const & env, io_state const & ios, unsigned num_threads):
     m_env(env), m_ios(ios), m_out(ios.get_regular_channel().get_stream()),
     m_num_threads(num_threads), m_empty_snapshot(m_env, m_ios.get_options()) {
+    m_thread_busy = false;
+}
+
+server::~server() {
+    reset_thread();
+}
+
+void server::interrupt_thread() {
+    if (m_thread_ptr)
+        m_thread_ptr->request_interrupt();
+}
+
+void server::reset_thread() {
+    if (m_thread_ptr) {
+        m_thread_ptr->request_interrupt();
+        m_thread_ptr->join();
+        m_thread_ptr.reset(nullptr);
+    }
+    m_thread_busy = false;
 }
 
 static std::string g_load("LOAD");
@@ -118,6 +131,7 @@ public:
 };
 
 void server::process_from(unsigned linenum) {
+    reset_thread();
     unsigned i = m_file->find(linenum);
     m_file->m_snapshots.resize(i);
     snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
@@ -128,53 +142,48 @@ void server::process_from(unsigned linenum) {
         block += m_file->m_lines[j];
         block += '\n';
     }
-    std::istringstream strm(block);
-    scoped_updt_options updt(m_ios, s.m_options);
-    parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
-             &m_file->m_snapshots, &m_file->m_info);
     // p.set_cache(&m_cache);
-    p();
+    m_thread_busy = true;
-}
+    m_thread_ptr.reset(new interruptible_thread([=]() {
-
+                try {
-void server::update() {
+                    snapshot & s = i == 0 ? m_empty_snapshot : m_file->m_snapshots[i-1];
-    if (m_file->m_from == m_file->m_lines.size())
+                    std::istringstream strm(block);
-        return;
+                    scoped_updt_options updt(m_ios, s.m_options);
-    process_from(m_file->m_from);
+                    parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
-    m_file->m_from = m_file->m_lines.size();
+                             &m_file->m_snapshots, &m_file->m_info);
+                    p();
+                    m_thread_busy  = false;
+                    std::cout << "DONE\n";
+                } catch (exception& ex) {}
+            }));
 }
 
 void server::load_file(std::string const & fname) {
+    interrupt_thread();
     std::ifstream in(fname);
     if (in.bad() || in.fail()) {
         m_out << "-- ERROR failed to open file '" << fname << "'" << std::endl;
     } else {
+        reset_thread();
         m_file.reset(new file(fname));
         m_file_map.insert(mk_pair(fname, m_file));
         for (std::string line; std::getline(in, line);) {
             m_file->m_lines.push_back(line);
         }
+        process_from(0);
     }
 }
 
 void server::visit_file(std::string const & fname) {
+    interrupt_thread();
     auto it = m_file_map.find(fname);
-    if (it == m_file_map.end())
+    if (it == m_file_map.end()) {
         load_file(fname);
-    else
+    } else {
+        reset_thread();
         m_file = it->second;
-}
+        process_from(0);
-
+    }
-void server::show_info(unsigned linenum) {
-    check_file();
-    update();
-    unsigned i = m_file->find(linenum);
-    environment const & env = i == 0 ? m_env               : m_file->m_snapshots[i-1].m_env;
-    options const & o       = i == 0 ? m_ios.get_options() : m_file->m_snapshots[i-1].m_options;
-    scoped_updt_options updt(m_ios, o);
-    io_state_stream out(env, m_ios);
-    out << "-- BEGININFO" << endl;
-    m_file->m_info.display(out, linenum);
-    out << "-- ENDINFO" << endl;
 }
 
 void server::read_line(std::istream & in, std::string & line) {
@@ -198,18 +207,24 @@ void server::check_file() {
 }
 
 void server::replace_line(unsigned linenum, std::string const & new_line) {
+    interrupt_thread();
     check_file();
     m_file->replace_line(linenum, new_line);
+    process_from(linenum);
 }
 
 void server::insert_line(unsigned linenum, std::string const & new_line) {
+    interrupt_thread();
     check_file();
     m_file->insert_line(linenum, new_line);
+    process_from(linenum);
 }
 
 void server::remove_line(unsigned linenum) {
+    interrupt_thread();
     check_file();
     m_file->remove_line(linenum);
+    process_from(linenum);
 }
 
 void server::check_line(unsigned linenum, std::string const & line) {
@@ -238,9 +253,27 @@ void server::set_option(std::string const & line) {
     m_out << "-- ENDSET" << std::endl;
 }
 
+void server::show_info(unsigned linenum) {
+    if (m_thread_busy) {
+        m_out << "-- BEGININFO\n-- NAY\n-- ENDINFO" << std::endl;
+        return;
+    }
+    check_file();
+    unsigned i = m_file->find(linenum);
+    environment const & env = i == 0 ? m_env               : m_file->m_snapshots[i-1].m_env;
+    options const & o       = i == 0 ? m_ios.get_options() : m_file->m_snapshots[i-1].m_options;
+    scoped_updt_options updt(m_ios, o);
+    io_state_stream out(env, m_ios);
+    out << "-- BEGININFO" << endl;
+    m_file->m_info.display(out, linenum);
+    out << "-- ENDINFO" << endl;
+}
+
 void server::eval(std::string const & line) {
-    if (m_file)
+    if (m_thread_busy) {
-        update();
+        m_out << "-- BEGINEVAL\n-- NAY\n-- ENDEVAL" << std::endl;
+        return;
+    }
     snapshot & s = !m_file || m_file->m_snapshots.empty() ? m_empty_snapshot : m_file->m_snapshots.back();
     std::istringstream strm(line);
     scoped_updt_options updt(m_ios, s.m_options);

src/frontends/lean/server.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <string>
 #include <unordered_map>
+#include "util/interrupt.h"
 #include "library/definition_cache.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/info_manager.h"
@@ -23,7 +24,6 @@ class server {
         std::vector<std::string>  m_lines;
         snapshot_vector           m_snapshots;
         info_manager              m_info;
-        unsigned                  m_from; // mark the first modified line that was not processed yet.
 
         file(std::string const & fname);
         unsigned find(unsigned linenum);
@@ -41,6 +41,8 @@ class server {
     unsigned                  m_num_threads;
     snapshot                  m_empty_snapshot;
     definition_cache          m_cache;
+    atomic<bool>              m_thread_busy;
+    std::unique_ptr<interruptible_thread> m_thread_ptr;
 
     void load_file(std::string const & fname);
     void visit_file(std::string const & fname);
@@ -54,12 +56,14 @@ class server {
     void set_option(std::string const & line);
     void eval(std::string const & line);
     unsigned find(unsigned linenum);
-    void update();
     void read_line(std::istream & in, std::string & line);
+    void reset_thread();
+    void interrupt_thread();
     unsigned get_linenum(std::string const & line, std::string const & cmd);
 
 public:
     server(environment const & env, io_state const & ios, unsigned num_threads = 1);
+    ~server();
     bool operator()(std::istream & in);
 };
 }