Skip to content

Commit

Permalink
fix: invalid namespace completions (#5322)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
mhuisi authored Sep 13, 2024
1 parent 626dda9 commit f989520
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 2 deletions.
10 changes: 9 additions & 1 deletion src/Lean/Environment.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/stdio.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit f989520

Please sign in to comment.