fix(frontends/lean/info_manager): bug in save_environment_options,

server was displaying old results

src/frontends/lean/info_manager.cpp

@@ -307,12 +307,13 @@ struct info_manager::imp {
         auto it  = m_env_info.begin();
         auto end = m_env_info.end();
         while (it != end) {
-            if (it->m_line > l)
+            if (it->m_line > l) {
                 break;
-            else if (it->m_line <= l && it->m_iteration < m_iteration)
-                it = m_env_info.erase(it);
-            else
+            } else if (it->m_line <= l && it->m_iteration < m_iteration) {
+                m_env_info.erase(it++);
+            } else {
                 ++it;
+            }
         }
         m_env_info.insert(env_info(l, m_iteration, env, o));
     }
@@ -647,7 +648,11 @@ void info_manager::display(environment const & env, io_state const & ios, unsign
 unsigned info_manager::get_processed_upto() const { return m_ptr->m_processed_upto; }
 optional<expr> info_manager::get_type_at(unsigned line, unsigned col) const { return m_ptr->get_type_at(line, col); }
 optional<expr> info_manager::get_meta_at(unsigned line, unsigned col) const { return m_ptr->get_meta_at(line, col); }
-void info_manager::block_new_info(bool f) {
-    m_ptr->block_new_info(f);
+void info_manager::block_new_info() {
+    m_ptr->block_new_info(true);
+}
+void info_manager::start() {
+    m_ptr->m_iteration++;
+    m_ptr->block_new_info(false);
 }
 }

src/frontends/lean/info_manager.h

@@ -46,7 +46,15 @@ public:
     void clear();
     void display(environment const & env, io_state const & ios, unsigned line,
                  optional<unsigned> const & col = optional<unsigned>()) const;
-    void block_new_info(bool f);
+    /** \brief Block new information from being inserted into this info_manager.
+        \remark #start_iteration unblocks it.
+    */
+    void block_new_info();
+    /** \breif Mark the start of a new information collection cycle.
+        It also enables new information to be added, i.e., it will undo
+        the effect of #block_new_info.
+    */
+    void start();
     unsigned get_processed_upto() const;
 };
 }

src/frontends/lean/server.cpp

@@ -53,7 +53,7 @@ void server::file::replace_line(unsigned line_num, std::string const & new_line)
     while (i < old_line.size() && i < new_line.size() && old_line[i] == new_line[i])
         i++;
     #endif
-    m_info.block_new_info(true);
+    m_info.block_new_info();
     #if 0
     // It turns out that is not a good idea to try to "keep" some of the information.
     // The info_manager will accumulate conflicting information and confuse the frontend.
@@ -67,7 +67,7 @@ void server::file::replace_line(unsigned line_num, std::string const & new_line)
 
 void server::file::insert_line(unsigned line_num, std::string const & new_line) {
     lock_guard<mutex> lk(m_lines_mutex);
-    m_info.block_new_info(true);
+    m_info.block_new_info();
     m_info.insert_line(line_num+1);
     while (line_num >= m_lines.size())
         m_lines.push_back("");
@@ -83,7 +83,7 @@ void server::file::insert_line(unsigned line_num, std::string const & new_line)
 
 void server::file::remove_line(unsigned line_num) {
     lock_guard<mutex> lk(m_lines_mutex);
-    m_info.block_new_info(true);
+    m_info.block_new_info();
     m_info.remove_line(line_num+1);
     if (line_num >= m_lines.size())
         return;
@@ -181,7 +181,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition
                     todo_file->m_snapshots.resize(i);
                     s = i == 0 ? m_empty_snapshot : todo_file->m_snapshots[i-1];
                     lean_assert(s.m_line > 0);
-                    todo_file->m_info.block_new_info(false);
+                    todo_file->m_info.start();
                     todo_file->m_info.set_processed_upto(s.m_line);
                     num_lines = todo_file->copy_to(block, s.m_line - 1);
                 }

tests/lean/interactive/num2.input

@@ -0,0 +1,16 @@
+VISIT num2.lean
+WAIT
+SET
+pp.notation false
+FINDP 39
+pos_num.si
+REPLACE 23
+  definition size (a : pos_num) : pos_num :=
+WAIT
+REPLACE 39
+  rec (pos pos_num.one) (λp, pos (pos_num.size p)) a
+WAIT
+FINDP 39
+pos_num.si
+FINDP 26
+pos_num.si

tests/lean/interactive/num2.input.expected.out

@@ -0,0 +1,38 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINSET
+-- ENDSET
+-- BEGINFINDP
+pos_num.bit0|pos_num → pos_num
+pos_num.is_inhabited|inhabited pos_num
+pos_num.inc|pos_num → pos_num
+pos_num.bit1|pos_num → pos_num
+pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.one|pos_num
+pos_num.num_bits|pos_num → pos_num
+pos_num|Type
+-- ENDFINDP
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINFINDP
+pos_num.size|pos_num → pos_num
+pos_num.bit0|pos_num → pos_num
+pos_num.is_inhabited|inhabited pos_num
+pos_num.inc|pos_num → pos_num
+pos_num.bit1|pos_num → pos_num
+pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.one|pos_num
+pos_num|Type
+-- ENDFINDP
+-- BEGINFINDP
+pos_num.size|pos_num → pos_num
+pos_num.bit0|pos_num → pos_num
+pos_num.is_inhabited|inhabited pos_num
+pos_num.inc|pos_num → pos_num
+pos_num.bit1|pos_num → pos_num
+pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
+pos_num.one|pos_num
+pos_num|Type
+-- ENDFINDP

tests/lean/interactive/num2.lean

@@ -0,0 +1,40 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+----------------------------------------------------------------------------------------------------
+import logic.classes.inhabited
+
+-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
+-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
+-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
+inductive pos_num : Type :=
+one  : pos_num,
+bit1 : pos_num → pos_num,
+bit0 : pos_num → pos_num
+
+theorem pos_num.is_inhabited [instance] : inhabited pos_num :=
+inhabited.mk pos_num.one
+
+namespace pos_num
+  definition inc (a : pos_num) : pos_num :=
+  rec (bit0 one) (λn r, bit0 r) (λn r, bit1 n) a
+
+  definition num_bits (a : pos_num) : pos_num :=
+  rec one (λn r, inc r) (λn r, inc r) a
+end pos_num
+
+inductive num : Type :=
+zero  : num,
+pos   : pos_num → num
+
+theorem num.is_inhabited [instance] : inhabited num :=
+inhabited.mk num.zero
+
+namespace num
+  definition inc (a : num) : num :=
+  rec (pos pos_num.one) (λp, pos (pos_num.inc p)) a
+
+  definition num_bits (a : num) : num :=
+  rec (pos pos_num.one) (λp, pos (pos_num.num_bits p)) a
+end num