feat: import auto-completion#2904
Merged
mhuisi merged 6 commits intoleanprover:masterfrom Nov 24, 2023
Merged
Conversation
|
tydeu
approved these changes
Nov 17, 2023
Member
tydeu
left a comment
There was a problem hiding this comment.
LGTM! I imagine I may need to tweak a few things when I implement lake available-imports, but I presume that is okay.
kim-em
reviewed
Nov 20, 2023
kim-em
reviewed
Nov 20, 2023
38e478d to
3400b9e
Compare
Kha
approved these changes
Nov 20, 2023
Member
Kha
left a comment
There was a problem hiding this comment.
I didn't review ImportCompletion in much detail
3400b9e to
2818511
Compare
tydeu
reviewed
Nov 20, 2023
cf1024b to
259f00c
Compare
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 21, 2023
mhuisi
added a commit
to mhuisi/std4
that referenced
this pull request
Nov 21, 2023
mhuisi
added a commit
to mhuisi/std4
that referenced
this pull request
Nov 21, 2023
mhuisi
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 22, 2023
mhuisi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 23, 2023
mhuisi
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 23, 2023
mhuisi
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 23, 2023
2 tasks
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 26, 2023
As part of leanprover/lean4#2904, an unused parameter of `initSrcSearchPath` was removed. This PR adjusts Mathlib for this change. The corresponding Std PR that adjusts a use of `initSrcSearchPath` there is at leanprover-community/batteries#383. Co-authored-by: mhuisi <mhuisi@protonmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 27, 2023
As part of leanprover/lean4#2904, an unused parameter of `initSrcSearchPath` was removed. This PR adjusts Mathlib for this change. The corresponding Std PR that adjusts a use of `initSrcSearchPath` there is at leanprover-community/batteries#383. Co-authored-by: mhuisi <mhuisi@protonmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Alex J Best <alex.j.best@gmail.com> Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
This was referenced Jan 4, 2024
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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 adds basic auto-completion support for imports. Since it still lacks Lake support for accurate completion suggestions (cc @tydeu - we already know what needs to be done), it falls back to traversing the
LEAN_SRC_PATHfor available imports.Three kinds of import completion requests are supported:
importcommand. Triggered when requesting completions in an empty space within the header.importcommand.Since the set of imports is potentially expensive to compute, they are cached for 10 seconds after the last import auto-completion request.
Closes #2655.
Changes
This PR also makes the following changes:
importsyntax was adjusted to provide partial syntax when a trailing dot is used.FileWorker.leanwas refactored lightly with some larger definitions being broken apart.WorkerStategained two new fields:currHeaderStxtracks the current header syntax, as opposed to tracking only the initial header syntax ininitHeaderStx. When the header syntax changes, a task is launched that restarts the file worker after a certain delay to avoid constant restarts while editing the header. During this time period, we may still want to serve import auto-completion requests, so we need to know the up-to-date header syntax.importCachingTask?contains a task that computes the set of available imports.determineLakePathhas moved to a new fileLean/Util/LakePath.leanas it is now needed both inImportCompletion.leanandFileWorker.lean.forEachModuleInfromLake/Config/Blob.leanhas moved toLean/Util/Path.leanas it is a generally useful utility function that was useful for traversing theLEAN_SRC_PATHas well.Tests
Unfortunately, this PR lacks tests since the set of imports available in
tests/lean/interactivewill not be stable. In the future, I will add support for testing LSP requests in full project setups, which is when tests for import auto-completion will be added as well.