This PR significantly improves the test coverage of the language server,
providing at least a single basic test for every request that is used by
the client. It also implements infrastructure for testing all of these
requests, e.g. the ability to run interactive tests in a project context
and refactors the interactive test runner to be more maintainable.
Finally, it also fixes a small bug with the recently implemented unknown
identifier code actions for auto-implicits (#10442) that was discovered
in testing, where the "import all unambiguous unknown identifiers" code
action didn't work correctly on auto-implicit identifiers.
This PR speeds up auto-completion by a factor of ~3.5x through various
performance improvements in the language server. On one machine, with
`import Mathlib`, completing `i` used to take 3200ms and now instead
yields a result in 920ms.
Specifically, the following improvements are made:
- The watchdog process no longer de-serializes and re-serializes most
messages from the file worker before passing them on to the user - a
fast partial de-serialization procedure is now used to determine whether
the message needs to be de-serialized in full or not.
- `escapePart` is optimized to perform better on ASCII strings that do
not need escaping.
- `Json.compress` is optimized to allocate fewer objects.
- A faster JSON compression specifically for completion responses is
implemented that skips allocating `Json` altogether.
- The JSON compression has been moved to the task where we convert a
request response to `Json` so that converting to a string won't block
the output task of the FileWorker and so the `Json` value is not marked
as multi-threaded when we compress is, which drastically increases the
cost of reference-counting.
- The JSON representation of the `data?` field of each completion item
is optimized.
- Both the completion kind and the set of completion tags for each
imported completion item is now cached.
- The filtering of duplicate completion items is optimized.
Other adjustments:
- `LT UInt8` and `LE UInt8` are moved to Prelude so that they can be
used in `Init.Meta` for the name part escaping fast path.
- `Array.usize` is exposed since it was marked as `@[simp]`.
This PR generates `.ctorIdx` functions for all inductive types, not just
enumeration types. This can be a building block for other constructions
(`BEq`, `noConfusion`) that are size-efficient even for large
inductives.
It also renames it from `.toCtorIdx` to `.ctorIdx`, which is the more
idiomatic naming.
The old name exists as an alias, with a deprecation attribute to be
added after the next
stage0 update.
These functions can arguably compiled down to a rather efficient tag
lookup, rather than a `case` statement. This is future work (but
hopefully near future).
For a fair number of basic types the compiler is not able to compile a
function using `casesOn` until further definitions have been defined.
This therefore (ab)uses the `genInjectivity` flag and
`gen_injective_theorems%` command to also control the generation of this
construct.
For (slightly) more efficient kernel reduction one could use `.rec`
rather than `.casesOn`. I did not do that yet, also because it
complicates compilation.
This PR significantly improves the performance of auto-completion by
optimizing individual requests by a factor of ~2 and by giving language
clients like VS Code the opportunity to reuse the state of previous
completion requests, thus greatly reducing the latency for the
auto-completion list to update when adding more characters to an
identifier.
In my testing:
- The latency of completing `C` in a file with `import Mathlib` was
reduced from ~1650ms to ~800ms
- The latency of completing `Cat` in a file with `import Mathlib` was
reduced from ~800ms to ~430ms
- The latency of completing dot notation was mostly unaffected
- Successive completions are now practically instant, e.g. if we were to
complete `C` and then type it out to `Cat`, before it would take roughly
~1650ms + ~800ms, whereas now there is only a significant latency for
completing `C` (~800ms) and the completion list is updated practically
instantly when typing out `Cat`.
<details>
<summary>(Video) Auto-completion latency before this PR</summary>
</details>
<details>
<summary>(Video) Auto-completion latency after this PR</summary>
</details>
In detail, this PR makes the following changes:
- Set `isIncomplete` to `false` in non-synthetic completion responses so
that the client can re-use these completion states.
- Replace the server side fuzzy matching with a simple and fast check
that all characters in the identifier thus far are present in the same
order in the declaration to match against. There are some examples where
the simple and fast check yields a completion item that the fuzzy
matching would filter, but since VS Code filters the completion items
with its own fuzzy matching after that anyways, these extra completion
items are never actually displayed to the user.
- Remove all notions of scoring and sorting completion items from the
language server. We now rely entirely on the client to sort the
completion items as it sees fit. In my testing, the only significant
change as a result of this is that while the language server would
sometimes penalize namespaces with lots of components, VS Code instead
uses a strictly alphabetic order. Even before this change, we never
actually really prioritized local variables over global variables, so
the penalty wasn't very helpful in practice. We might add some small
form of local variable prioritization in the future, though.
- Remove the empty completion list hack that was introduced in #1885. It
does not appear to be necessary anymore.
It's difficult to distinguish theorems from regular definitions in the
completion menu, which is annoying when using completion for searching
one or the other. This PR makes theorem completions use the "Eureka!"
icon ()
to distinguish them more clearly from other completions.
NB: We are very limited in terms of which icons we can pick here since
[the completion kinds provided by LSP / VS
Code](https://code.visualstudio.com/docs/editor/intellisense#_types-of-completions)
are optimized for object-oriented programming languages, but I think
this choice strikes a nice balance between being easy to identify,
having some visual connection to theorem proving and not being used a
lot in other languages and thus not clashing with pre-existing
associations.
When the elaborator doesn't provide us with any `CompletionInfo`, we
currently provide no completions whatsoever. But in many cases, we can
still provide some helpful identifier completions without elaborator
information. This PR adds a fallback mode for this situation.
There is more potential here, but this should be a good start.
In principle, this issue alleviates #5172 (since we now provide
completions in these contexts). I'll leave it up to an elaboration
maintainer whether we also want to ensure that the completion infos are
provided correctly in these cases.
