fix: auto-completion bugs and performance

[mhuisi]

This PR addresses several performance issues in the auto-completion implementation. It also fixes a number of smaller bugs related to auto-completion.

In a file with import Mathlib, the performance of various kinds of completions has improved as follows:

• Completing C: 49000ms -> 1400ms
• Completing Cat: 14300ms -> 1000ms
• Completing x. for x : Nat: 3700ms -> 220ms
• Completing . for an expected type of Nat: 11000ms -> 180ms

The following bugs have been fixed as well:

• VS Code never used our custom completion order. Now, the server fuzzy completion score decides the order that completions appear in.
• Dot auto-completion for private types did not work at all. It does now.
• Completing .<identifier> (where the expected type is used to infer the namespace) did not filter by the expected type and instead displayed all matching constants in the respective namespace. Now, it uses the expected type for filtering. Note that this is not perfect because sub-namespaces are technically correct completions as well (e.g. .Foo.foobar). Implementing this is future work.
• Completing . was often not possible at all. Now, as long as the . is not used in a bracket (where it may be used for the anonymous lambda feature, e.g. (. + 1)), it triggers the correct completion.
• Fixes Completion in def in namespace can add unnecessary namespace components #3228.
• The auto-completion in #check commands would always try to complete identifiers using the full declaration name (including namespaces) if it could be resolved. Now it simply uses the identifier itself in case users want to complete this identifier to another identifier.

Details

Regarding completion performance, I have more ideas on how to improve it further in the future.

Other changes:

• The feature that completions with a matching expected type are sorted to the top of the server-side ordering was removed. This was never enabled in VS Code because it would use its own completion item order and when testing it I found it to be more confusing than useful.
• In the server-side ordering, we would always display keywords at the top of the list. They are now displayed according to their fuzzy match score as well.

The following approaches have been used to improve performance:

• Pretty-printing the type for every single completion made up a significant amount of the time needed to compute the completions. We now do not pretty-print the type for every single completion that is offered to the user anymore. Instead, the language server now supports completionItem/resolve requests to compute the type lazily when the user selects a completion item.
  • Note that we need to keep the amount of properties that we compute in a resolve request to a minimum. When the server receives the resolve request, the document state may have changed from the state it was in when the initial auto-completion request was received. LSP doesn't tell us when it will stop sending resolve requests, so we cannot keep this state around, as we would have to keep it around forever.
    LSP's solution for this dilemma is to have servers send all the state they need to compute a response to a resolve request to the client as part of the initial auto completion response (which then sends it back as part of the resolve request), but this is clearly infeasible for all real language servers where the amount of state needed to resolve a request is massive.
    This means that the only practical solution is to use the current state to compute a response to the resolve request, which may yield an incorrect result. This scenario can especially occur when using LiveShare where the document is edited by another person while cycling through available completions.
• Request handlers can now specify a "header caching handler" that is called after elaborating the header of a file. Request handlers can use this caching handler to compute caches for information stored in the header. The auto-completion uses this to pre-compute non-blacklisted imported declarations, which in turn allow us to iterate only over non-blacklisted imported declarations where we would before iterate over all declarations in the environment. This is significant because blacklisted declarations make up about 4/5 of all declarations.
• Dot completion now looks up names modulo private prefixes to figure out whether a declaration is in the namespace of the type to the left of the dot instead of first stripping the private prefix from the name and then comparing it. This has the benefit that we do not need to scan the full name in most cases.

This PR also adds a couple of regression tests for fixed bugs, but no benchmarks. We will add these in the future when we add proper support for benchmarking server interaction sessions to our benchmarking architecture.

All tests that were broken by producing different completion output (empty detail field, added sortText? and data? fields) have been manually checked by me to be still correct before replacing their expected output.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 47595540bbcd5ef218e60e11d6586589ff3788e1 --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-22 20:44:40)
• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-02-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-02-26 09:39:25)