search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.74k stars 427 forks source link

Lean's LSP internals appear in autocompletes for `IO.FS.Stream` #6135

Open david-christiansen opened 5 days ago

david-christiansen commented 5 days ago

Description

When a library transitively imports the Lean language server, then various functions that it defines in the IO.FS.Stream namespace show up in completion results for streams. In fact, they make up the majority of these completion results!

This could easily hit a user who's downstream of Verso or Alloy, both of which define their own LSP handlers.

Context

This came up when working on the IO chapter of the reference manual, but it's not a blocker in the slightest.

Steps to Reproduce

  1. Open a new empty Lean file and type #check IO.FS.Stream. and invoke completion.
  2. Observe the completion list
  3. Add import Lean as the first line of the file
  4. Invoke completion in the same position as before, and observe the completion list

Expected behavior:

I would expect that the completions were unchanged.

Actual behavior:

The majority of the completions list has to do with JSON-RPC and LSP, giving the impression that this is the purpose of IO.FS.Stream.

Suggestions

I think this could be solved in two ways in the language server:

  1. Get those functions out of the namespace. This would make the experience of working on the LSP server a bit worse, because dot-completion would no longer select those functions.

  2. Define abbref LspStream := IO.FS.Stream and then put the functions in the LSPStream namespace. This would spare downstream users from seeing them, and also perhaps make it marginally more clear which role a given stream plays.

Versions

"4.15.0-nightly-2024-11-19", on live.lean-lang.org.

Impact

I think this is a papercut at worst.

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

nomeata commented 5 days ago

Isn't there also the idea floating around of a change to name resolution, so that if open A, then A.B.f works as B.f for b : B? So that namespace can add selective dot notation to other types?

david-christiansen commented 5 days ago

That language change would indeed introduce a third way to remedy this!