fix: namespace completion to only use the short name

[Rob23oba]

This PR changes namespace completion to use the same algorithm as declaration identifier completion, which makes it use the short name (last name component) for completions instead of the full name, avoiding namespace duplications.

Closes #5654

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88078930a92aa55089e936a5fe8e99ec65ab2ceb --onto 6ca31baa55e4b29c9667085736863f9ca840b16c. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-15 11:20:19)
• ✅ Mathlib branch lean-pr-testing-8350 has successfully built against this PR. (2025-05-19 20:00:17) View Log

[mhuisi]

Thanks!

It's probably fine, but could you also double-check that completion still performs roughly the same with this change with import Mathlib?

You can do so by rebasing your PR on nightly-with-mathlib , creating a new project that depends on the PR testing branch, setting Lean4 > Trace: Server in VS Code to 'messages', observing the timings in the 'Lean: Editor' output panel for completion requests that VS Code emits and comparing against master. Single character identifier completion requests are usually the worst case.

[Rob23oba]

I ran the following test:

Test code

import Mathlib

open Lean Elab Command Server Completion

def test (c : Syntax) : CommandElabM Unit := do
  elabCommand c
  let fileMap := FileMap.ofString c.getTrailing?.get!.str
  let position := c.getTailPos?.get!
  let pos := fileMap.toPosition position
  let params : Lsp.CompletionParams := {
    textDocument := {
      uri := "file://Basic.lean"
    }
    position := {
      line := pos.line
      character := pos.column
    }
  }
  for _ in [0:30] do
    let trees ← getInfoTrees
    for tree in trees do
      let token ← RequestCancellationToken.new
      let time ← IO.monoNanosNow
      let hb ← IO.getNumHeartbeats
      discard <| (find? params fileMap position c tree {}).run token
      let hb' ← IO.getNumHeartbeats
      let time' ← IO.monoNanosNow
      Lean.logInfo m!"timing: {time' - time}, heartbeats: {hb' - hb}"

elab "#test_completion " c:command : command => test c

#test_completion #check A

on both nightly-testing and this PR, the results:

1. heartbeats increased marginally: 19379397 -> 19467124 (both rather consistent)
2. time decreased slightly (although this is probably just noise): average 691ms, standard deviation 25ms -> avarage 683ms, standard deviation 12ms

[mhuisi]

Great! :-)