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

Skip verification on non-semantic syntax adjustments while typing #4940

Open
Rekkonnect opened this issue Jan 5, 2024 · 1 comment
Open
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@Rekkonnect
Copy link

Summary

Avoid verifying the entire file when the only changes are inside a comment, or insignificant whitespace (outside a string literal)

Background and Motivation

Sometimes we type comments, and sometimes we also format our code's indentation. Those changes in the syntax have 0 effect on the semantics of the program, and the verifier should therefore never run. All the verification information may be safely carried over to the next iteration of the code (assuming the LSP runs). This can save a significant amount of resources.

Proposed Feature

This is going to affect the LSP, taking advantage of the difference of the previous and the current syntax trees. If the difference is only found to be inside the comments, or in insignificant whitespace, we omit verifying the entire program again, copying the results from the previous verification.

As a further expansion of this feature, we may optionally avoid terminating the previous verification process if we discover that the syntax tree difference is indeed non-semantic.

It's important to note that the locations of the symbols are correctly recalculated, if need be.

Alternatives

No response

@Rekkonnect Rekkonnect added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Jan 5, 2024
@keyboardDrummer
Copy link
Member

Duplicate of #2331

@keyboardDrummer keyboardDrummer marked this as a duplicate of #2331 Jan 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Development

No branches or pull requests

2 participants