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

Add basic support for cancellation of resolution #4175

Merged

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Jun 14, 2023

Changes

  • Add support for cancelling resolution work at module granularity. Before this PR, the language server would always finish it's currently running resolution job before starting resolution on the most recent changes, skipping resolution work of obsolete changes that was not yet started. With this PR, the language server can also stop it's current resolution work at the module boundaries.
  • Add a telemetry publication that says how much time was spent on resolution

Testing

I see improved behavior on large Dafny codebases with this change. The IDE generally becomes more responsive, switching away from 'Resolving...' into other states faster.

Given that from a user perspective the resolution process is black box, there's no contract for when in that process cancellation should be supported. I think the right way to test this is to have a codebase that takes a long time to resolve, and to test that changes will always cancel the current resolution within a time smaller than X. However, making such a test is time consuming and I would like to deliver this fix to users already, so I'm not adding such a test yet.

I also haven't added a test for the telemetry change but that is not a user facing change.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer marked this pull request as ready for review June 14, 2023 19:31
@keyboardDrummer keyboardDrummer enabled auto-merge (squash) June 14, 2023 19:34
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like a small but great improvement that should definitely enhance the responsiveness of the resolution.
I would advise as well to later put these throwIfCancellationRequested also when starting to resolve individual declarations, because there could be a lot in a module.

@keyboardDrummer keyboardDrummer merged commit 8f1311c into dafny-lang:master Jun 15, 2023
@keyboardDrummer keyboardDrummer deleted the resolutionCancellation branch June 15, 2023 13:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants