Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Auto-complete offered after match … with #3462

Closed
nomeata opened this issue Feb 22, 2024 · 2 comments · Fixed by #3778
Closed

Auto-complete offered after match … with #3462

nomeata opened this issue Feb 22, 2024 · 2 comments · Fixed by #3778
Labels
bug Something isn't working

Comments

@nomeata
Copy link
Collaborator

nomeata commented Feb 22, 2024 •
edited
Loading

Description

Typing

example (n : Nat) : n = n :=  match n with

and waiting a bit opens a non-helpful popup that may even fire when then pressing enter.

bug

Additional Information

4.6.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@nomeata nomeata added the bug Something isn't working label Feb 22, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Feb 22, 2024

Seems to happen also on master (89490f6)

@nomeata
Copy link
Collaborator Author

nomeata commented Feb 22, 2024

The completion also depends on the symbol before with, here n; we get different completions with m there.

The tea time discussion says that this is somehow a consequence of the architecture and hard to fix 🤷

@nomeata nomeata mentioned this issue Mar 8, 2024
Open
This was referenced Mar 26, 2024
Open
Merged
github-merge-queue bot pushed a commit that referenced this issue Apr 2, 2024
@mhuisi @Kha
fix: don't use info nodes before cursor for completion (#3778)
ecf0459 
This fixes an issue where the completion would use info nodes before the
cursor for computing completions.

Fixes #3462.

ToDo:
- [x] Fix test failures for completions that previously worked by
accident (cc: @Kha)
- [x] stage0 update

---------

Co-authored-by: Sebastian Ullrich <[email protected]>
@Kha Kha closed this as completed in #3778 Apr 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: don't use info nodes before cursor for completion mhuisi/lean4
1 participant
@nomeata