Reading a text file

Stream: lean4

[Reijo Jaakkola]

I am writing a test in IO_test.lean for IO.FS.Handle.read. When EOF is reached with this function, it should return an empty array. However, with the following line

let ys <- withFile <name of the file> Mode.read $ fun h => h.read 1;

I got as my output [76]. Furthermore, if I read four bytes, then I get [76,105,110,101]. However, if I add the following line before this line

withFile <name of the file> Mode.write fun h => do pure();

I do get the empty array as my output, as expected. What is going on here?

[Gabriel Ebner]

Maybe this bug? https://github.com/leanprover/lean4/pull/514

[Reijo Jaakkola]

Not sure what you mean. I have the change that you mentioned in my own branch, so it should not be causing this.

[Sebastian Ullrich]

man 3 fopen

w      Truncate  file  to zero length or create text file for writing.  The stream is positioned at the begin‐
              ning of the file.

Mode.write is expected to truncate the file

[Notification Bot]

This topic was moved here from #general > Reading a text file by Sebastian Ullrich

[Reijo Jaakkola]

But shouldn't Mode.read position the stream at the start of the file? In which case if the file is already empty (as it was in my case) the h.read should already return the empty array since it encounters EOF?

[Sebastian Ullrich]

I don't know what file you are reading, but the bytes you posted spell out "Line", that doesn't seem very arbitrary :)

[Reijo Jaakkola]

Lol, it did indeed contain them, I just forgot it... Thanks for the translation :)