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.
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.
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.
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:53which has aReadToEndAsyncbut 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:92which has the same usage as its parentsDafnyFile.cs:96store the call as a closure in theGetContentof a field of aDafnyFile. This field is read in different places:- DafnyConsolePrinter.cs:72
ProgramParser.cs:269var 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:321var source = dafnyFile.GetContent().ReadToEnd();reads to the end but does not close the streamFormatCommand.cs:75using 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.
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.
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.
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.
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.
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 !!! |
MikaelMayer
changed the title
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.