Update ide mode to delay dependence scanning until the first check of the full buffer #4055
+12
−3
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
… current state of the buffer (for dependence scanning)
Contributor
|
See also #3941, which fixed a part of this issue. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Previously, if one created a new file and starting typing F* code in it, then one would have to restart the ide before trying to check any code, because the dependence scan would run on the initial state of the buffer (which would be empty).
Now, I update the "virtual file system" (vfs) entry for the file at each call to run_full_buffer in the IDE. This then makes the initial dependence scan run on the current version of the file rather than the initial version, avoiding the restart.
This actually also means that one can launch the ide without actually having any file on the disk, as shown by the new test case.
Note: this still doesn't solve the more general problem of adding dependences on the fly.