fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name

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

src/frontends/lean/info_manager.cpp

@@ -54,7 +54,8 @@ info_manager::info_manager():m_sorted_upto(0) {}
 void info_manager::sort_core() {
     if (m_sorted_upto == m_data.size())
         return;
-    std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end());
+    std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end(),
+                     [](std::unique_ptr<info_data> const & i1, std::unique_ptr<info_data> const & i2) { return *i1 < *i2; });
     m_sorted_upto = m_data.size();
 }
 
@@ -90,6 +91,7 @@ void info_manager::invalidate(unsigned sline) {
     sort_core();
     unsigned i = find(sline, 0);
     m_data.resize(i);
+    if (m_data.size() < m_sorted_upto)
         m_sorted_upto = m_data.size();
 }
 

src/frontends/lean/parser.cpp

@@ -174,6 +174,7 @@ void parser::throw_nested_exception(exception & ex, pos_info p) {
 }
 
 #define CATCH(ShowError, ThrowError)                    \
+save_pre_info_data();                                   \
 m_found_errors = true;                                  \
 if (!m_use_exceptions && m_show_errors) { ShowError ; } \
 sync();                                                 \
@@ -192,6 +193,7 @@ void parser::protected_call(std::function<void()> && f, std::function<void()> &&
         CATCH(display_error(ex.what(), ex.m_pos),
               throw_parser_exception(ex.what(), ex.m_pos));
     } catch (interrupted & ex) {
+        save_pre_info_data();
         reset_interrupt();
         if (m_verbose)
             regular_stream() << "!!!Interrupted!!!" << endl;
@@ -1165,6 +1167,7 @@ bool parser::parse_commands() {
                         break;
                     case scanner::token_kind::ScriptBlock:
                         parse_script();
+                        save_snapshot();
                         break;
                     case scanner::token_kind::Eof:
                         done = true;
@@ -1192,10 +1195,14 @@ void parser::add_delayed_theorem(environment const & env, name const & n, level_
 }
 
 void parser::save_snapshot() {
+    m_pre_info_data.clear();
     if (!m_snapshot_vector)
         return;
     if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
         m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line()));
+}
+
+void parser::save_pre_info_data() {
     // if elaborator failed, then m_pre_info_data contains type information before elaboration.
     if (m_info_manager) {
         m_info_manager->append(m_pre_info_data, false);

src/frontends/lean/parser.h

@@ -156,6 +156,7 @@ class parser {
     void save_snapshot();
     void save_overload(expr const & e);
     void save_type_info(expr const & e);
+    void save_pre_info_data();
 
 public:
     parser(environment const & env, io_state const & ios,

src/frontends/lean/server.cpp

@@ -84,6 +84,7 @@ void server::read_file(std::string const & fname) {
     if (in.bad() || in.fail()) {
         std::cout << "Error: failed to open file '" << fname << "'";
     } else {
+        m_fname = fname;
         m_lines.clear();
         for (std::string line; std::getline(in, line);) {
             m_lines.push_back(line);