fix: old&new frontend interference

The new test was not working because new frontend was using old
frontend function.

src/Lean/Attributes.lean

@@ -236,8 +236,7 @@ attrs.foldlM (fun env attr => attr.activateScoped env scope) env
    It activates scoped attributes in the new resulting namespace. -/
 @[export lean_push_scope]
 def pushScope (env : Environment) (header : Name) (isNamespace : Bool) : IO Environment := do
-let env := env.pushScopeCore header isNamespace;
-let ns  := env.getNamespace;
+let env := Lean.TODELETE.pushScopeCore env header isNamespace;
 -- attrs ← attributeArrayRef.get;
 -- attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
 pure env
@@ -245,7 +244,7 @@ pure env
 /- We use this function to implement commands `end foo` for closing namespaces and sections. -/
 @[export lean_pop_scope]
 def popScope (env : Environment) : IO Environment := do
-let env := env.popScopeCore;
+let env := Lean.TODELETE.popScopeCore env;
 -- attrs ← attributeArrayRef.get;
 -- attrs.foldlM (fun env attr => attr.popScope env) env
 pure env

src/Lean/Elab/Command.lean

@@ -279,7 +279,7 @@ fun ctx ref => EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 private def addScope (kind : String) (header : String) (newNamespace : Name) : CommandElabM Unit :=
 modify $ fun s => {
   s with
-  env    := s.env.registerNamespace newNamespace,
+  env    := registerNamespace s.env newNamespace,
   scopes := { s.scopes.head! with kind := kind, header := header, currNamespace := newNamespace } :: s.scopes
 }
 

src/Lean/Elab/Quotation.lean

@@ -416,7 +416,7 @@ let ctxMeta : Meta.Context := {
 let ctxTerm : Term.Context := {
   fileName := "foo",
   fileMap := FileMap.ofString "",
-  currNamespace := oldCtx.env.getNamespace,
+  currNamespace := Lean.TODELETE.getNamespace oldCtx.env,
   openDecls := oldCtx.open_nss.map $ fun n => OpenDecl.simple n []
 };
 match unsafeIO $ x.toIO {} { env := oldCtx.env } ctxMeta {} ctxTerm {} with

src/Lean/Elab/Util.lean

@@ -72,7 +72,7 @@ match attrParamSyntaxToIdentifier arg with
 | some k =>
   checkSyntaxNodeKind env k
   <|>
-  checkSyntaxNodeKindAtNamespaces env k env.getNamespaces -- TODO: fix for the new frontend. We do not store the current namespaces and OpenDecls in the environment
+  checkSyntaxNodeKindAtNamespaces env k (Lean.TODELETE.getNamespaces env) -- TODO: fix for the new frontend. We do not store the current namespaces and OpenDecls in the environment
   <|>
   checkSyntaxNodeKind env (defaultParserNamespace ++ k)
   <|>

src/Lean/Scopes.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Environment
 
 namespace Lean
+namespace TODELETE
 
 /- Scope management
 
@@ -40,8 +41,6 @@ registerSimplePersistentEnvExtension {
 @[init regScopeManagerExtension]
 constant scopeManagerExt : SimplePersistentEnvExtension Name ScopeManagerState := arbitrary _
 
-namespace Environment
-
 @[export lean_get_namespaces]
 def getNamespaces (env : Environment) : List Name :=
 (scopeManagerExt.getState env).namespaces
@@ -51,7 +50,7 @@ def getNamespaceSet (env : Environment) : NameSet :=
 
 @[export lean_is_namespace]
 def isNamespace (env : Environment) (n : Name) : Bool :=
-env.getNamespaceSet.contains n
+(getNamespaceSet env).contains n
 
 @[export lean_in_section]
 def inSection (env : Environment) : Bool :=
@@ -61,11 +60,11 @@ match (scopeManagerExt.getState env).isNamespace with
 
 @[export lean_has_open_scopes]
 def hasOpenScopes (env : Environment) : Bool :=
-!env.getNamespaces.isEmpty
+!(getNamespaces env).isEmpty
 
 @[export lean_get_namespace]
 def getNamespace (env : Environment) : Name :=
-match env.getNamespaces with
+match getNamespaces env with
 | (n::_) => n
 | _      => Name.anonymous
 
@@ -88,7 +87,7 @@ else s.namespaces.foldl
   none
 
 def registerNamespaceAux (env : Environment) (n : Name) : Environment :=
-if env.getNamespaceSet.contains n then env else scopeManagerExt.addEntry env n
+if (getNamespaceSet env).contains n then env else scopeManagerExt.addEntry env n
 
 @[export lean_register_namespace]
 def registerNamespace : Environment → Name → Environment
@@ -96,9 +95,9 @@ def registerNamespace : Environment → Name → Environment
 | env, _                  => env
 
 def pushScopeCore (env : Environment) (header : Name) (isNamespace : Bool) : Environment :=
-let ns    := env.getNamespace;
+let ns    := getNamespace env;
 let newNs := if isNamespace then ns ++ header else ns;
-let env   := env.registerNamespaceAux newNs;
+let env   := registerNamespaceAux env newNs;
 let env   := scopeManagerExt.modifyState env $ fun s =>
   { s with
     headers     := header :: s.headers,
@@ -107,12 +106,12 @@ let env   := scopeManagerExt.modifyState env $ fun s =>
 env
 
 def popScopeCore (env : Environment) : Environment :=
-if env.getNamespaces.isEmpty then env
+if (getNamespaces env).isEmpty then env
 else scopeManagerExt.modifyState env $ fun s =>
   { s with
     headers     := s.headers.tail!,
     namespaces  := s.namespaces.tail!,
     isNamespace := s.isNamespace.tail! }
 
-end Environment
+end TODELETE
 end Lean

tests/lean/run/namespaceIssue.lean

@@ -0,0 +1,10 @@
+new_frontend
+
+def Bla.x := 10
+
+namespace Foo
+export Bla(x)
+end Foo
+
+open Foo
+#check x