feat: handle \r on all operating systems in IO.FS.lines (#4973)

Closes: #4573
This commit is contained in:
Henrik Böving 2024-08-12 11:51:50 +02:00 committed by GitHub
parent 5c182bd540
commit da9d44df2d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 13 additions and 1 deletions

View file

@ -496,7 +496,7 @@ partial def lines (fname : FilePath) : IO (Array String) := do
pure lines
else if line.back == '\n' then
let line := line.dropRight 1
let line := if System.Platform.isWindows && line.back == '\x0d' then line.dropRight 1 else line
let line := if line.back == '\r' then line.dropRight 1 else line
read <| lines.push line
else
pure <| lines.push line

12
tests/lean/run/4573.lean Normal file
View file

@ -0,0 +1,12 @@
def test : IO Unit := do
let tmpFile := "4573.tmp"
let baseLines := #["foo", "bar", "foobar"]
let content := baseLines[0] ++ "\r\n" ++ baseLines[1] ++ "\n" ++ baseLines[2]
IO.FS.writeFile tmpFile content
let readLines ← IO.FS.lines tmpFile
IO.println <| baseLines == readLines
IO.FS.removeFile tmpFile
/-- info: true -/
#guard_msgs in
#eval test