Unexpected workspace symbol search results

[Kha]

Gonna use this issue to collect a few unexpected results I've encountered

• searching for smap or SMap does not find the actual type

[gebner]

See also #1510.

[rish987]

I can take this one on. My investigation thus far shows that there may be a bug or some score weighting tweaking necessary in fuzzyMatchCore. If you add

  for ((name, score), _) in symbols.qsort (fun ((_, s1), _) ((_, s2), _) => s1 > s2) do
    dbg_trace s!"{name}: {score}"

to handleWorkspaceSymbol to print out the results in order of score, you'll find that when you query by SMap, the symbol Lean.SMap is there, but its score is too low to show up in the top 100 results.

[Kha]

Nice, sounds like the right direction!

[Kha]

We would probably expect matches with exact extract components to be at the top here?

[Kha]

(fun game: what's the shortest query to get me to Array.extract? aexr is pretty good!) edit: axt is probably optimal, though it's interesting that it wouldn't prioritize Array.ext