From b010805000e0096cada3574250c5ef09d0e9f3f3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 23 Aug 2022 11:11:18 +0200 Subject: [PATCH] fix: `Handle.read` at EOF --- src/runtime/io.cpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 38bfa4bbbb..7c02e2fe1b 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -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));