possible bug in IO.FS.lines

Stream: general

[Asei Inoue]

IO.FS.lines can treat CRLF file in WIndows only. It can not treat CRLF files in Ubuntu (and CI!).

partial def lines (fname : FilePath) : IO (Array String) := do
  let h ← Handle.mk fname Mode.read
  let rec read (lines : Array String) := do
    let line ← h.getLine
    if line.length == 0 then
      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
      read <| lines.push line
    else
      pure <| lines.push line
  read #[]

[Asei Inoue]

This caused misterious error in my package, mdgen.

This specification is intended?

[Kim Morrison]

I guess it would be pretty safe to drop the platform check here and just jump straight to testing line.back, but I don't know what the preferred behaviour is for Windows files on non-Windows systems. You could open an issue to track this, at least.

[Asei Inoue]

where to open issue? leanprover/lean4?

[Jz Pan]

I think the standard C implementation (std::getline or fgets) only treats \n as linebreak, and actually will put \n into the returned string. So on Windows you'll get an extra \r in the return value, but this is OK.

[Asei Inoue]

done https://github.com/leanprover/lean4/issues/4573