feat: use incrementality for completion in tactic blocks #5205
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
|
Mathlib CI status (docs):
|
mhuisi
changed the title
Kha
reviewed
Aug 30, 2024
Comment on lines
39
to
40
| -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent | ||
| -- command starts with a keyword that (currently?) does not participate in completion. |
There was a problem hiding this comment.
This doesn't seem to be true anymore as the subsequent syntax can now also be a tactic keyword and they do participate in completion
There was a problem hiding this comment.
I changed the implementation to use the syntax endpos now, which (I think) should not cause any issues.
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Sep 16, 2024
…5205) This PR enables the use of incrementality for completion in tactic blocks. Consider the following example: ```lean example : True := by have : True := T sleep 10000 ``` Before this PR, in order to respond to a completion request after `T`, `sleep 10000` has to complete first since the command must be fully elaborated. After this PR, the completion request is responded to immediately.
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.
This PR enables the use of incrementality for completion in tactic blocks. Consider the following example:
Before this PR, in order to respond to a completion request after
T,sleep 10000has to complete first since the command must be fully elaborated. After this PR, the completion request is responded to immediately.