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.
This PR is an effort to improve reasoning at the Nat level about
bitvectors and reduce of Fin and Nat.
It slightly tightens some proofs, but is generally aimed at reducing
inconsistencies between definitions at the Nat and Fin types in favor of
more consistently using Nat operations.
This ports leanprover/std4#664 to Lean core.
Here was the rational I provided in the discussion for
leanprover/std4#664:
It's mostly about consistency. If we use the same types and style in
definitions and proofs, there is less surprise when unfolding or
otherwise using definitions. We use some Nat based operations that
haven't been extended to Fin such as the bitwise operations, and I don't
want to pay the overhead of introducing a Fin version of every Bitvector
operation.
So this basically means Nat is preferred.
One argument potentially in favor of Fin is that we could reuse results
proven there, but that doesn't really seem to be the case so far.
A second argument is that we want to simplify expression to use more
canonical forms and we currently can pretty-print those operations
better using ofNat than ofFin. We could define the notations using ofFin
of course though, but that's additional operators that will show up in
expressions.
This is not a complete upstreaming of that file (it also supports `∀ᵉ (x
< 2) (y < 3), p x y` as shorthand for `∀ x < 2, ∀ y < 3, p x y`, but I
don't think we need this; it is used in Mathlib).
Syntaxes still need to be made built-in.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
This change
* moves `termination_by` and `decreasing_by` next to the function they
apply to
* simplify the syntax of `termination_by`
* apply the `decreasing_by` goal to all goals at once, for better
interactive use.
See the section in `RELEASES.md` for more details and migration advise.
This is a hard breaking change, requiring developers to touch every
`termination_by` in their code base. We decided to still do it as a
hard-breaking change, because supporting both old and new syntax at the
same time would be non-trivial, and not save that much. Moreover, this
requires changes to some metaprograms that developers might have
written, and supporting both syntaxes at the same time would make
_their_ migration harder.
This makes hover info, go to definition, etc work for the `h` in `cases
h : e`. The implementation is similar to that used for the `generalize h
: e = x` tactic.
This PR adds per-package server options to resolve#2455. It is based on
the previous work in #2456, but takes a different approach: options are
loaded for the specific file in the file worker when `print-paths` is
called, instead of loading them in the watchdog with a separate Lake
command. This change addresses review comments made in #2456.
In doing so, it introduces two new Lake config fields:
- `leanOptions`: `-D` flag options that are passed to both the language
server and `lean` when building.
- `moreServerOptions`: `-D` flag options that are passed to the language
server.
Since `print-paths` must also accept a file path to compute the options
for that file, this PR is changing the API for `print-paths`. As there
have been numerous complaints about the name `print-paths`, I also
decided to change it to `setup-file` in this PR, since it would break
compatibility with the old Lake API anyways.
This PR deprecates the Lakefile field `moreServerArgs` in favor of
`moreGlobalServerArgs`, as suggested in the review for #2456.
Fixes#2455
---------
Co-authored-by: digama0 <mcarneir@andrew.cmu.edu>
This implements a request handler for the `textDocument/rename` LSP
request, enabling renames via F2. It handles both local renames (e.g.
`let x := 1; x` to `let y := 1; y`) as well as global renames
(definitions).
Unfortunately it does not work for "orphan" files outside a project, as
it uses ilean data for the current file and this does not seem to be
saved for orphan files. As a result, the test file does not work,
although one can manually test the implementation against a project such
as mathlib. (This issue already exists for the "references" request,
e.g. ctrl click on the first `x` in `let x := 1; x` takes you to the
second one only if you are not in an orphan file.)
* Fixesleanprover-community/mathlib4#7124
* feat: allow upper case single character identifiers when relaxedAutoImplicit false
* update tests
* fix tests
* fix another test
---------
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.
