-
Notifications
You must be signed in to change notification settings - Fork 406
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Revamp file reading and writing (#4906)
This PR: - changes the implementation of `readBinFile` and `readFile` to only require two system calls (`stat` + `read`) instead of one `read` per 1024 byte chunk. - fixes a bug where `Handle.getLine` would get tripped up by a NUL character in the line and cut the string off. This is caused by the fact that the original implementation uses `strlen` and `lean_mk_string` which is the backer of `mk_string` does so as well. - fixes a bug where `Handle.putStr` and thus by extension `writeFile` would get tripped up by a NUL char in the line and cut the string off. Cause here is the use of `fputs` when a NUL char is possible. Closes: #4891 Closes: #3546 Closes: #3741
- Loading branch information
Showing
4 changed files
with
62 additions
and
46 deletions.
There are no files selected for viewing
This file contains 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
This file contains 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
This file contains 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
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
def test : IO Unit := do | ||
let tmpFile := "3546.tmp" | ||
let firstLine := "foo\u0000bar\n" | ||
let content := firstLine ++ "hello world\nbye" | ||
IO.FS.writeFile tmpFile content | ||
let handle ← IO.FS.Handle.mk tmpFile .read | ||
let firstReadLine ← handle.getLine | ||
let cond := firstLine == firstReadLine && firstReadLine.length == 8 -- paranoid | ||
IO.println cond | ||
IO.FS.removeFile tmpFile | ||
|
||
/-- info: true -/ | ||
#guard_msgs in | ||
#eval test |