From f989520d2b17ec2fe987a69fee44a5272be1ff10 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 13 Sep 2024 14:23:03 +0200 Subject: [PATCH] fix: invalid namespace completions (#5322) This PR fixes an issue reported a while ago at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60Monad.2Emap.60.20is.20a.20namespace.3F/near/425662846 where `Monad.map` was incorrectly reported by the autocompletion as a namespace. The underlying issue is that `Monad.map` contains an internal declaration `_default`. This PR ensures that no namespaces are registered that only contain internal declarations. This also means that `open`ing namespaces that only contain internal declarations will now fail. The Mathlib adaption for this is a minor change where a declaration (i.e. a namespace that only contains internal declarations) was `open`ed by accident. --- src/Lean/Environment.lean | 10 +++++++++- tests/lean/stdio.lean | 2 +- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 18074c9806..8bceddada3 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1016,7 +1016,15 @@ private def registerNamePrefixes : Environment → Name → Environment @[export lean_environment_add] private def add (env : Environment) (cinfo : ConstantInfo) : Environment := - let env := registerNamePrefixes env cinfo.name + let name := cinfo.name + let env := match name with + | .str _ s => + if s.get 0 == '_' then + -- Do not register namespaces that only contain internal declarations. + env + else + registerNamePrefixes env name + | _ => env env.addAux cinfo @[export lean_display_stats] diff --git a/tests/lean/stdio.lean b/tests/lean/stdio.lean index afb38d9d57..f660d0e51b 100644 --- a/tests/lean/stdio.lean +++ b/tests/lean/stdio.lean @@ -10,7 +10,7 @@ out.putStrLn "print stdout" let err ← IO.getStderr; (err.putStr "print stderr" : IO Unit) -open usingIO IO +open IO def test : IO Unit := do FS.withFile "stdout1.txt" IO.FS.Mode.write $ fun h₁ => do