feat: Revamp file reading and writing #4906
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
tests/lean/3546.lean
Outdated
| IO.println cond | ||
| IO.FS.removeFile tmpFile | ||
|
|
||
| #eval test |
There was a problem hiding this comment.
This could use #guard_msgs, right?
There was a problem hiding this comment.
Might as well move this to tests/run now?
|
!bench |
|
Here are the benchmark results for commit aaff432. Benchmark Metric Change
======================================================
+ lake build clean task-clock -1.2% (-16.7 σ)
+ stdlib tactic execution -1.5% (-19.1 σ)
+ stdlib wall-clock -1.6% (-31.0 σ) |
|
!bench |
|
Here are the benchmark results for commit 1be6f69. |
tests/lean/3546.lean
Outdated
| IO.println cond | ||
| IO.FS.removeFile tmpFile | ||
|
|
||
| #eval test |
There was a problem hiding this comment.
Might as well move this to tests/run now?
|
|
||
| def readFile (fname : FilePath) : IO String := do | ||
| let data ← readBinFile fname | ||
| match String.fromUTF8? data with |
There was a problem hiding this comment.
Does this make a copy of the data?
There was a problem hiding this comment.
Yes, unfortunately the runtime representation of ByteArray has the data part inlined instead of as a pointer and the layout of the ByteArray and String object are not compatible :/.
|
Of course windows doesn't have getline and this breaks everything /o\ |
This PR:
readBinFileandreadFileto only require two system calls (stat+read) instead of onereadper 1024 byte chunk.Handle.getLinewould 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 usesstrlenandlean_mk_stringwhich is the backer ofmk_stringdoes so as well.Handle.putStrand thus by extensionwriteFilewould get tripped up by a NUL char in the line and cut the string off. Cause here is the use offputswhen a NUL char is possible.Closes: #4891
Closes: #3546
Closes: #3741