max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: Handle.read at EOF

Browse source
This commit is contained in:
Sebastian Ullrich 2022-08-23 11:11:18 +02:00 • committed by Leonardo de Moura
parent a69d7fb018
commit b010805000
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/runtime/io.cpp
View file

@ -282,17 +282,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /*
/* Handle.read : (@& Handle) → USize → IO ByteArray */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (feof(fp)) {
return io_result_mk_ok(alloc_sarray(1, 0, 0));
}
obj_res res = lean_alloc_sarray(1, 0, nbytes);
usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
if (n > 0) {
lean_sarray_set_size(res, n);
return io_result_mk_ok(res);
} else if (feof(fp)) {
dec_ref(res);
return io_result_mk_ok(alloc_sarray(1, 0, 0));
clearerr(fp);
lean_sarray_set_size(res, n);
return io_result_mk_ok(res);
} else {
dec_ref(res);
return io_result_mk_error(decode_io_error(errno, nullptr));