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.

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

fix: don't issue atomic id completions when there is a dangling dot #5837

Merged
merged 1 commit into from
Nov 19, 2024

Conversation

mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Oct 25, 2024

This PR fixes an old auto-completion bug where x. would issue nonsensical completions when x. could not be elaborated as a dot completion.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 25, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 25, 2024

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0c190239a5e2d7f99413da0c54a575a0d0353b6 --onto 193b6f2bec332ac0bce33e10856a96163d4be456. (2024-10-25 13:10:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4bef3588b592c1cdcba190ef9bcd92b05fd5cbb7 --onto 5a99cb326c9e9052e135cc63ed02b63371cff6d3. (2024-11-19 09:02:23)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d6f898001bbb34604797a495d18803a9df584106 --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 12:21:25)

@mhuisi mhuisi force-pushed the mhuisi/atomic-dangling-dot branch from 51aa9e7 to a0171c4 Compare November 19, 2024 08:41
@mhuisi mhuisi force-pushed the mhuisi/atomic-dangling-dot branch from a0171c4 to 66d0c2e Compare November 19, 2024 12:04
@mhuisi mhuisi marked this pull request as ready for review November 19, 2024 12:21
@mhuisi mhuisi added the changelog-server Language server, widgets, and IDE extensions label Nov 19, 2024
@mhuisi mhuisi added this pull request to the merge queue Nov 19, 2024
Merged via the queue into leanprover:master with commit b7667c1 Nov 19, 2024
18 of 20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants