28211, "jabraham17", "[Bug]: 'fileReader.readLine' gets weird EOF errors on super long lines", "2025-12-16T00:52:23Z"
Summary of Problem
Description:
I am finding that fileReader.readLine throws UnexpectedEofError when giving very large lines to read (but under max(int))
Is this issue currently blocking your progress?
no
Steps to Reproduce
Source Code:
config var f = "file.txt";
config var n = 15_000;
use IO, Random;
var w = openWriter(f);
var a: [0..#n] real;
fillRandom(a);
w.writeln(a);
w.close();
{
var r = openReader(f);
defer r.close();
var line: string;
try {
while r.readLine(line) {
writeln("Read line of length ", line.size);
}
} catch e {
writeln("Caught error: ", e);
}
}
{
var r = openReader(f);
defer r.close();
var line: string;
try {
while true {
line = r.readLine(string);
writeln("Read line of length ", line.size);
}
} catch e: EofError {
} catch e {
writeln("Caught error: ", e);
}
}
{
var r = openReader(f);
defer r.close();
try {
for line in r.lines() {
writeln("Read line of length ", line.size);
}
} catch e {
writeln("Caught error: ", e);
}
}
Running this program as ./a.out --n=10 shows that all 3 methods to read lines works. But running by default with --n=15_000 shows that the first two crash with UnexpectedEofError (after reading the line) and only r.lines() works.
I see the same issues with bytes.
I would expect a BadFormatError if that line was longer than the internal buffer (as spec'd in the docs), but UnexpectedEofError seems like an erroneous error case, especially since r.lines() handles it fine