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: language server dropping requests #7178

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Feb 21, 2025

This PR fixes a race condition in the language server that would sometimes cause it to drop requests and never respond to them when editing the header of a file. This in turn could cause semantic highlighting to stop functioning in VS Code, as VS Code would stop emitting requests when a prior request was dropped, and also cause the InfoView to become defective. It would also cause import auto-completion to feel a bit wonky, since these requests were sometimes dropped. This race condition has been present in the language server since its first version in 2020.

This PR also reverts the futile fix attempt in #7130.

The specific race condition was that if the file worker crashed or had to be restarted while a request was in flight in the file worker, then we wouldn't correctly replay it in our watchdog crash-restart logic. This PR adjusts this logic to fix this.

@mhuisi mhuisi added the changelog-server Language server, widgets, and IDE extensions label Feb 21, 2025
@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 Feb 21, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 21, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-02-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2025-02-21 17:41:17)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad1e04c82697938afb1df0525d8207dafaf8e043 --onto 2960b384af1f29f566f59a3ede8ac982e4628f19. (2025-02-23 20:15:55)

@mhuisi mhuisi marked this pull request as draft February 23, 2025 19:03
@mhuisi mhuisi force-pushed the mhuisi/dropped-responses branch from e0458c5 to d09ea5f Compare February 23, 2025 19:41
@mhuisi mhuisi force-pushed the mhuisi/dropped-responses branch from 30cda8b to 56a89de Compare February 24, 2025 10:00
@mhuisi mhuisi marked this pull request as ready for review February 24, 2025 10:01
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