feat(library/init/lean/elaborator): pass current namespace to C++ elaborator

This seems to be the only information in `scope_mng_ext` we definitely need

library/init/lean/elaborator.lean

@@ -33,6 +33,7 @@ structure old_elaborator_state :=
 (include_vars : list name)
 (options : options)
 (next_inst_idx : nat)
+(ns : name)
 
 constant elaborate_command (filename : string) : expr → old_elaborator_state →
   option old_elaborator_state × message_log
@@ -312,10 +313,19 @@ def to_pexpr : syntax → elaborator_m expr
   | _ := error stx $ "unexpected node: " ++ to_string k.name)
 | stx := error stx $ "unexpected: " ++ to_string stx
 
+/-- Returns the active namespace, that is, the concatenation of all active `namespace` commands. -/
+def get_namespace : elaborator_m name := do
+  st ← get,
+  pure $ match st.local_state.ns_stack with
+  | ns::_ := ns
+  | _     := name.anonymous
+
 def old_elab_command (stx : syntax) (cmd : expr) : elaborator_m unit :=
 do cfg ← read,
    st ← get,
+   ns ← get_namespace,
    let (st', msgs) := elaborate_command cfg.filename cmd {
+     ns := ns,
      univs := st.local_state.univs.entries,
      vars := st.local_state.vars.entries,
      include_vars := st.local_state.include_vars.to_list,
@@ -594,13 +604,6 @@ def open.elaborate : elaborator :=
   modify $ λ st, {st with local_state := {st.local_state with
     open_decls := st.local_state.open_decls ++ v.spec}}
 
-/-- Returns the active namespace, that is, the concatenation of all active `namespace` commands. -/
-def get_namespace : elaborator_m name := do
-  st ← get,
-  pure $ match st.local_state.ns_stack with
-  | ns::_ := ns
-  | _     := name.anonymous
-
 def export.elaborate : elaborator :=
 λ stx, do
   let v := view «export» stx,

src/frontends/lean/vm_elaborator.cpp

@@ -340,6 +340,8 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
     auto options = to_options(cfield(vm_st, 5));
     p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
             parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info {1, 0}));
+    auto ns = to_name(cfield(vm_st, 7));
+    p.set_env(set_namespace(env, ns));
 
     auto cmd = to_expr(vm_cmd);
     message_log log;
@@ -356,7 +358,8 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
             cfield(vm_st, 3),
             cfield(vm_st, 4),
             cfield(vm_st, 5),
-            cfield(vm_st, 6)
+            cfield(vm_st, 6),
+            cfield(vm_st, 7)
         });
         vm_out = mk_vm_some(vm_st2);
     } catch (exception & e) {

src/library/scoped_ext.cpp

@@ -45,6 +45,12 @@ name const & get_namespace(environment const & env) {
     scope_mng_ext const & ext = get_extension(env);
     return !is_nil(ext.m_namespaces) ? head(ext.m_namespaces) : name::anonymous();
 }
+// temporary HACK
+environment set_namespace(environment const & env, name const & ns) {
+    scope_mng_ext ext;
+    ext.m_namespaces = {ns};
+    return update(env, ext);
+}
 
 name const & get_scope_header(environment const & env) {
     scope_mng_ext const & ext = get_extension(env);

src/library/scoped_ext.h

@@ -40,6 +40,7 @@ bool has_open_scopes(environment const & env);
 environment add_namespace(environment const & env, name const & ns);
 
 name const & get_namespace(environment const & env);
+environment set_namespace(environment const & env, name const & ns);
 name const & get_scope_header(environment const & env);
 /** \brief Return the current stack of namespaces.
     Example: at