-
Notifications
You must be signed in to change notification settings - Fork 261
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: Formatting on VSCode for multi-file projects with project file #4918
Conversation
This PR makes sure StreamReaders are closed after use, which prevented formatting from overwriting the files randomly. I don't think I can write a test case for that.
Ensure formatting only consider the opened file
var reader = new StreamReader(uri.LocalPath); | ||
var str = reader.ReadToEnd(); | ||
reader.Close(); | ||
return new StringReader(str); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not OK for performance reasons. We need to design our code towards parsing in a streaming fashion. Could you take this part out for now so we can fix #4836 ASAP?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I usually worry more about correctness than performance, but I think I might find something that suits both of our needs and I'll put it up in a separate PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was about to write a StreamReader that auto-closes the file it reads when done, since I haven't found any. However, after analzying the code further, I don't think it is necessary.
Here is an analysis to consider:
IFileSystem.cs:50 public TextReader ReadFile(Uri uri) {
is called byDafnyProject.cs:53
which has aReadToEndAsync
but does not closes the streamIFileSystem.cs:25 public TextReader ReadFile(Uri uri) {
which has the same usage as its parentsLanguageServerFileSystem.cs:41 existingText = OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd();
which reads to the end but does not closes the streamLanguageServerFileSystem:92
which has the same usage as its parentsDafnyFile.cs:96
store the call as a closure in theGetContent
of a field of aDafnyFile
. This field is read in different places:- DafnyConsolePrinter.cs:72
ProgramParser.cs:269
var text = SourcePreprocessor.ProcessDirectives(getReader(), new List<string>());
which returns a source file after preprocessing. as a single string, but does not close the streamCoverageReporter.cs:321
var source = dafnyFile.GetContent().ReadToEnd();
reads to the end but does not close the streamFormatCommand.cs:75
using var content = dafnyFile.GetContent(); var originalText = await content.ReadToEndAsync();
This one also reads to the end and close the stream appropriately (I don't remember doing that, probably you did when you migrate to the new file system, so thanks)
- DafnyConsolePrinter.cs:72
In short, we currently never rely on streaming files and just forget to close it in almost every place. C# does perform auto-closing but is lazy and for big files it won't do it fast enough, which crashes the formatter on the command-line randomly.
So my recommandation is just to do this read and close it immediately so that it becomes possible to write after read. I'll create a separate PR for that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
DafnyProject.cs:53 which has a ReadToEndAsync but does not closes the stream
What makes you say it does not close the stream? It uses a using
directive:
using var textReader = fileSystem.ReadFile(uri);
Regarding the rest of the list, good finds! Let's fix them.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Blocking for performance reasons. Details in comments.
Source/DafnyDriver/CompilerDriver.cs
Outdated
@@ -596,6 +596,7 @@ private record TargetPaths(string Directory, string Filename) { | |||
if (moreText != null) { | |||
target.Write(moreText); | |||
} | |||
target.Close(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does the above using directive not already guarantee that target is closed? This line seems obsolete.
@@ -83,8 +83,9 @@ private class Indentations { | |||
public int binOpIndent = -1; | |||
public int binOpArgIndent = -1; | |||
|
|||
internal TokenNewIndentCollector(Program program) { | |||
internal TokenNewIndentCollector(Program program, Uri uri) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What uri is this? My impression is that you want to format one file at a time, which is fine, but let's make that explicit by renaming uri
to fileToFormat
ReduceBlockiness = reduceBlockiness | ||
}; | ||
foreach (var child in program.DefaultModuleDef.PreResolveChildren) { | ||
if (child.Tok.line != 0 && child.Tok.Uri != uri) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
child.Tok.line != 0
what is the meaning of this check? Could you assign the expression to a variable to clarify?
Thanks for fixing #4836 !!! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome, thanks
This PR makes sure StreamReaders are closed after use, which prevented formatting from overwriting the files randomly. The reason why to do this despite an obvious memory increase is that in [all places where we use this StreamReader](#4918 (comment)), we actually already read to the end and don't make use of the streaming. Before, the "dafny format" command was throwing exceptions on large files, and now it no longer throws an exception (test added for that) Even better, this solved the issue that when I create a blank Dafny file and try to save it, it used to complain with "Failed to save 'todelete.dfy': Unable to write file". (Fixes dafny-lang/ide-vscode#452) <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
I fixed the fact that the formatter was trying to incorporate every file in the DafnyFile project instead of considering only the file being viewed. I also updated the tests to reflect this new parameter.
I tested manually, and when formatting a file part of a project file, the formatting now works seamlessly (fixes #4836)
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.