Completion in def in namespace can add unnecessary namespace components #3228
Comments
github-merge-queue bot
pushed a commit
that referenced
this issue
Feb 26, 2024
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 #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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Completion in the
defbut not in#checkcompletes toB1.foo. Both the surrounding namespace and the nesting A.B1 seem to be necessary to reproduce.The text was updated successfully, but these errors were encountered: