feat: display auto-implicits as inlay hints #3910
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Apr 15, 2024
|
Prototype developed with @nomeata at FRO retreat TODO:
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 15, 2024
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
It definitely needs an opt out (I personally dislike inlay hints because of the effect they have on the cursor), but I think it should be possible to opt out only of certain kinds of inlay hints (assuming we get more in the future). I do think this should be enabled by default though. It will be much more effective than the syntax highlighting at warning people that auto implicits are happening. |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Apr 15, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 15, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
Feb 4, 2025
This PR adds preliminary support for inlay hints, as well as support for inlay hints that denote the auto-implicits of a function. Hovering over an auto-implicit displays its type and double-clicking the auto-implicit inserts it into the text document.  This PR is an extension of #3910. ### Known issues - In VS Code, when inserting an inlay hint, the inlay hint may linger for a couple of seconds before it disappears. This is a defect of the VS Code implementation of inlay hints and cannot adequately be resolved by us. - When making a change to the document, it may take a couple of seconds until the inlay hints respond to the change. This is deliberate and intended to reduce the amount of inlay hint flickering while typing. VS Code has a mechanism of its own for this, but in my experience it is still far too sensitive without additional latency. - Inserting an auto-implicit inlay hint that depends on an auto-implicit meta-variable causes a "failed to infer binder type" error. We can't display these meta-variables in the inlay hint because they don't have a user-displayable name, so it is not clear how to resolve this problem. - Inlay hints are currently always resolved eagerly, i.e. we do not support the `textDocument/inlayHint/resolve` request yet. Implementing support for this request is future work. ### Other changes - Axioms did not support auto-implicits due to an oversight in the implementation. This PR ensures they do. - In order to reduce the amount of inlay hint flickering when making a change to the document, the language server serves old inlay hints for parts of the file that have not been processed yet. This requires LSP request handler state (that sometimes must be invalidated on `textDocument/didChange`), so this PR introduces the notion of a stateful LSP request handler. - The partial response mechanism that we use for semantic tokens, where we simulate incremental LSP responses by periodically emitting refresh requests to the client, is generalized to accommodate both inlay hints and semantic tokens. Additionally, it is made more robust to ensure that we never emit refresh requests while a corresponding request is in flight, which causes VS Code to discard the respond of the request, as well as to ensure that we keep prompting VS Code to send another request if it spuriously decides not to respond to one of our refresh requests. - The synthetic identifier of an `example` had the full declaration as its (non-canonical synthetic) range. Since we need a reasonable position for the identifier to insert an inlay hint for the auto-implicits of an `example`, we change the (canonical synthetic) range of the synthetic identifier to that of the `example` keyword. - The semantic highlighting request handling is moved to a separate file. ### Breaking changes - The semantic highlighting request handler is not a pure request handler anymore, but a stateful one. Notably, this means that clients that extend the semantic highlighting of the Lean language server with the `chainLspRequestHandler` function must now use the `chainStatefulLspRequestHandler` function instead.
|
Closing as this PR was superseded by #6768. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.