fix(frontends/lean/parser): must save state of name_generator in parser snapshot

To provide typing and auto-completion information, we create a
background process by starting lean with the option --server.
In "server" mode, we create snapshots of the parser state.
The idea is to be able to quickly reprocess a file when the user makes a
modification. This commit fixes a bug in the snapshot operation.
It was not saving in the snapshots the unique name generator used by the parser.
By creating a fresh name generator, we may accidentally
assign the same internal name to two different constants.
This bug triggered the crash described in issue #593.

This commit fixes the test in the comment
https://github.com/leanprover/lean/issues/593#issuecomment-101768484

This commit also adds a smaller version of the problem to the test suite

src/frontends/lean/parser.cpp

@@ -116,6 +116,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_has_params = false;
     m_keep_theorem_mode = tmode;
     if (s) {
+        m_ngen               = s->m_ngen;
         m_local_level_decls  = s->m_lds;
         m_local_decls        = s->m_eds;
         m_level_variables    = s->m_lvars;
@@ -1839,7 +1840,7 @@ void parser::save_snapshot() {
     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_snapshot_vector->push_back(snapshot(m_env, m_ngen, m_local_level_decls, m_local_decls,
                                               m_level_variables, m_variables, m_include_vars,
                                               m_ios.get_options(), m_parser_scope_stack, m_scanner.get_line()));
 }

src/frontends/lean/parser.h

@@ -67,6 +67,7 @@ typedef list<parser_scope_stack_elem> parser_scope_stack;
 /** \brief Snapshot of the state of the Lean parser */
 struct snapshot {
     environment        m_env;
+    name_generator     m_ngen;
     local_level_decls  m_lds;
     local_expr_decls   m_eds;
     name_set           m_lvars; // subset of m_lds that is tagged as level variable
@@ -77,10 +78,10 @@ struct snapshot {
     unsigned           m_line;
     snapshot():m_line(0) {}
     snapshot(environment const & env, options const & o):m_env(env), m_options(o), m_line(1) {}
-    snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds,
-             name_set const & lvars, name_set const & vars, name_set const & includes, options const & opts,
-             parser_scope_stack const & pss, unsigned line):
-        m_env(env), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
+    snapshot(environment const & env, name_generator const & ngen, local_level_decls const & lds,
+             local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
+             name_set const & includes, options const & opts, parser_scope_stack const & pss, unsigned line):
+        m_env(env), m_ngen(ngen), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
         m_options(opts), m_parser_scope_stack(pss), m_line(line) {}
 };
 

tests/lean/interactive/snapshot_bug.input

@@ -0,0 +1,7 @@
+VISIT snapshot_bug.lean
+WAIT
+INSERT 21
+
+REPLACE 22
+lemma ker.has_one (Hom : is_hom f) : 1 ∈ ker f := sorry
+WAIT

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

@@ -0,0 +1,4 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGINWAIT
+-- ENDWAIT

tests/lean/interactive/snapshot_bug.lean

@@ -0,0 +1,32 @@
+import algebra.group data.set
+namespace group_hom
+open algebra
+-- ⁻¹ in eq.ops conflicts with group ⁻¹
+-- open eq.ops
+open set
+open function
+local attribute set [reducible]
+structure is_subgroup [class] {A : Type} (H : set A) : Type
+
+section
+variables {A B : Type}
+variable [s1 : group A]
+variable [s2 : group B]
+include s1
+include s2
+definition is_hom (f : A → B) := ∀ a b, f (a*b) = (f a)*(f b)
+
+variable f : A → B
+variable Hom : is_hom f
+definition ker : set A := λ a, (f a) = 1
+
+lemma ker.has_one (Hom : is_hom f) : 1 ∈ ker f := sorry
+theorem hom_map_one : f 1 = 1 := sorry
+theorem hom_map_mul_closed (Hom : is_hom f) (H : set A) : unit :=
+sorry
+
+variable {H : set A}
+variable [is_subgH : is_subgroup H]
+include is_subgH
+end
+end group_hom